1open HolKernel Parse boolLib bossLib; 2 3open monadsyntax ltlTheory errorStateMonadTheory 4 5local open stringTheory in end 6 7val _ = new_theory "formParse"; 8 9(* grammar parsed looks like 10 11 F ::= D "->" F | D 12 D ::= C "|" D | C 13 C ::= U "&" C | U 14 U ::= B "U" U | B 15 B ::= "G" B | "F" B | "X" B | "!" B | "(" F ")" | <id> 16 17 all the binary operators (->, |, & and U) are right-associative, 18 and that order gives their relative precedences, so that -> is 19 weakest and U is tightest. 20 21 Identifiers are non-empty strings of lower-case letters. 22 23 This is (fairly) consistent with the grammar for temporal formulas in 24 25 https://spot.lrde.epita.fr/tl.pdf 26 27 There's no support for 'true' and 'false' as special reserved words. 28 29*) 30 31val _ = ParseExtras.tight_equality() 32val _ = add_monadsyntax() 33 34val _ = temp_inferior_overload_on ("return",``errorStateMonad$UNIT``) 35val _ = temp_inferior_overload_on ("fail", ``errorStateMonad$ES_FAIL``) 36val _ = temp_overload_on ("monad_bind", ``errorStateMonad$BIND``) 37val _ = temp_overload_on ("monad_unitbind", ``errorStateMonad$IGNORE_BIND``); 38val _ = temp_overload_on ("assert", ``errorStateMonad$ES_GUARD``); 39val _ = temp_overload_on ("++", ``errorStateMonad$ES_CHOICE``); 40 41val token_def = Define��� 42 (token p [] = p []) ��� 43 (token p (h::t) = if isSpace h then token p t else p (h::t)) 44���; 45 46val token_APPEND = Q.store_thm( 47 "token_APPEND[simp]", 48 ���EVERY isSpace s1 ��� token p (s1 ++ s2) = token p s2���, 49 Induct_on ���s1��� >> simp[token_def]); 50 51val token_Spaces = token_APPEND |> Q.INST [���s2��� |-> ���[]���] 52 |> REWRITE_RULE [listTheory.APPEND_NIL] 53 54val literal_def = Define��� 55 literal s inp = if s <<= inp then SOME ((), DROP (LENGTH s) inp) 56 else NONE 57���; 58 59val ident_def = Define��� 60 (ident [] = NONE) ��� 61 (ident (h::t) = if isAlpha h ��� isLower h then 62 case ident t of 63 NONE => SOME([h], t) 64 | SOME (i, r) => SOME (h::i, r) 65 else NONE) 66���; 67 68val ident_EQ_SOME = Q.store_thm( 69 "ident_EQ_SOME[simp]", 70 ���ident s = SOME v ��� 71 ���px sx. s = px ++ sx ��� px ��� [] ��� EVERY (��c. isAlpha c ��� isLower c) px ��� 72 (���c t. sx = c::t ��� ��isAlpha c ��� ��isLower c) ��� v = (px, sx)���, 73 qid_spec_tac ���v��� >> Induct_on ���s��� >> simp[ident_def] >> 74 rpt gen_tac >> rename [���isAlpha c1���] >> Cases_on ���isAlpha c1 ��� isLower c1��� 75 >- (simp[optionTheory.option_case_eq, pairTheory.pair_case_eq, PULL_EXISTS] >> 76 rw[EQ_IMP_THM] 77 >- (rw[] >> 78 fs[ident_def, optionTheory.option_case_eq, pairTheory.pair_case_eq])>> 79 Cases_on ���px��� >> fs[] >> rw[] >> 80 rename [���ident (cs ++ sx) = NONE���] >> Cases_on ���cs��� >> simp[] >> 81 Cases_on ���sx��� >> fs[ident_def]) >> 82 simp[] >> rw[] >> Cases_on ���px��� >> simp[] >> metis_tac[]); 83 84val token_EQ_NONE = Q.store_thm( 85 "token_EQ_NONE", 86 ���(token p s = NONE) ��� 87 ���px sx. s = px ++ sx ��� EVERY isSpace px ��� (���h t. sx = h::t ��� ��isSpace h) ��� 88 p sx = NONE���, 89 Induct_on ���s��� >> simp[token_def, TypeBase.case_eq_of ``:bool``] >> rw[] >> 90 rw[EQ_IMP_THM] 91 >- (rename [���h :: (px ++ sx)���] >> map_every qexists_tac [���h::px���, ���sx���] >> 92 simp[]) 93 >- (rename [���h::rest = _ ++ _���] >> map_every qexists_tac [���[]���, ���h::rest���] >> 94 simp[]) 95 >- (rename [���h::rest = px ++ sx���] >> Cases_on ���isSpace h��� 96 >- (simp[] >> Cases_on ���px��� >> fs[] >> rw[] >> metis_tac[]) 97 >- (���px = []��� by (Cases_on ���px��� >> fs[] >> rw[] >> fs[]) >> 98 fs[]))); 99 100val token_EQ_SOME = Q.store_thm( 101 "token_EQ_SOME", 102 ���(token p s = SOME (v, s')) ��� 103 ���px sx. s = px ++ sx ��� EVERY isSpace px ��� (���h t. sx = h :: t ��� ��isSpace h) ��� 104 p sx = SOME (v, s')���, 105 Induct_on ���s��� >> simp[token_def, TypeBase.case_eq_of ���:bool���] >> 106 qx_gen_tac ���c��� >> Cases_on ���isSpace c��� >> simp[] 107 >- (rw[EQ_IMP_THM] 108 >- (map_every qexists_tac [���c :: px���, ���sx���] >> simp[]) >> 109 ������pt. px = c :: pt��� by (Cases_on ���px��� >> fs[] >> rw[] >> fs[]) >> 110 fs[] >> metis_tac[]) >> 111 rw[EQ_IMP_THM] 112 >- (rename [���p (c::s) = SOME _���] >> map_every qexists_tac [���[]���, ���c::s���] >> 113 simp[]) >> 114 Cases_on ���px��� >> fs[]); 115 116val literal_EQ_SOME = Q.store_thm( 117 "literal_EQ_SOME", 118 ���literal l s = SOME ((), sx) ��� (s = l ++ sx)���, 119 csimp[literal_def, rich_listTheory.IS_PREFIX_APPEND, PULL_EXISTS, 120 rich_listTheory.DROP_LENGTH_APPEND]); 121 122val literal_EQ_NONE = Q.store_thm( 123 "literal_EQ_NONE", 124 ���literal l s = NONE ��� ��(l <<= s)���, 125 simp[literal_def]); 126 127val parseFGX_def = Define ��� 128 parseFGX fgx top = 129 do 130 token (literal "F") ; 131 f <- fgx ; 132 return (LTL_F f "") 133 od ++ 134 do 135 token (literal "G") ; 136 f <- fgx ; 137 return (LTL_G f "") 138 od ++ 139 do 140 token (literal "X") ; 141 f <- fgx ; 142 return (F_X f) 143 od ++ 144 do 145 token (literal "!") ; 146 f <- fgx ; 147 return (F_NEG f) 148 od ++ 149 do 150 token (literal "(") ; 151 f <- top ; 152 token (literal ")") ; 153 return f 154 od ++ 155 do 156 v <- token ident ; 157 return (F_VAR v) 158 od 159���; 160 161val parseFGX_CONG = Q.store_thm( 162 "parseFGX_CONG[defncong]", 163 ������s1 s2 f1 f2 top1 top2. 164 (s1 = s2) ��� (���s. LENGTH s < LENGTH s1 ��� (f1 s = f2 s)) ��� 165 (���s. LENGTH s < LENGTH s1 ��� (top1 s = top2 s)) ��� 166 (parseFGX f1 top1 s1 = parseFGX f2 top2 s2)���, 167 simp[] >> rpt strip_tac >> 168 simp[parseFGX_def, GSYM ES_CHOICE_ASSOC, IGNORE_BIND_DEF] >> 169 ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 170 ONCE_REWRITE_TAC [BIND_DEF] >> 171 rename [���token (literal "F") s0���] >> 172 reverse (Cases_on ���token (literal "F") s0���) >> simp[] 173 >- (rename [���token (literal "F") s0 = SOME p���] >> Cases_on ���p��� >> simp[] >> 174 simp[BIND_DEF] >> fs[token_EQ_SOME, literal_EQ_SOME] >> 175 rename [���option_CASE (f2 s')���, ���f1 _ = f2 _���] >> 176 reverse (Cases_on ���f2 s'���) >> simp[UNIT_DEF] 177 >- (rename [���f2 s' = SOME p���] >> Cases_on ���p��� >> simp[]) >> 178 REWRITE_TAC [GSYM listTheory.APPEND_ASSOC, listTheory.APPEND] >> 179 ntac 4 (ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 180 simp[BIND_DEF, token_def, literal_def])) >> 181 fs[token_EQ_NONE, literal_EQ_NONE] >> Cases_on ���sx��� >> fs[] 182 >- simp[ES_CHOICE_DEF, token_Spaces, BIND_DEF, token_def, literal_def] >> 183 ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 184 simp[token_Spaces, BIND_DEF, token_def, literal_def] >> rw[] 185 >- (rename [���option_CASE (f2 s2)���, ���f1 _ = f2 _���] >> Cases_on ���f2 s2��� >> 186 simp[] 187 >- ntac 3 (ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 188 simp[BIND_DEF, token_def, literal_def]) >> 189 rename [���f2 s2 = SOME p���] >> Cases_on ���p��� >> simp[UNIT_DEF]) >> 190 ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 191 simp[BIND_DEF, token_def, literal_def] >> rw[] 192 >- (rename [���option_CASE (f2 s2)���, ���f1 _ = f2 _���] >> Cases_on ���f2 s2��� >> 193 simp[] 194 >- ntac 2 (ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 195 simp[BIND_DEF, token_def, literal_def]) >> 196 rename [���f2 s2 = SOME p���] >> Cases_on ���p��� >> simp[UNIT_DEF]) >> 197 ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 198 simp[BIND_DEF, token_def, literal_def] >> rw[] 199 >- (rename [���option_CASE (f2 s2)���, ���f1 _ = f2 _���] >> Cases_on ���f2 s2��� >> 200 simp[] 201 >- ntac 2 (ONCE_REWRITE_TAC [ES_CHOICE_DEF] >> 202 simp[BIND_DEF, token_def, literal_def]) >> 203 rename [���f2 s2 = SOME p���] >> Cases_on ���p��� >> simp[UNIT_DEF]) >> 204 simp[ES_CHOICE_DEF, BIND_DEF, token_def, literal_def] >> rw[]); 205 206val ParseFGX_def = tDefine "ParseFGX" ` 207 ParseFGX top s = parseFGX (ParseFGX top) top s 208` (WF_REL_TAC ���inv_image $< (STRLEN o SND)���); 209 210val ParseFGX_thm = 211 ParseFGX_def 212 |> SIMP_RULE (srw_ss() ++ boolSimps.ETA_ss) 213 [parseFGX_def, Once (GSYM FUN_EQ_THM)] 214 215val mksafe_def = Define��� 216 mksafe f s = case f s of 217 NONE => NONE 218 | SOME (v, s') => if IS_SUFFIX s s' then SOME (v, s') 219 else NONE 220���; 221 222val is_safe_def = Define��� 223 is_safe p = ���s s' v. p s = SOME (v,s') ��� IS_SUFFIX s s' 224���; 225 226val is_safe_mksafe = Q.store_thm( 227 "is_safe_mksafe[simp]", 228 ���is_safe (mksafe p)���, 229 simp[is_safe_def, mksafe_def, optionTheory.option_case_eq, 230 pairTheory.pair_case_eq]); 231 232val IGNORE_BIND_EQ_SOME = Q.store_thm( 233 "IGNORE_BIND_EQ_SOME[simp]", 234 ���IGNORE_BIND m1 m2 s = SOME r ��� ���v0 s'. m1 s = SOME (v0,s') ��� m2 s' = SOME r���, 235 simp[IGNORE_BIND_DEF, BIND_DEF, optionTheory.option_case_eq, 236 pairTheory.pair_case_eq, PULL_EXISTS]); 237 238val is_safe_mksafe_id = Q.store_thm( 239 "is_safe_mksafe_id", 240 ���is_safe p ��� mksafe p = p���, 241 simp[is_safe_def, mksafe_def, FUN_EQ_THM, optionTheory.option_case_eq, 242 pairTheory.pair_case_eq, PULL_EXISTS] >> rw[] >> csimp[] >> 243 metis_tac[optionTheory.option_CASES, pairTheory.pair_CASES]); 244 245val IS_SUFFIX_APPEND_I = Q.store_thm( 246 "IS_SUFFIX_APPEND_I", 247 ���IS_SUFFIX m n ��� IS_SUFFIX (p ++ m) n���, 248 simp[rich_listTheory.IS_SUFFIX_APPEND, PULL_EXISTS]); 249 250val IS_SUFFIX_APPEND_E = Q.store_thm( 251 "IS_SUFFIX_APPEND_E", 252 ���IS_SUFFIX m (p ++ n) ��� IS_SUFFIX m n���, 253 simp[rich_listTheory.IS_SUFFIX_APPEND, PULL_EXISTS]); 254 255val IS_SUFFIX_TRANS = Q.store_thm( 256 "IS_SUFFIX_TRANS", 257 ���IS_SUFFIX m n ��� IS_SUFFIX n p ��� IS_SUFFIX m p���, 258 metis_tac[rich_listTheory.IS_PREFIX_TRANS, 259 rich_listTheory.IS_SUFFIX_compute]); 260 261val is_safe_BIND = Q.store_thm( 262 "is_safe_BIND", 263 ���is_safe m ��� (���v. is_safe (f v)) ��� is_safe (BIND m f)���, 264 simp[is_safe_def, BIND_DEF, optionTheory.option_case_eq, PULL_EXISTS, 265 pairTheory.pair_case_eq] >> rpt strip_tac >> 266 rpt (first_x_assum drule) >> metis_tac[IS_SUFFIX_TRANS]); 267 268val is_safe_ParseFGX = Q.store_thm( 269 "is_safe_ParseFGX", 270 ���is_safe top ��� is_safe (ParseFGX top)���, 271 simp[is_safe_def] >> strip_tac >> 272 gen_tac >> completeInduct_on ���STRLEN s��� >> fs[PULL_FORALL] >> 273 rw[Once ParseFGX_thm] >> pop_assum mp_tac >> 274 simp[ES_CHOICE_DEF, optionTheory.option_case_eq] >> 275 simp[BIND_DEF, optionTheory.option_case_eq, token_EQ_SOME, literal_EQ_SOME, 276 pairTheory.pair_case_eq, PULL_EXISTS, UNIT_DEF] >> 277 rw[] 278 >- simp[IS_SUFFIX_APPEND_I] 279 >- (first_assum (drule_then assume_tac) >> irule IS_SUFFIX_TRANS >> 280 rename [���IS_SUFFIX s0 (ws ++ ")" ++ s)���] >> qexists_tac ���s0��� >> 281 simp[IS_SUFFIX_APPEND_I] >> metis_tac[IS_SUFFIX_APPEND_E]) 282 >- (fs[] >> rpt (irule IS_SUFFIX_APPEND_I) >> first_x_assum irule >> 283 simp[] >> metis_tac[]) 284 >- (fs[] >> rpt (irule IS_SUFFIX_APPEND_I) >> first_x_assum irule >> 285 simp[] >> metis_tac[]) 286 >- (fs[] >> rpt (irule IS_SUFFIX_APPEND_I) >> first_x_assum irule >> 287 simp[] >> metis_tac[]) 288 >- (fs[] >> rpt (irule IS_SUFFIX_APPEND_I) >> first_x_assum irule >> 289 simp[] >> metis_tac[])); 290 291val IS_SUFFIX_LENGTH = Q.store_thm( 292 "IS_SUFFIX_LENGTH", 293 ���IS_SUFFIX m n ��� LENGTH n ��� LENGTH m���, 294 metis_tac[listTheory.LENGTH_REVERSE, rich_listTheory.IS_PREFIX_LENGTH, 295 rich_listTheory.IS_SUFFIX_compute]); 296 297 298val ParseFGX_CONG = Q.store_thm("ParseFGX_CONG[defncong]", 299 ������s1 s2 t1 t2. 300 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 301 ParseFGX t1 s1 = ParseFGX t2 s2���, 302 ONCE_REWRITE_TAC [ParseFGX_def] >> rpt strip_tac >> rw[] >> 303 rename [���parseFGX _ _ s���] >> 304 ������t. STRLEN t ��� STRLEN s ��� 305 parseFGX (��a. ParseFGX t1 a) t1 t = parseFGX (��a. ParseFGX t2 a) t2 t��� 306 suffices_by metis_tac[DECIDE ���x:num ��� x���] >> gen_tac >> 307 completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >> 308 irule parseFGX_CONG >> simp[] >> rpt strip_tac >> 309 ONCE_REWRITE_TAC [ParseFGX_def] >> first_x_assum irule >> simp[]); 310 311val mksafe_cong = Q.store_thm("mksafe_cong", 312 ������n. (���s. STRLEN s < n ��� t1 s = t2 s) ��� 313 ���s. STRLEN s < n ��� mksafe t1 s = mksafe t2 s���, 314 simp[mksafe_def]); 315 316val parseU_def = Define��� 317 parseU u top = 318 do 319 f1 <- ParseFGX (mksafe top) ; 320 do 321 token (literal "U") ; 322 f2 <- u ; 323 return (F_U f1 f2) 324 od ++ return f1 325 od 326���; 327 328val parseU_CONG = Q.store_thm("parseU_CONG[defncong]", 329 ������s1 s2 t1 t2 c1 c2. 330 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 331 (���s. STRLEN s < STRLEN s1 ��� c1 s = c2 s) ��� 332 (parseU c1 t1 s1 = parseU c2 t2 s2)���, 333 rw[parseU_def, BIND_DEF] >> 334 csimp[optionTheory.option_case_eq, pairTheory.pair_case_eq] >> 335 rename [������s. STRLEN s < STRLEN s0 ��� _ s = _ s���] >> 336 ������s. STRLEN s < STRLEN s0 ��� mksafe t1 s = mksafe t2 s��� 337 by metis_tac[mksafe_cong] >> 338 ���ParseFGX (mksafe t2) s0 = ParseFGX (mksafe t1) s0��� 339 by (irule ParseFGX_CONG >> simp[]) >> 340 dsimp[] >> csimp[] >> rename [���ParseFGX (mksafe t) s = NONE���] >> 341 Cases_on ���ParseFGX (mksafe t) s��� >> simp[] >> 342 rename [���ParseFGX (mksafe t) s = SOME p���] >> 343 Cases_on ���p��� >> simp[BIND_DEF, IGNORE_BIND_DEF, ES_CHOICE_DEF] >> 344 rename [���token (literal "U") s2���] >> Cases_on ���token (literal "U") s2��� >> 345 simp[] >> rename [���token _ s2 = SOME p���] >> Cases_on ���p��� >> 346 fs[token_EQ_SOME, literal_EQ_SOME, optionTheory.option_case_eq, UNIT_DEF, 347 PULL_EXISTS, pairTheory.pair_case_eq] >> 348 rename [���c1 ss = NONE���, ���c1 _ = c2 _���, ���c1 ss = SOME (_, ws ++ "U" ++ ss)���] >> 349 Cases_on ���c1 ss��� >> simp[] 350 >- (disj1_tac >> rw[] >> 351 ���is_safe (ParseFGX (mksafe t))��� by simp[is_safe_ParseFGX] >> 352 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 353 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 354 Q.UNDISCH_THEN `c1 ss = NONE` mp_tac >> simp[]) >> 355 ���is_safe (ParseFGX (mksafe t))��� by simp[is_safe_ParseFGX] >> 356 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 357 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 358 qpat_x_assum `c1 ss = SOME _` mp_tac >> simp[] >> 359 metis_tac[pairTheory.pair_CASES]); 360 361val ParseU_def = tDefine "ParseU" ��� 362 ParseU top s = parseU (ParseU top) top s 363��� (WF_REL_TAC ���inv_image $< (STRLEN o SND)���); 364 365val ParseU_thm = 366 ParseU_def |> SIMP_RULE (srw_ss() ++ boolSimps.ETA_ss) [parseU_def] 367 368val ParseU_CONG = Q.store_thm( 369 "ParseU_CONG[defncong]", 370 ������s1 s2 t1 t2. 371 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 372 ParseU t1 s1 = ParseU t2 s2���, 373 simp[] >> rpt strip_tac >> rename [���ParseU _ s���] >> 374 ������t. STRLEN t ��� STRLEN s ��� ParseU t1 t = ParseU t2 t��� 375 suffices_by metis_tac[DECIDE ���x:num ��� x���] >> gen_tac >> 376 completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >> 377 ONCE_REWRITE_TAC [ParseU_def] >> irule parseU_CONG >> simp[]); 378 379val is_safe_ParseU = Q.store_thm( 380 "is_safe_ParseU", 381 ���is_safe (ParseU top)���, 382 simp[is_safe_def] >> gen_tac >> completeInduct_on ���STRLEN s��� >> 383 fs[PULL_FORALL] >> 384 simp[Once ParseU_thm, BIND_DEF, optionTheory.option_case_eq, is_safe_def, 385 pairTheory.pair_CASES, PULL_EXISTS, pairTheory.FORALL_PROD, 386 ES_CHOICE_DEF, UNIT_DEF, token_EQ_SOME, literal_EQ_SOME] >> 387 rw[] 388 >- metis_tac[is_safe_def, is_safe_ParseFGX, is_safe_mksafe] >> 389 fs[pairTheory.pair_case_eq] >> rw[] >> 390 rename [���ParseFGX (mksafe top) s0 = SOME (f1, px ++ "U" ++ s2)���] >> 391 ���IS_SUFFIX s0 (px ++ "U" ++ s2)��� 392 by metis_tac[is_safe_def, is_safe_mksafe, is_safe_ParseFGX] >> 393 rename [���ParseU top s2 = SOME (f2, s3)���] >> 394 ���IS_SUFFIX s2 s3��� 395 by (first_x_assum irule >> simp[] >> fs[rich_listTheory.IS_SUFFIX_APPEND])>> 396 metis_tac[IS_SUFFIX_TRANS, IS_SUFFIX_APPEND_E]); 397 398val parseCNJ_def = Define��� 399 parseCNJ cnj top = 400 do 401 f1 <- ParseU (mksafe top) ; 402 do 403 token (literal "&") ; 404 f2 <- cnj ; 405 return (F_CONJ f1 f2) 406 od ++ return f1 407 od 408���; 409 410val parseCNJ_CONG = Q.store_thm("parseCNJ_CONG[defncong]", 411 ������s1 s2 t1 t2 c1 c2. 412 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 413 (���s. STRLEN s < STRLEN s1 ��� c1 s = c2 s) ��� 414 (parseCNJ c1 t1 s1 = parseCNJ c2 t2 s2)���, 415 rw[parseCNJ_def, BIND_DEF] >> 416 csimp[optionTheory.option_case_eq, pairTheory.pair_case_eq] >> 417 rename [������s. STRLEN s < STRLEN s0 ��� _ s = _ s���] >> 418 ������s. STRLEN s < STRLEN s0 ��� mksafe t1 s = mksafe t2 s��� 419 by metis_tac[mksafe_cong] >> 420 ���ParseU (mksafe t2) s0 = ParseU (mksafe t1) s0��� 421 by (irule ParseU_CONG >> simp[]) >> 422 dsimp[] >> csimp[] >> rename [���ParseU (mksafe t) s = NONE���] >> 423 Cases_on ���ParseU (mksafe t) s��� >> simp[] >> 424 rename [���ParseU (mksafe t) s = SOME p���] >> 425 Cases_on ���p��� >> simp[BIND_DEF, IGNORE_BIND_DEF, ES_CHOICE_DEF] >> 426 rename [���token (literal "&") s2���] >> Cases_on ���token (literal "&") s2��� >> 427 simp[] >> rename [���token _ s2 = SOME p���] >> Cases_on ���p��� >> 428 fs[token_EQ_SOME, literal_EQ_SOME, optionTheory.option_case_eq, UNIT_DEF, 429 PULL_EXISTS, pairTheory.pair_case_eq] >> 430 rename [���c1 ss = NONE���, ���c1 _ = c2 _���, ���c1 ss = SOME (_, ws ++ "&" ++ ss)���] >> 431 Cases_on ���c1 ss��� >> simp[] 432 >- (disj1_tac >> rw[] >> 433 ���is_safe (ParseU (mksafe t))��� by simp[is_safe_ParseU] >> 434 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 435 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 436 Q.UNDISCH_THEN `c1 ss = NONE` mp_tac >> simp[]) >> 437 ���is_safe (ParseU (mksafe t))��� by simp[is_safe_ParseU] >> 438 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 439 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 440 qpat_x_assum `c1 ss = SOME _` mp_tac >> simp[] >> 441 metis_tac[pairTheory.pair_CASES]); 442 443val ParseCNJ_def = tDefine "ParseCNJ" ��� 444 ParseCNJ top s = parseCNJ (ParseCNJ top) top s 445��� (WF_REL_TAC ���inv_image $< (STRLEN o SND)���) 446 447val ParseCNJ_thm = 448 ParseCNJ_def |> SIMP_RULE (srw_ss() ++ boolSimps.ETA_ss) [parseCNJ_def] 449 450val ParseCNJ_CONG = Q.store_thm( 451 "ParseCNJ_CONG[defncong]", 452 ������s1 s2 t1 t2. 453 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 454 ParseCNJ t1 s1 = ParseCNJ t2 s2���, 455 simp[] >> rpt strip_tac >> rename [���ParseCNJ _ s���] >> 456 ������t. STRLEN t ��� STRLEN s ��� ParseCNJ t1 t = ParseCNJ t2 t��� 457 suffices_by metis_tac[DECIDE ���x:num ��� x���] >> gen_tac >> 458 completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >> 459 ONCE_REWRITE_TAC [ParseCNJ_def] >> irule parseCNJ_CONG >> simp[]); 460 461val is_safe_ParseCNJ = Q.store_thm( 462 "is_safe_ParseCNJ", 463 ���is_safe (ParseCNJ top)���, 464 simp[is_safe_def] >> gen_tac >> completeInduct_on ���STRLEN s��� >> 465 fs[PULL_FORALL] >> 466 simp[Once ParseCNJ_thm, BIND_DEF, optionTheory.option_case_eq, is_safe_def, 467 pairTheory.pair_CASES, PULL_EXISTS, pairTheory.FORALL_PROD, 468 ES_CHOICE_DEF, UNIT_DEF, token_EQ_SOME, literal_EQ_SOME] >> 469 rw[] 470 >- metis_tac[is_safe_def, is_safe_ParseU, is_safe_mksafe] >> 471 fs[pairTheory.pair_case_eq] >> rw[] >> 472 rename [���ParseU (mksafe top) s0 = SOME (f1, px ++ "&" ++ s2)���] >> 473 ���IS_SUFFIX s0 (px ++ "&" ++ s2)��� 474 by metis_tac[is_safe_def, is_safe_mksafe, is_safe_ParseU] >> 475 rename [���ParseCNJ top s2 = SOME (f2, s3)���] >> 476 ���IS_SUFFIX s2 s3��� 477 by (first_x_assum irule >> simp[] >> fs[rich_listTheory.IS_SUFFIX_APPEND])>> 478 metis_tac[IS_SUFFIX_TRANS, IS_SUFFIX_APPEND_E]); 479 480val F_DISJ_def = zDefine��� 481 F_DISJ f1 f2 = F_NEG (F_CONJ (F_NEG f1) (F_NEG f2)) 482���; 483 484val parseDSJ_def = Define��� 485 parseDSJ d top = 486 do 487 f1 <- ParseCNJ (mksafe top) ; 488 do 489 token (literal "|") ; 490 f2 <- d ; 491 return (F_DISJ f1 f2) 492 od ++ return f1 493 od 494���; 495 496val parseDSJ_CONG = Q.store_thm("parseDSJ_CONG[defncong]", 497 ������s1 s2 t1 t2 d1 d2. 498 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 499 (���s. STRLEN s < STRLEN s1 ��� d1 s = d2 s) ��� 500 (parseDSJ d1 t1 s1 = parseDSJ d2 t2 s2)���, 501 rw[parseDSJ_def, BIND_DEF] >> 502 csimp[optionTheory.option_case_eq, pairTheory.pair_case_eq] >> 503 rename [������s. STRLEN s < STRLEN s0 ��� _ s = _ s���] >> 504 ������s. STRLEN s < STRLEN s0 ��� mksafe t1 s = mksafe t2 s��� 505 by metis_tac[mksafe_cong] >> 506 ���ParseCNJ (mksafe t2) s0 = ParseCNJ (mksafe t1) s0��� 507 by (irule ParseCNJ_CONG >> simp[]) >> 508 dsimp[] >> csimp[] >> rename [���ParseCNJ (mksafe t) s = NONE���] >> 509 Cases_on ���ParseCNJ (mksafe t) s��� >> simp[] >> 510 rename [���ParseCNJ (mksafe t) s = SOME p���] >> 511 Cases_on ���p��� >> simp[BIND_DEF, IGNORE_BIND_DEF, ES_CHOICE_DEF] >> 512 rename [���token (literal "|") s2���] >> Cases_on ���token (literal "|") s2��� >> 513 simp[] >> rename [���token _ s2 = SOME p���] >> Cases_on ���p��� >> 514 fs[token_EQ_SOME, literal_EQ_SOME, optionTheory.option_case_eq, UNIT_DEF, 515 PULL_EXISTS, pairTheory.pair_case_eq] >> 516 rename [���c1 ss = NONE���, ���c1 _ = c2 _���, ���c1 ss = SOME (_, ws ++ "|" ++ ss)���] >> 517 Cases_on ���c1 ss��� >> simp[] 518 >- (disj1_tac >> rw[] >> 519 ���is_safe (ParseCNJ (mksafe t))��� by simp[is_safe_ParseCNJ] >> 520 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 521 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 522 Q.UNDISCH_THEN `c1 ss = NONE` mp_tac >> simp[]) >> 523 ���is_safe (ParseCNJ (mksafe t))��� by simp[is_safe_ParseCNJ] >> 524 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 525 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 526 qpat_x_assum `c1 ss = SOME _` mp_tac >> simp[] >> 527 metis_tac[pairTheory.pair_CASES]); 528 529val ParseDSJ_def = tDefine "ParseDSJ" ��� 530 ParseDSJ top s = parseDSJ (ParseDSJ top) top s 531��� (WF_REL_TAC ���inv_image $< (STRLEN o SND)���) 532 533val ParseDSJ_thm = 534 ParseDSJ_def |> SIMP_RULE (srw_ss() ++ boolSimps.ETA_ss) [parseDSJ_def] 535 536val ParseDSJ_CONG = Q.store_thm( 537 "ParseDSJ_CONG[defncong]", 538 ������s1 s2 t1 t2. 539 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 540 ParseDSJ t1 s1 = ParseDSJ t2 s2���, 541 simp[] >> rpt strip_tac >> rename [���ParseDSJ _ s���] >> 542 ������t. STRLEN t ��� STRLEN s ��� ParseDSJ t1 t = ParseDSJ t2 t��� 543 suffices_by metis_tac[DECIDE ���x:num ��� x���] >> gen_tac >> 544 completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >> 545 ONCE_REWRITE_TAC [ParseDSJ_def] >> irule parseDSJ_CONG >> simp[]); 546 547val is_safe_ParseDSJ = Q.store_thm( 548 "is_safe_ParseDSJ", 549 ���is_safe (ParseDSJ top)���, 550 simp[is_safe_def] >> gen_tac >> completeInduct_on ���STRLEN s��� >> 551 fs[PULL_FORALL] >> 552 simp[Once ParseDSJ_thm, BIND_DEF, optionTheory.option_case_eq, is_safe_def, 553 pairTheory.pair_CASES, PULL_EXISTS, pairTheory.FORALL_PROD, 554 ES_CHOICE_DEF, UNIT_DEF, token_EQ_SOME, literal_EQ_SOME] >> 555 rw[] 556 >- metis_tac[is_safe_def, is_safe_ParseCNJ, is_safe_mksafe] >> 557 fs[pairTheory.pair_case_eq] >> rw[] >> 558 rename [���ParseCNJ (mksafe top) s0 = SOME (f1, px ++ "|" ++ s2)���] >> 559 ���IS_SUFFIX s0 (px ++ "|" ++ s2)��� 560 by metis_tac[is_safe_def, is_safe_mksafe, is_safe_ParseCNJ] >> 561 rename [���ParseDSJ top s2 = SOME (f2, s3)���] >> 562 ���IS_SUFFIX s2 s3��� 563 by (first_x_assum irule >> simp[] >> fs[rich_listTheory.IS_SUFFIX_APPEND])>> 564 metis_tac[IS_SUFFIX_TRANS, IS_SUFFIX_APPEND_E]); 565 566val F_IMP_def = zDefine��� 567 F_IMP f1 f2 = F_DISJ (F_NEG f1) f2 568���; 569 570val parseIMP_def = Define��� 571 parseIMP d top = 572 do 573 f1 <- ParseDSJ (mksafe top) ; 574 do 575 token (literal "->") ; 576 f2 <- d ; 577 return (F_IMP f1 f2) 578 od ++ return f1 579 od 580���; 581 582val parseIMP_CONG = Q.store_thm("parseIMP_CONG[defncong]", 583 ������s1 s2 t1 t2 d1 d2. 584 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 585 (���s. STRLEN s < STRLEN s1 ��� d1 s = d2 s) ��� 586 (parseIMP d1 t1 s1 = parseIMP d2 t2 s2)���, 587 rw[parseIMP_def, BIND_DEF] >> 588 csimp[optionTheory.option_case_eq, pairTheory.pair_case_eq] >> 589 rename [������s. STRLEN s < STRLEN s0 ��� _ s = _ s���] >> 590 ������s. STRLEN s < STRLEN s0 ��� mksafe t1 s = mksafe t2 s��� 591 by metis_tac[mksafe_cong] >> 592 ���ParseDSJ (mksafe t2) s0 = ParseDSJ (mksafe t1) s0��� 593 by (irule ParseDSJ_CONG >> simp[]) >> 594 dsimp[] >> csimp[] >> rename [���ParseDSJ (mksafe t) s = NONE���] >> 595 Cases_on ���ParseDSJ (mksafe t) s��� >> simp[] >> 596 rename [���ParseDSJ (mksafe t) s = SOME p���] >> 597 Cases_on ���p��� >> simp[BIND_DEF, IGNORE_BIND_DEF, ES_CHOICE_DEF] >> 598 rename [���token (literal "->") s2���] >> Cases_on ���token (literal "->") s2��� >> 599 simp[] >> rename [���token _ s2 = SOME p���] >> Cases_on ���p��� >> 600 fs[token_EQ_SOME, literal_EQ_SOME, optionTheory.option_case_eq, UNIT_DEF, 601 PULL_EXISTS, pairTheory.pair_case_eq] >> 602 rename [���c1 ss = NONE���, ���c1 _ = c2 _���, ���c1 ss = SOME (_, ws ++ "->" ++ ss)���] >> 603 Cases_on ���c1 ss��� >> simp[] 604 >- (disj1_tac >> rw[] >> 605 ���is_safe (ParseDSJ (mksafe t))��� by simp[is_safe_ParseDSJ] >> 606 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 607 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 608 Q.UNDISCH_THEN `c1 ss = NONE` mp_tac >> simp[]) >> 609 ���is_safe (ParseDSJ (mksafe t))��� by simp[is_safe_ParseDSJ] >> 610 fs[is_safe_def] >> pop_assum drule >> strip_tac >> 611 drule IS_SUFFIX_LENGTH >> simp[] >> strip_tac >> 612 qpat_x_assum `c1 ss = SOME _` mp_tac >> simp[] >> 613 metis_tac[pairTheory.pair_CASES]); 614 615val ParseIMP_def = tDefine "ParseIMP" ��� 616 ParseIMP top s = parseIMP (ParseIMP top) top s 617��� (WF_REL_TAC ���inv_image $< (STRLEN o SND)���) 618 619val ParseIMP_thm = 620 ParseIMP_def |> SIMP_RULE (srw_ss() ++ boolSimps.ETA_ss) [parseIMP_def] 621 622val ParseIMP_CONG = Q.store_thm( 623 "ParseIMP_CONG[defncong]", 624 ������s1 s2 t1 t2. 625 (s1 = s2) ��� (���s. STRLEN s < STRLEN s1 ��� t1 s = t2 s) ��� 626 ParseIMP t1 s1 = ParseIMP t2 s2���, 627 simp[] >> rpt strip_tac >> rename [���ParseIMP _ s���] >> 628 ������t. STRLEN t ��� STRLEN s ��� ParseIMP t1 t = ParseIMP t2 t��� 629 suffices_by metis_tac[DECIDE ���x:num ��� x���] >> gen_tac >> 630 completeInduct_on ���STRLEN t��� >> fs[PULL_FORALL] >> rw[] >> 631 ONCE_REWRITE_TAC [ParseIMP_def] >> irule parseIMP_CONG >> simp[]); 632 633val is_safe_ParseIMP = Q.store_thm( 634 "is_safe_ParseIMP", 635 ���is_safe (ParseIMP top)���, 636 simp[is_safe_def] >> gen_tac >> completeInduct_on ���STRLEN s��� >> 637 fs[PULL_FORALL] >> 638 simp[Once ParseIMP_thm, BIND_DEF, optionTheory.option_case_eq, is_safe_def, 639 pairTheory.pair_CASES, PULL_EXISTS, pairTheory.FORALL_PROD, 640 ES_CHOICE_DEF, UNIT_DEF, token_EQ_SOME, literal_EQ_SOME] >> 641 rw[] 642 >- metis_tac[is_safe_def, is_safe_ParseDSJ, is_safe_mksafe] >> 643 fs[pairTheory.pair_case_eq] >> rw[] >> 644 rename [���ParseDSJ (mksafe top) s0 = SOME (f1, px ++ "->" ++ s2)���] >> 645 ���IS_SUFFIX s0 (px ++ "->" ++ s2)��� 646 by metis_tac[is_safe_def, is_safe_mksafe, is_safe_ParseDSJ] >> 647 rename [���ParseIMP top s2 = SOME (f2, s3)���] >> 648 ���IS_SUFFIX s2 s3��� 649 by (first_x_assum irule >> simp[] >> fs[rich_listTheory.IS_SUFFIX_APPEND])>> 650 metis_tac[IS_SUFFIX_TRANS, IS_SUFFIX_APPEND_E]); 651 652 653val Parse_def = tDefine "Parse" ���Parse s = ParseIMP Parse s��� 654 (WF_REL_TAC ���inv_image $< STRLEN���) 655 656val is_safe_Parse = Q.store_thm( 657 "is_safe_Parse", 658 ���is_safe Parse���, 659 simp[is_safe_def, Once Parse_def] >> simp[GSYM is_safe_def] >> 660 simp_tac (srw_ss() ++ boolSimps.ETA_ss) [is_safe_ParseIMP]); 661 662val Parse_thm = save_thm( 663 "Parse_thm", 664 Parse_def 665 |> SIMP_RULE (srw_ss() ++ boolSimps.ETA_ss) 666 [ParseIMP_thm, is_safe_mksafe_id, is_safe_Parse]); 667 668val eg1 = time EVAL ���Parse "pp & Gq -> pp U X(x|!y|z)"���; 669 670val _ = export_theory(); 671