1open HolKernel Parse boolLib bossLib; 2open listTheory rich_listTheory combinTheory; 3open pred_setTheory; 4 5val _ = new_theory "regexMarked"; 6 7 8open regexSemanticsTheory; 9open regexExecutableTheory; 10 11 12 13(* definitions *) 14(* ----------------------------------------------------------------------------- *) 15val _ = Datatype regexDatatypes.MReg_datatype_quot; 16 17(* this could possibly part of the theory file *) 18val MReg_rws = type_rws ``:'a MReg``; (*fetch "-" "MReg_distinct"*) 19val MReg_rw = LIST_CONJ MReg_rws; 20val MReg_ss = rewrites MReg_rws; 21 22 23val MARK_REG_def = Define ` 24 (MARK_REG (Eps) = MEps ) /\ 25 (MARK_REG (Sym c) = MSym F c ) /\ 26 (MARK_REG (Alt p q) = MAlt (MARK_REG p) (MARK_REG q)) /\ 27 (MARK_REG (Seq p q) = MSeq (MARK_REG p) (MARK_REG q)) /\ 28 (MARK_REG (Rep r) = MRep (MARK_REG r) ) 29`; 30val UNMARK_REG_def = Define ` 31 (UNMARK_REG (MEps) = Eps ) /\ 32 (UNMARK_REG (MSym _ c) = Sym c ) /\ 33 (UNMARK_REG (MAlt p q) = Alt (UNMARK_REG p) (UNMARK_REG q)) /\ 34 (UNMARK_REG (MSeq p q) = Seq (UNMARK_REG p) (UNMARK_REG q)) /\ 35 (UNMARK_REG (MRep r) = Rep (UNMARK_REG r) ) 36`; 37 38 39 40val empty_def = Define ` 41 (empty (MEps) <=> T ) /\ 42 (empty (MSym _ _) <=> F ) /\ 43 (empty (MAlt p q) <=> (empty p) \/ (empty q)) /\ 44 (empty (MSeq p q) <=> (empty p) /\ (empty q)) /\ 45 (empty (MRep r) <=> T ) 46`; 47 48val final_def = Define ` 49 (final (MEps) <=> F ) /\ 50 (final (MSym b _) <=> b ) /\ 51 (final (MAlt p q) <=> (final p) \/ (final q) ) /\ 52 (final (MSeq p q) <=> ((final p) /\ (empty q)) \/ (final q)) /\ 53 (final (MRep r) <=> final r ) 54`; 55 56val shift_def = Define ` 57 (shift _ (MEps) _ = MEps ) /\ 58 (shift m (MSym _ x) c = MSym (m /\ (x = c)) x ) /\ 59 (shift m (MAlt p q) c = MAlt (shift m p c) (shift m q c) ) /\ 60 (shift m (MSeq p q) c = MSeq (shift m p c) (shift ((m /\ (empty p)) \/ final p) q c)) /\ 61 (shift m (MRep r) c = MRep (shift (m \/ (final r)) r c) ) 62`; 63 64 65 66val acceptM_def = Define ` 67 (acceptM r [] = empty r ) /\ 68 (acceptM r (c::cs) = final (FOLDL (shift F) (shift T r c) cs)) 69`; 70 71 72 73 74 75 76 77 78 79 80(* rewrite theorems *) 81(* ----------------------------------------------------------------------------- *) 82(* rewrites for MARK_REG *) 83val MARK_REG_DEFs = store_thm ("MARK_REG_DEFs", `` 84 ( MARK_REG (Eps) = MEps ) /\ 85 (!c. MARK_REG (Sym c) = MSym F c ) /\ 86 (!p q. MARK_REG (Alt p q) = MAlt (MARK_REG p) (MARK_REG q)) /\ 87 (!p q. MARK_REG (Seq p q) = MSeq (MARK_REG p) (MARK_REG q)) /\ 88 (!r. MARK_REG (Rep r) = MRep (MARK_REG r) ) 89``, 90 91 REWRITE_TAC [MARK_REG_def] 92); 93 94(* rewrites for UNMARK_REG *) 95val UNMARK_REG_DEFs = store_thm ("UNMARK_REG_DEFs", `` 96 ( UNMARK_REG (MEps) = Eps ) /\ 97 (!b c. UNMARK_REG (MSym b c) = Sym c ) /\ 98 (!p q. UNMARK_REG (MAlt p q) = Alt (UNMARK_REG p) (UNMARK_REG q)) /\ 99 (!p q. UNMARK_REG (MSeq p q) = Seq (UNMARK_REG p) (UNMARK_REG q)) /\ 100 (!r. UNMARK_REG (MRep r) = Rep (UNMARK_REG r) ) 101``, 102 103 REWRITE_TAC [UNMARK_REG_def] 104); 105 106(* rewrites for empty *) 107val empty_DEFs = store_thm ("empty_DEFs", `` 108 ( empty (MEps) <=> T ) /\ 109 (!b c. empty (MSym b c) <=> F ) /\ 110 (!p q. empty (MAlt p q) <=> (empty p) \/ (empty q)) /\ 111 (!p q. empty (MSeq p q) <=> (empty p) /\ (empty q)) /\ 112 (!r. empty (MRep r) <=> T ) 113``, 114 115 REWRITE_TAC [empty_def] 116); 117 118(* rewrites for final *) 119val final_DEFs = store_thm ("final_DEFs", `` 120 ( final (MEps) <=> F ) /\ 121 (!b c. final (MSym b c) <=> b ) /\ 122 (!p q. final (MAlt p q) <=> (final p) \/ (final q) ) /\ 123 (!p q. final (MSeq p q) <=> ((final p) /\ (empty q)) \/ (final q)) /\ 124 (!r. final (MRep r) <=> final r ) 125``, 126 127 REWRITE_TAC [final_def] 128); 129 130(* rewrites for shift *) 131val shift_DEFs = store_thm ("shift_DEFs", `` 132 (!m c. shift m (MEps) c = MEps ) /\ 133 (!m b x c. shift m (MSym b x) c = MSym (m /\ (x = c)) x ) /\ 134 (!m p q c. shift m (MAlt p q) c = MAlt (shift m p c) (shift m q c) ) /\ 135 (!m p q c. shift m (MSeq p q) c = MSeq (shift m p c) (shift ((m /\ (empty p)) \/ final p) q c)) /\ 136 (!m r c. shift m (MRep r) c = MRep (shift (m \/ (final r)) r c) ) 137``, 138 139 REWRITE_TAC [shift_def] 140); 141 142(* rewrites for acceptM *) 143val acceptM_DEFs = store_thm ("acceptM_DEFs", `` 144 (!r. acceptM r [] = empty r ) /\ 145 (!r c cs. acceptM r (c::cs) = final (FOLDL (shift F) (shift T r c) cs)) 146``, 147 148 REWRITE_TAC [acceptM_def] 149); 150 151 152 153 154 155 156 157 158 159(* sanity and helper lemmata *) 160(* ----------------------------------------------------------------------------- *) 161(* --------------------- MARK_REG and UNMARK_REG *) 162(* generate nodelist helper definition *) 163val EXP_NODELIST_def = Define ` 164 (EXP_NODELIST (MEps) = [MEps]) /\ 165 (EXP_NODELIST (MSym b x) = [MSym b x]) /\ 166 (EXP_NODELIST (MAlt p q) = (EXP_NODELIST p) ++ (EXP_NODELIST q)) /\ 167 (EXP_NODELIST (MSeq p q) = (EXP_NODELIST p) ++ (EXP_NODELIST q)) /\ 168 (EXP_NODELIST (MRep r) = (EXP_NODELIST r)) 169`; 170 171val HAS_MARKS_def = Define ` 172 HAS_MARKS mr = ?x. MEM (MSym T x) (EXP_NODELIST mr) 173`; 174 175val HAS_MARKS_ALT_DEF = store_thm ("HAS_MARKS_ALT_DEF", `` 176 ( HAS_MARKS (MEps) <=> F ) /\ 177 (!b x. (HAS_MARKS (MSym b x) <=> b) ) /\ 178 (!p q. (HAS_MARKS (MAlt p q) <=> (HAS_MARKS p) \/ (HAS_MARKS q))) /\ 179 (!p q. (HAS_MARKS (MSeq p q) <=> (HAS_MARKS p) \/ (HAS_MARKS q))) /\ 180 (!r. (HAS_MARKS (MRep r) <=> (HAS_MARKS r)) ) 181``, 182 183 SIMP_TAC (list_ss++MReg_ss) [HAS_MARKS_def, EXP_NODELIST_def, EXISTS_OR_THM] 184); 185 186(* MARK_REG: afterwards all Sym c are MSym F c <=> !r. ~HAS_MARKS (MARK_REG r) *) 187val MARK_REG_NOT_HAS_MARKS_thm = store_thm ("MARK_REG_NOT_HAS_MARKS_thm", `` 188 (!r. ~HAS_MARKS (MARK_REG r)) 189``, 190 191 Induct_on `r` >> ( 192 FULL_SIMP_TAC (list_ss++MReg_ss) [HAS_MARKS_ALT_DEF, MARK_REG_DEFs] 193 ) 194); 195 196(* UNMARK_MARK reverses if MSyms are F *) 197val UNMARK_MARK_thm = store_thm ("UNMARK_MARK_thm", `` 198 (!mr. (~HAS_MARKS mr) ==> (mr = MARK_REG (UNMARK_REG mr))) 199``, 200 201 Induct_on `mr` >> ( 202 FULL_SIMP_TAC (list_ss++MReg_ss) [HAS_MARKS_ALT_DEF, UNMARK_REG_DEFs, MARK_REG_DEFs] 203 ) 204); 205 206(* MARK_UNMARK reverses always *) 207val MARK_UNMARK_thm = store_thm ("MARK_UNMARK_thm", `` 208 (!r. UNMARK_REG (MARK_REG r) = r) 209``, 210 211 Induct_on `r` >> ( 212 METIS_TAC [MARK_REG_DEFs, UNMARK_REG_DEFs] 213 ) 214); 215 216 217(* --------------------- empty *) 218(* accepts the empty language? i.e., <=> accept r [], or, [] IN (language_of r) *) 219val empty_accept_thm = store_thm ("empty_accept_thm", `` 220 (!mr. (empty mr) <=> (accept (UNMARK_REG mr) [])) 221``, 222 223 Induct_on `mr` >> ( 224 ASM_SIMP_TAC list_ss [empty_DEFs, UNMARK_REG_DEFs, accept_DEFs, split_DEFs, parts_DEFs] 225 ) 226); 227 228val empty_sem_thm = store_thm ("empty_sem_thm", `` 229 (!mr. (empty mr) <=> [] IN (language_of (UNMARK_REG mr))) 230``, 231 232 REWRITE_TAC [empty_accept_thm, accept_correctness_thm] 233); 234 235 236 237(* restregexes helper definition *) 238(* represents a set of regular expressions without marking *) 239(* each of the regular expressions stands for how to finish matching the input MReg, starting from a T mark *) 240val lang_of_MF_def = Define ` 241 (lang_of_MF (MEps) = {} ) /\ 242 (lang_of_MF (MSym b _) = if b then {[]} else {} ) /\ 243 (lang_of_MF (MAlt p q) = (lang_of_MF p) UNION (lang_of_MF q) ) /\ 244 (lang_of_MF (MSeq p q) = { u ++ v | u IN (lang_of_MF p) /\ v IN (language_of (UNMARK_REG q))} UNION (lang_of_MF q)) /\ 245 (lang_of_MF (MRep r) = { FLAT (u::l) | u IN (lang_of_MF r) /\ EVERY (\w. w IN (language_of (UNMARK_REG r))) l }) 246`; 247 248val lang_of_M_def = Define ` 249 lang_of_M m mr = (if m then (language_of (UNMARK_REG mr)) else {}) UNION (lang_of_MF mr) 250`; 251 252(* this rewrite lemma helps to simplify and clarify the proof of lang_of_M_shift_m_thm *) 253val lang_of_M_REWRS = store_thm ("lang_of_M_REWRS", `` 254 (!w m. w IN (lang_of_M m MEps ) <=> (m /\ (w = []))) /\ 255 (!w m b x. w IN (lang_of_M m (MSym b x)) <=> (m /\ (w = [x])) \/ (b /\ (w = []))) /\ 256 (!w m p q. w IN (lang_of_M m (MAlt p q)) <=> (w IN lang_of_M m p) \/ (w IN lang_of_M m q)) /\ 257 258 (!w m p q. w IN (lang_of_M m (MSeq p q)) <=> (w IN lang_of_MF q) \/ (?w1 w2. (w1 IN lang_of_M m p) /\ (w2 IN ( language_of (UNMARK_REG q))) /\ (w = w1 ++ w2))) /\ 259 260 (!w m r. w IN (lang_of_M m (MRep r) ) <=> (?w' wl. 261 (w = APPEND w' (FLAT wl)) /\ 262 ((m /\ (w' = [])) \/ (w' IN lang_of_MF r)) /\ 263 (!w'. MEM w' wl ==> (w' IN (language_of (UNMARK_REG r)))))) 264``, 265 266 SIMP_TAC 267 (list_ss++pred_setSimps.PRED_SET_ss++boolSimps.LIFT_COND_ss++boolSimps.EQUIV_EXTRACT_ss) 268 [lang_of_M_def, UNMARK_REG_DEFs, language_of_DEFs, lang_of_MF_def, UNION_EMPTY, EVERY_MEM] >> 269 270 REPEAT STRIP_TAC >- ( 271 Cases_on `m` >> METIS_TAC[] 272 ) >> 273 274 EQ_TAC >> STRIP_TAC >| 275 [ 276 rename1 `w = FLAT wl` >> 277 Q.EXISTS_TAC `[]` >> 278 Q.EXISTS_TAC `wl` >> 279 ASM_SIMP_TAC list_ss [] 280 , 281 METIS_TAC[] 282 , 283 DISJ1_TAC >> 284 FULL_SIMP_TAC list_ss [] >> 285 METIS_TAC[] 286 , 287 DISJ2_TAC >> 288 METIS_TAC[] 289 ] 290); 291 292val lang_of_MF_NOT_HAS_MARKS_thm = store_thm ("lang_of_MF_NOT_HAS_MARKS_thm", `` 293 (!mr. (~HAS_MARKS mr) ==> ((lang_of_MF mr) = {})) 294``, 295 296 Induct_on `mr` >> ( 297 ASM_SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [lang_of_MF_def, HAS_MARKS_ALT_DEF, EXTENSION] 298 ) 299); 300 301 302 303(* --------------------- final *) 304(* what is a state and what means a mark, what does this mean for final (how to interpret final) *) 305(* state is a set of positions, a mark is a potential matching, final says wether the end of such a matching is marked, whether one of the nondeterministic "sub"states accepts *) 306(* !!! if the regular expression after a mark accepts [] *) 307val final_sem_thm = store_thm ("final_sem_thm", `` 308 (!mr. (final mr) <=> [] IN lang_of_MF mr) 309``, 310 311 Induct_on `mr` >> ( 312 ASM_SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss++boolSimps.LIFT_COND_ss) [final_DEFs, lang_of_MF_def, language_of_DEFs, empty_sem_thm, boolTheory.EQ_IMP_THM] 313 ) >> 314 315 REPEAT STRIP_TAC >> 316 Q.EXISTS_TAC `[]` >> 317 SIMP_TAC (list_ss) [] 318); 319 320val final_NOT_HAS_MARKS_thm = store_thm ("final_NOT_HAS_MARKS_thm", `` 321 (!mr. (~HAS_MARKS mr) ==> ((final mr) <=> F)) 322``, 323 324 Induct_on `mr` >> ( 325 FULL_SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss) [final_sem_thm, HAS_MARKS_ALT_DEF, lang_of_MF_def] 326 ) 327); 328 329 330 331(* --------------------- shift *) 332(* how to create marks, relation to the input state, m and c *) 333(* m means whether to shift marks in from the left, and c says which "next positions" are to be marked *) 334(* recursively, m says whether to start, c says what to match, this should be right for all marks that are already there and the virtual mark m *) 335(* !!! if (in r) the regular expression after a mark (and the virtual mark m) accepts [c] *) 336(* final (shift m r c) <=> ? *) 337 338val shift_F_NOT_HAS_MARKS_thm = store_thm ("shift_F_NOT_HAS_MARKS_thm", `` 339 (!mr c. (~HAS_MARKS mr) ==> ((shift F mr c) = mr)) 340``, 341 342 Induct_on `mr` >> ( 343 ASM_SIMP_TAC std_ss [HAS_MARKS_ALT_DEF, shift_DEFs, final_NOT_HAS_MARKS_thm] 344 ) 345); 346 347val UNMARK_REG_shift_thm = store_thm ("UNMARK_REG_shift_thm", `` 348 (!mr m c. ((UNMARK_REG (shift m mr c)) = (UNMARK_REG mr))) 349``, 350 351 Induct_on `mr` >> ( 352 FULL_SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss) [HAS_MARKS_ALT_DEF, shift_DEFs, final_NOT_HAS_MARKS_thm, UNMARK_REG_DEFs] 353 ) 354); 355 356 357val lang_of_MF_lang_of_M_F_thm = store_thm ("lang_of_MF_lang_of_M_F_thm", `` 358 (!mr. (lang_of_MF mr) = lang_of_M F mr) 359``, 360 361 SIMP_TAC (std_ss++pred_setSimps.PRED_SET_ss) [lang_of_M_def] 362); 363 364val FLAT_splitup_thm = store_thm ("FLAT_splitup_thm", `` 365 (!c cs l. (c::cs = FLAT l) ==> (?ht tl. 366 (FLAT l = FLAT ((c::ht)::tl)) /\ 367 (!x. MEM x ((c::ht)::tl) ==> MEM x l) 368 )) 369``, 370 371 Induct_on `l` >- SIMP_TAC list_ss [] >> 372 373 REPEAT STRIP_TAC >> 374 Cases_on `h` >> (FULL_SIMP_TAC list_ss [] >> METIS_TAC []) 375); 376 377 378val lang_of_MF_shift_m_thm = store_thm ("lang_of_MF_shift_m_thm", `` 379 (!mr c cs m. (cs IN (lang_of_MF (shift m mr c))) <=> 380 ((c::cs) IN (lang_of_M m mr))) 381``, 382 383 Induct_on `mr` >| 384 [ 385 SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss++boolSimps.LIFT_COND_ss++boolSimps.EQUIV_EXTRACT_ss) 386 [shift_DEFs, lang_of_M_def, lang_of_MF_def, UNMARK_REG_DEFs, language_of_DEFs] 387 , 388 SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss++boolSimps.LIFT_COND_ss++boolSimps.EQUIV_EXTRACT_ss) 389 [shift_DEFs, lang_of_M_def, lang_of_MF_def, UNMARK_REG_DEFs, language_of_DEFs] 390 , 391 ASM_SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss++boolSimps.LIFT_COND_ss++boolSimps.EQUIV_EXTRACT_ss) 392 [shift_DEFs, lang_of_M_def, lang_of_MF_def, UNMARK_REG_DEFs, language_of_DEFs] 393 , 394 395 FULL_SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss++boolSimps.LIFT_COND_ss++boolSimps.EQUIV_EXTRACT_ss) 396 [shift_DEFs, lang_of_M_REWRS, lang_of_MF_def, UNMARK_REG_DEFs, language_of_DEFs, UNMARK_REG_shift_thm] >> 397 398 POP_ASSUM (K ALL_TAC) >> 399 POP_ASSUM (K ALL_TAC) >> 400 401 REWRITE_TAC [boolTheory.EQ_IMP_THM] >> 402 REPEAT STRIP_TAC >| 403 [ 404 DISJ2_TAC >> 405 Q.EXISTS_TAC `(c::u)` >> 406 Q.EXISTS_TAC `v` >> 407 ASM_SIMP_TAC (list_ss++QI_ss) [] 408 , 409 Cases_on `(m /\ empty mr \/ final mr) = F` >- ( 410 DISJ1_TAC >> FULL_SIMP_TAC (pure_ss) [lang_of_MF_lang_of_M_F_thm] 411 ) >> 412 413 FULL_SIMP_TAC (list_ss) [lang_of_M_def, empty_sem_thm, final_sem_thm] >> ( 414 DISJ2_TAC >> 415 Q.EXISTS_TAC `[]` >> 416 Q.EXISTS_TAC `(c::cs)` >> 417 ASM_SIMP_TAC (list_ss) [] 418 ) 419 , 420 Cases_on `(m /\ empty mr \/ final mr) = F` >- ( 421 DISJ2_TAC >> FULL_SIMP_TAC (pure_ss) [lang_of_MF_lang_of_M_F_thm] 422 ) >> 423 424 FULL_SIMP_TAC (list_ss) [lang_of_M_def, empty_sem_thm, final_sem_thm] >> ( 425 DISJ2_TAC >> 426 Q.EXISTS_TAC `[]` >> 427 Q.EXISTS_TAC `(c::cs)` >> 428 ASM_SIMP_TAC (list_ss) [] 429 ) 430 , 431 Cases_on `w1` >- ( 432 DISJ2_TAC >> 433 Cases_on `m` >- ( 434 FULL_SIMP_TAC (list_ss) [final_sem_thm, empty_sem_thm, lang_of_M_def] 435 ) >> 436 437 FULL_SIMP_TAC (list_ss) [final_sem_thm, empty_sem_thm, lang_of_M_def] 438 ) >> 439 440 DISJ1_TAC >> 441 Q.EXISTS_TAC `t` >> 442 Q.EXISTS_TAC `w2` >> 443 FULL_SIMP_TAC (list_ss) [] 444 ] 445 446 , 447 448 FULL_SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss++boolSimps.LIFT_COND_ss++boolSimps.EQUIV_EXTRACT_ss) 449 [shift_DEFs, lang_of_M_REWRS, lang_of_MF_def, UNMARK_REG_DEFs, language_of_DEFs, UNMARK_REG_shift_thm] >> 450 451 POP_ASSUM (K ALL_TAC) >> 452 453 REWRITE_TAC [boolTheory.EQ_IMP_THM] >> 454 REPEAT STRIP_TAC >| 455 [ 456 FULL_SIMP_TAC list_ss [lang_of_M_def, EVERY_MEM] >- ( 457 Cases_on `~(m \/ final mr)` >> FULL_SIMP_TAC list_ss [] >> ( 458 (* handles both cases: m, final mr *) 459 Q.EXISTS_TAC `[]` >> 460 Q.EXISTS_TAC `(c::u)::l` >> 461 FULL_SIMP_TAC (list_ss) [final_sem_thm] >> 462 METIS_TAC [] 463 ) 464 ) >> 465 Q.EXISTS_TAC `c::u` >> 466 Q.EXISTS_TAC `l` >> 467 FULL_SIMP_TAC list_ss [] 468 , 469 FULL_SIMP_TAC (list_ss) [] >> 470 471 ASSUME_TAC (Q.SPECL [`c`,`cs`,`wl`] FLAT_splitup_thm) >> 472 REV_FULL_SIMP_TAC (list_ss) [] >> 473 474 Q.EXISTS_TAC `ht` >> 475 Q.EXISTS_TAC `tl` >> 476 FULL_SIMP_TAC (list_ss) [lang_of_M_def, EVERY_MEM] 477 , 478 Cases_on `w'` >- ( 479 Cases_on `~final mr` >> FULL_SIMP_TAC (list_ss) [final_sem_thm] >> 480 481 ASSUME_TAC (Q.SPECL [`c`,`cs`,`wl`] FLAT_splitup_thm) >> 482 REV_FULL_SIMP_TAC (list_ss) [] >> 483 484 Q.EXISTS_TAC `ht` >> 485 Q.EXISTS_TAC `tl` >> 486 FULL_SIMP_TAC (list_ss) [lang_of_M_def, EVERY_MEM] 487 ) >> 488 Q.EXISTS_TAC `t` >> 489 Q.EXISTS_TAC `wl` >> 490 FULL_SIMP_TAC (list_ss) [lang_of_M_def, EVERY_MEM] 491 ] 492 ] 493); 494 495val lang_of_MF_shift_T_thm = store_thm ("lang_of_MF_shift_T_thm", `` 496 (!mr c cs. (~HAS_MARKS mr) ==> ( 497 (cs IN (lang_of_MF (shift T mr c)) <=> 498 (c::cs) IN (language_of (UNMARK_REG mr))) 499 )) 500``, 501 502 SIMP_TAC std_ss [lang_of_MF_shift_m_thm, lang_of_M_def, lang_of_MF_NOT_HAS_MARKS_thm, UNION_EMPTY] 503); 504 505val final_FOLDL_shift_F_thm = store_thm ("final_FOLDL_shift_F_thm", `` 506 (!mr w. (final (FOLDL (shift F) mr w)) <=> (w IN (lang_of_MF mr))) 507``, 508 509 Induct_on `w` >> ( 510 FULL_SIMP_TAC (list_ss++pred_setSimps.PRED_SET_ss) [final_sem_thm, lang_of_MF_shift_m_thm, lang_of_M_def] 511 ) 512); 513 514 515(* --------------------- acceptM *) 516(* just rewrites *) 517(* should be enough, essentially recurses the shifting with initialization first and is therefore just an inductive extension of the things before *) 518(* 519 (acceptM r [] = empty r ) /\ 520 (acceptM r ((c:'a)::cs) = final (FOLDL (shift F) (shift T r c) cs)) 521*) 522 523 524 525 526 527 528 529 530(* correctness of definition *) 531(* ----------------------------------------------------------------------------- *) 532val acceptM_correctness_thm = store_thm("acceptM_correctness_thm", ``!r w. acceptM (MARK_REG r) w <=> w IN (language_of r)``, 533 534 Cases_on `w` >> ( 535 REWRITE_TAC [acceptM_DEFs, empty_sem_thm, MARK_UNMARK_thm] >> 536 SIMP_TAC list_ss [MARK_REG_NOT_HAS_MARKS_thm, lang_of_MF_shift_T_thm, MARK_UNMARK_thm, final_FOLDL_shift_F_thm] 537 ) 538); 539 540val acceptM_accept_thm = store_thm("acceptM_accept_thm", ``!r w. acceptM (MARK_REG r) w <=> accept r w``, 541 542 REWRITE_TAC [acceptM_correctness_thm, accept_correctness_thm] 543); 544 545 546 547 548 549 550 551 552val _ = export_theory(); 553