1(* Define a small-step semantics for the deterministic FOR language, prove it 2 * equivalent to the functional big-step *) 3 4open HolKernel Parse boolLib bossLib; 5open optionTheory pairTheory pred_setTheory finite_mapTheory stringTheory; 6open integerTheory listTheory optionTheory rich_listTheory; 7open BasicProvers; 8open forTheory determSemTheory simple_traceTheory; 9open relationTheory 10 11val _ = new_theory "forSmall"; 12 13val _ = temp_tight_equality (); 14 15val ect = BasicProvers.EVERY_CASE_TAC; 16 17val some_no_choice = Q.prove ( 18`!f. (some x. f x) = NONE ��� ��?x. f x`, 19 rw [some_def]); 20 21(* A small step semantics for the deterministic FOR language *) 22 23(* Add a Handle statement that will stop breaks from propagating *) 24val _ = Datatype ` 25small_t = 26 | Dec string small_t 27 | Exp e 28 | Break 29 | Seq small_t small_t 30 | If e small_t small_t 31 | For e e small_t 32 | Handle small_t`; 33 34val t_to_small_t_def = Define ` 35(t_to_small_t ((Dec string t):t) = ((Dec string (t_to_small_t t)) : small_t)) ��� 36(t_to_small_t (Exp e) = Exp e) ��� 37(t_to_small_t Break = Break) ��� 38(t_to_small_t (Seq t1 t2) = Seq (t_to_small_t t1) (t_to_small_t t2)) ��� 39(t_to_small_t (If e t1 t2) = If e (t_to_small_t t1) (t_to_small_t t2)) ��� 40(t_to_small_t (For e1 e2 t) = For e1 e2 (t_to_small_t t))`; 41 42val is_val_e_def = Define ` 43(is_val_e (Num n) = T) ��� 44(is_val_e _ = F)`; 45 46val (step_e_rules, step_e_ind, step_e_cases) = Hol_reln ` 47(!s x n. 48 FLOOKUP s x = SOME n 49 ��� 50 step_e (s, Var x) (s, Num n)) ��� 51(!s n1 n2. 52 step_e (s, Add (Num n1) (Num n2)) (s, Num (n1 + n2))) ��� 53(!s s2 e1 e2 e3. 54 is_val_e e1 ��� 55 step_e (s, e2) (s2, e3) 56 ��� 57 step_e (s, Add e1 e2) (s2, Add e1 e3)) ��� 58(!s s2 e1 e2 e3. 59 step_e (s, e1) (s2, e3) 60 ��� 61 step_e (s, Add e1 e2) (s2, Add e3 e2)) ��� 62(!s x n. 63 step_e (s, Assign x (Num n)) (s |+ (x, n), Num n)) ��� 64(!s s2 x e1 e2. 65 step_e (s, e1) (s2, e2) 66 ��� 67 step_e (s, Assign x e1) (s2, Assign x e2))`; 68 69val is_val_t_def = Define ` 70(is_val_t (Exp e) = is_val_e e) ��� 71(is_val_t Break = T) ��� 72(is_val_t _ = F)`; 73 74val (step_t_rules, step_t_ind, step_t_cases) = Hol_reln ` 75(!s t x. 76 step_t (s, Dec x t) (s |+ (x, 0), t)) ��� 77(!s s2 e e2. 78 step_e (s, e) (s2, e2) 79 ��� 80 step_t (s, Exp e) (s2, Exp e2)) ��� 81(!s s2 t1 t2 t1'. 82 step_t (s, t1) (s2, t1') 83 ��� 84 step_t (s, Seq t1 t2) (s2, Seq t1' t2)) ��� 85(!s t. 86 step_t (s, Seq Break t) (s, Break)) ��� 87(!s n t. 88 step_t (s, Seq (Exp (Num n)) t) (s, t)) ��� 89(!s s2 e t1 t2 e2. 90 step_e (s, e) (s2,e2) 91 ��� 92 step_t (s, If e t1 t2) (s2, If e2 t1 t2)) ��� 93(!s t1 t2. 94 step_t (s, If (Num 0) t1 t2) (s, t2)) ��� 95(!s n t1 t2. 96 n ��� 0 97 ��� 98 step_t (s, If (Num n) t1 t2) (s, t1)) ��� 99(!s. 100 step_t (s, Handle Break) (s, Exp (Num 0))) ��� 101(!s t. 102 is_val_t t ��� 103 t ��� Break 104 ��� 105 step_t (s, Handle t) (s, t)) ��� 106(!s1 s2 t1 t2. 107 step_t (s1, t1) (s2, t2) 108 ��� 109 step_t (s1, Handle t1) (s2, Handle t2)) ��� 110(!s e1 e2 t. 111 step_t (s, For e1 e2 t) (s, Handle (If e1 (Seq t (Seq (Exp e2) (For e1 e2 t))) (Exp (Num 0)))))`; 112 113val small_diverges_def = Define ` 114small_diverges t = 115 ���s1 t1. step_t^* (FEMPTY, t) (s1, t1) ��� ?s2 t2. step_t (s1, t1) (s2, t2)`; 116 117val semantics_small_def = Define ` 118semantics_small t = 119 let t = t_to_small_t t in 120 case some s. step_t^* (FEMPTY, t) s ��� ��?s2 t2. step_t s (s2, t2) of 121 | NONE => Diverge 122 | SOME (s1, t1) => 123 case t1 of 124 | Exp e => if is_val_e e then Terminate else Crash 125 | _ => Crash`; 126 127(* ----------- Connect to functional big step -------------- *) 128 129val for_unload_def = Define ` 130 for_unload st = 131 case SND st of 132 | Break => NONE 133 | Exp (Num n) => SOME n`; 134 135val for_small_sem_def = Define ` 136 for_small_sem = 137 <| step := (\st. some st'. step_t st st'); 138 is_value := (\st. is_val_t (SND st)); 139 load := (\t. (FEMPTY, t_to_small_t t)); 140 unload := for_unload |>`; 141 142val for_eval_def = Define ` 143 for_eval st env t = 144 case sem_t st t of 145 (Rval v, s) => (s, Val (SOME v)) 146 | (Rbreak, s) => (s, Val NONE) 147 | (Rtimeout, s) => (s, Timeout) 148 | (Rfail, s) => (s, Error)`; 149 150val for_big_sem_def = Define ` 151 for_big_sem = 152 <| eval := for_eval; 153 init_st := <| clock := 0; store := FEMPTY |>; 154 init_env := (); 155 get_clock := (\x. x.clock); 156 set_clock := (\c st. st with clock := c); 157 unload := I |>`; 158 159val (res_rel_t_rules, res_rel_t_ind, res_rel_t_cases) = Hol_reln ` 160(!i s. 161 res_rel_t (Rval i, s) (s.store, Exp (Num i))) ��� 162(!s t. 163 (~?s' t'. step_t (s.store, t) (s', t')) ��� 164 ~is_val_t t 165 ��� 166 res_rel_t (Rfail, s) (s.store, t)) ��� 167(!s. 168 res_rel_t (Rbreak, s) (s.store, Break)) ��� 169(!s t. 170 (?s' t'. step_t (s.store, t) (s', t')) ��� 171 s.clock = 0 172 ��� 173 res_rel_t (Rtimeout, s) (s.store, t))`; 174 175val (res_rel_e_rules, res_rel_e_ind, res_rel_e_cases) = Hol_reln ` 176(!i s. 177 res_rel_e (Rval i, s) (s.store, Num i)) ��� 178(!s e. 179 (~?s' e'. step_e (s.store, e) (s', e')) ��� 180 ~is_val_e e 181 ��� 182 res_rel_e (Rfail, s) (s.store, e))` 183 184val _ = set_trace "Goalstack.print_goal_at_top" 0; 185 186val step_t_strongind = (fetch "-" "step_t_strongind") 187val step_e_strongind = (fetch "-" "step_e_strongind") 188 189val etac = (fs[Once step_t_cases]>>fs[Once step_t_cases,Once step_e_cases]) 190 191(* Determinism of the small step relation *) 192val step_e_determ = Q.prove( 193` ���se se1. 194 step_e se se1 ��� 195 (���se2. 196 step_e se se2 ��� se1 = se2)`, 197 ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD] 198 >- 199 (fs[Once step_e_cases]>>rfs[]) 200 >- 201 ntac 2(fs[Once step_e_cases]>>rfs[]) 202 >- 203 (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[] 204 >- 205 fs[is_val_e_def,Once step_e_cases] 206 >- 207 metis_tac[] 208 >- 209 (Cases_on`e1`>>fs[is_val_e_def,Once step_e_cases])) 210 >- 211 (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[] 212 >- 213 fs[Once step_e_cases] 214 >- 215 (Cases_on`e1`>>fs[is_val_e_def,Once step_e_cases]) 216 >- 217 metis_tac[]) 218 >- 219 ntac 2 (fs[Once step_e_cases]) 220 >- 221 (pop_assum mp_tac >> simp[Once step_e_cases]>>rw[] 222 >- 223 fs[Once step_e_cases] 224 >- 225 metis_tac[])) 226 227val step_t_determ = Q.prove( 228` ���st st1. 229 step_t st st1 ��� 230 (���st2. 231 step_t st st2 ��� st1 = st2)`, 232 ho_match_mp_tac step_t_strongind >>rw[] 233 >- etac 234 >- 235 (fs[Once step_t_cases]>> 236 imp_res_tac step_e_determ>> 237 fs[]) 238 >- 239 (pop_assum mp_tac>> 240 simp[Once step_t_cases]>>fs[FORALL_PROD]>>rw[] 241 >- 242 metis_tac[] 243 >- 244 fs[Once step_t_cases] 245 >- 246 fs[Once step_t_cases,Once step_e_cases]) 247 >- etac 248 >- etac 249 >- 250 (fs[Once step_t_cases] 251 >- 252 (imp_res_tac step_e_determ>>fs[]) 253 >> etac) 254 >- etac 255 >- etac 256 >- etac 257 >- 258 (fs[Once step_t_cases]>>rfs[]>> 259 Cases_on`t`>>fs[is_val_t_def]>> 260 Cases_on`e`>>fs[is_val_e_def]>> 261 fs[Once step_t_cases]>> 262 fs[Once step_e_cases]) 263 >- 264 (pop_assum mp_tac>> 265 simp[Once step_t_cases]>>rw[] 266 >- 267 etac 268 >- 269 (Cases_on`t1`>>fs[is_val_t_def]>>Cases_on`e`>>fs[is_val_e_def]>> 270 fs[Once step_t_cases,Once step_e_cases]) 271 >> 272 fs[FORALL_PROD]>>metis_tac[]) 273 >> 274 fs[Once step_t_cases]) 275 276val step_t_select_unique = Q.prove( 277`step_t (q,r) st' ��� 278 (@st'. step_t (q,r) st') = st'`, 279 rw[]>> 280 metis_tac[step_t_determ]) 281 282val some_to_SOME_step_e = Q.prove( 283`step_e A B ��� 284 (some st'. step_e A st') = 285 SOME B`, 286 rw[]>>fs[some_def]>> 287 metis_tac[step_e_determ]) |> GEN_ALL 288 289val some_to_SOME_step_t = Q.prove( 290`step_t A B ��� 291 (some st'. step_t A st') = 292 SOME B`, 293 rw[]>>fs[some_def]>>metis_tac[step_t_determ]) |>GEN_ALL 294 295(* Contextual transitions of the small step semantics *) 296val check_trace_seq = Q.prove( 297`���tr. 298 check_trace (��st. some st'. step_t st st') tr ��� 299 check_trace (��st. some st'. step_t st st') (MAP (��st,t. (st,Seq t p)) tr)`, 300 Induct>>rw[]>> 301 Cases_on`tr`>>fs[check_trace_def]>> 302 Cases_on`h`>>Cases_on`h'`>> 303 match_mp_tac some_to_SOME_step_t>> 304 fs[some_def]>> 305 simp[Once step_t_cases]>> 306 metis_tac[step_t_select_unique]) 307 308val check_trace_assign = Q.prove( 309`���tr. 310 check_trace (��st. some st'. step_e st st') tr ��� 311 check_trace (��st. some st'. step_e st st') (MAP (��st,e. (st,Assign s e)) tr)`, 312 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 313 Cases_on`h`>>Cases_on`h'`>> 314 match_mp_tac some_to_SOME_step_e>> 315 fs[some_def]>> 316 simp[Once step_e_cases]>> 317 metis_tac[step_e_determ]) 318 319val check_trace_add1 = Q.prove( 320`���tr. 321 check_trace (��st. some st'. step_e st st') tr ��� 322 check_trace (��st. some st'. step_e st st') (MAP (��st,e. (st,Add e e')) tr)`, 323 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 324 Cases_on`h`>>Cases_on`h'`>> 325 match_mp_tac some_to_SOME_step_e>> 326 fs[some_def]>> 327 simp[Once step_e_cases]>> 328 metis_tac[step_e_determ]) 329 330val check_trace_add2 = Q.prove( 331`���tr. 332 check_trace (��st. some st'. step_e st st') tr ��� 333 check_trace (��st. some st'. step_e st st') (MAP (��st,e'. (st,Add (Num i) e')) tr)`, 334 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 335 Cases_on`h`>>Cases_on`h'`>> 336 match_mp_tac some_to_SOME_step_e>> 337 fs[some_def]>> 338 simp[Once step_e_cases]>> 339 metis_tac[step_e_determ,is_val_e_def]) 340 341val check_trace_exp = Q.prove( 342`���tr. 343 check_trace (��st. some st'. step_e st st') tr ��� 344 check_trace (��st. some st'. step_t st st') (MAP (��st,e'. (st,Exp e')) tr)`, 345 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 346 Cases_on`h`>>Cases_on`h'`>> 347 match_mp_tac some_to_SOME_step_t>> 348 fs[some_def]>> 349 simp[Once step_t_cases]>> 350 metis_tac[step_e_determ]) 351 352val check_trace_if1 = Q.prove( 353`���tr. 354 check_trace (��st. some st'. step_e st st') tr ��� 355 check_trace (��st. some st'. step_t st st') (MAP (��st,e'. (st,If e' a b)) tr)`, 356 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 357 Cases_on`h`>>Cases_on`h'`>> 358 match_mp_tac some_to_SOME_step_t>> 359 fs[some_def]>> 360 simp[Once step_t_cases]>> 361 metis_tac[step_e_determ]) 362 363val check_trace_for1 = Q.prove( 364`���tr. 365 check_trace (��st. some st'. step_e st st') tr ��� 366 check_trace (��st. some st'. step_t st st') 367 (MAP (��st,e'. (st, 368 Handle (If e' a b))) tr)`, 369 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 370 Cases_on`h`>>Cases_on`h'`>> 371 match_mp_tac some_to_SOME_step_t>> 372 fs[some_def]>> 373 simp[Once step_t_cases]>> 374 simp[Once step_t_cases]>> 375 metis_tac[step_e_determ]) 376 377val check_trace_for2 = Q.prove( 378`���tr. 379 check_trace (��st. some st'. step_t st st') tr ��� 380 check_trace (��st. some st'. step_t st st') 381 (MAP (��st,t'. (st, 382 Handle (Seq t' a))) tr)`, 383 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 384 Cases_on`h`>>Cases_on`h'`>> 385 match_mp_tac some_to_SOME_step_t>> 386 fs[some_def]>> 387 simp[Once step_t_cases]>> 388 simp[Once step_t_cases]>> 389 metis_tac[step_e_determ]) 390 391val check_trace_for3 = Q.prove( 392`���tr. 393 check_trace (��st. some st'. step_e st st') tr ��� 394 check_trace (��st. some st'. step_t st st') 395 (MAP (��st,e'. (st, 396 Handle (Seq (Exp e') a))) tr)`, 397 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 398 Cases_on`h`>>Cases_on`h'`>> 399 match_mp_tac some_to_SOME_step_t>> 400 fs[some_def]>> 401 ntac 3 (simp[Once step_t_cases])>> 402 metis_tac[step_e_determ]) 403 404val check_trace_handle = Q.prove( 405`���tr. 406 check_trace (��st. some st'. step_t st st') tr ��� 407 check_trace (��st. some st'. step_t st st') 408 (MAP (��st,t'. (st, 409 Handle t')) tr)`, 410 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 411 Cases_on`h`>>Cases_on`h'`>> 412 match_mp_tac some_to_SOME_step_t>> 413 fs[some_def]>> 414 simp[Once step_t_cases]>> 415 Cases_on`st'`>>metis_tac[step_t_determ]) 416 417(* Non-existence of contextual transitions in small-step *) 418val no_step_e_assign = Q.prove( 419`���e. 420 (���s' e'. ��step_e (s,e) (s',e')) ��� 421 ��is_val_e e 422 ��� 423 ���s' e'. ��step_e (s,Assign v e) (s',e')`, 424 Induct>>rw[is_val_e_def]>> 425 simp[Once step_e_cases]) 426 427val no_step_e_add1 = Q.prove( 428`���e. 429 (���s' e'. ��step_e (s,e) (s',e')) ��� 430 ��is_val_e e 431 ��� 432 ���s' e'. ��step_e (s,Add e e'') (s',e')`, 433 Induct>>rw[is_val_e_def]>>simp[Once step_e_cases,is_val_e_def]) 434 435val no_step_e_add2 = Q.prove( 436`���e. 437 (���s' e'. ��step_e (s,e) (s',e')) ��� 438 ��is_val_e e 439 ��� 440 ���s' e'. ��step_e (s,Add (Num i) e) (s',e')`, 441 Induct>>rw[is_val_e_def]>> 442 rpt (simp[Once step_e_cases])) 443 444val no_step_t_exp = Q.prove( 445`���e. 446 (���s' e'. ��step_e (s,e) (s',e')) ��� 447 ��is_val_e e 448 ��� 449 ���s' t'. ��step_t (s,Exp e) (s',t')`, 450 Induct>>rw[is_val_e_def]>> 451 simp[Once step_t_cases]) 452 453val no_step_t_seq = Q.prove( 454`���t. 455 (���s' t'. ��step_t (s,t) (s',t')) ��� 456 ��is_val_t t 457 ��� 458 ���s' t'. ��step_t (s,Seq t p) (s',t')`, 459 Induct>>rw[is_val_t_def]>> 460 simp[Once step_t_cases]>> 461 Cases_on`e`>>fs[is_val_e_def]) 462 463val no_step_t_if1 = Q.prove( 464`���e. 465 (���s' e'. ��step_e (s,e) (s',e')) ��� 466 ��is_val_e e 467 ��� 468 ���s' t'. ��step_t (s,If e a b) (s',t')`, 469 Induct>>rw[is_val_e_def]>> 470 simp[Once step_t_cases]) 471 472val no_step_t_handle = Q.prove( 473`���t. 474 (���s' t'. ��step_t (s,t) (s',t')) ��� 475 ��is_val_t t 476 ��� 477 ���s' t'. ��step_t (s,Handle t) (s',t')`, 478 Induct>>rw[is_val_t_def]>> 479 simp[Once step_t_cases,is_val_t_def]) 480 481val LAST_MAP = Q.prove( 482`���ls. ls ��� [] ��� LAST (MAP f ls) = f (LAST ls)`, 483 Induct>>fs[LAST_DEF]>>rw[]) 484 485val HD_MAP = Q.prove( 486`���ls. ls ��� [] ��� HD(MAP f ls) = f (HD ls)`, 487 Induct>>rw[]) 488 489val HD_APPEND = Q.prove( 490`ls ��� [] ��� HD (ls ++ ls') = HD ls`, 491Cases_on`ls`>>fs[]) 492 493val LAST_APPEND = Q.prove( 494`ls' ��� [] ��� LAST (ls ++ ls') = LAST ls'`, 495Cases_on`ls'`>>fs[]) 496 497val sem_e_not_timeout = Q.prove ( 498`!st e r. sem_e st e ��� (Rtimeout, r)`, 499 Induct_on `e` >> 500 rw [sem_e_def] >> 501 ect >> 502 fs [] >> 503 metis_tac []); 504 505val sem_e_not_break = Q.prove( 506`!st e r. sem_e st e ��� (Rbreak,r)`, 507 Induct_on`e`>>rw[sem_e_def]>> 508 ect>> 509 fs[]>>metis_tac[]); 510 511val LAST_HD_eq = Q.prove(` 512���ls ls'. 513 ls ��� [] ��� ls' ��� [] ��� 514 LAST ls = HD ls' ��� 515 BUTLASTN 1 ls ++ ls' = 516 ls ++ TL ls'`, 517 Induct>>fs[LAST_DEF,BUTLASTN_1]>>rw[]>> 518 Cases_on`ls'`>>fs[FRONT_DEF]) 519 520(* Start connecting functional big step to small step traces *) 521val sem_e_big_small_lem = Q.prove( 522`!s e r. 523 sem_e s e = r 524 ��� 525 ?tr. 526 tr ��� [] ��� 527 check_trace (\st. some st'. step_e st st') tr ��� 528 HD tr = (s.store, e) ��� 529 res_rel_e r (LAST tr)`, 530 Induct_on`e`>>rw[]>>fs[sem_e_def] 531 >- 532 (FULL_CASE_TAC>>fs[res_rel_e_cases] 533 >- 534 (qexists_tac`[(s'.store,Var s)]`>>fs[check_trace_def,is_val_e_def]>> 535 simp[Once step_e_cases]) 536 >- 537 (qexists_tac`[(s'.store,Var s);(s'.store,Num x)]`>> 538 fs[check_trace_def,some_def]>> 539 ntac 2 (simp[Once step_e_cases]))) 540 >- 541 (fs[res_rel_e_cases]>> 542 qexists_tac`[s.store,Num i]`>>fs[check_trace_def]) 543 >- 544 (ntac 2 FULL_CASE_TAC>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout] 545 >- 546 (FULL_CASE_TAC>>fs[sem_e_not_break,sem_e_not_timeout]>> 547 last_x_assum(qspec_then`s` assume_tac)>>rfs[]>> 548 last_x_assum(qspec_then`r` assume_tac)>>rfs[]>> 549 qabbrev_tac`ls1 = (MAP (��st,e. (st,Add e e')) tr)`>> 550 qabbrev_tac`ls2 = (MAP (��st,e'. (st,Add (Num i) e')) tr')`>> 551 qabbrev_tac`ls = BUTLASTN 1 ls1 ++ ls2`>> 552 fs[res_rel_e_cases]>> 553 `LAST ls1 = HD ls2` by 554 (unabbrev_all_tac>>fs[LAST_MAP,HD_MAP])>> 555 `ls = ls1 ++ (TL ls2)` by 556 (unabbrev_all_tac>> 557 fs[LAST_HD_eq]) 558 >- 559 (qexists_tac`ls ++ [(r'.store,Num(i+i'))]`>>reverse (rw[]) 560 >- 561 fs[Abbr`ls1`,HD_MAP,HD_APPEND] 562 >> 563 match_mp_tac check_trace_append2>>fs[check_trace_def]>>rw[] 564 >- 565 (`check_trace (��st. some st'. step_e st st') ls2` by 566 fs[check_trace_add2,Abbr`ls2`]>> 567 Cases_on`ls2`>>fs[]>>Cases_on`t`>>fs[] 568 >- 569 metis_tac[check_trace_add1] 570 >> 571 match_mp_tac check_trace_append2>>fs[check_trace_def]>>rw[]>> 572 fs[Abbr`ls1`]>>metis_tac[check_trace_add1]) 573 >- 574 (qsuff_tac `LAST (ls1 ++ TL ls2) = LAST ls2` 575 >- 576 (fs[Abbr`ls2`,LAST_APPEND,LAST_MAP]>>rw[]>> 577 `step_e (r'.store,Add (Num i) (Num i')) (r'.store,Num (i+i'))` by 578 simp[Once step_e_cases]>> 579 fs[some_def]>> 580 metis_tac[step_e_determ]) 581 >> 582 rfs[markerTheory.Abbrev_def,LAST_APPEND])) 583 >> 584 qexists_tac`ls`>>rw[] 585 >- 586 (unabbrev_all_tac>>fs[]) 587 >- 588 (`check_trace (��st. some st'. step_e st st') ls2` by 589 fs[check_trace_add2,Abbr`ls2`]>> 590 Cases_on`ls2`>>fs[]>>Cases_on`t`>>fs[] 591 >- 592 metis_tac[check_trace_add1] 593 >> 594 match_mp_tac check_trace_append2>>fs[check_trace_def]>>rw[]>> 595 metis_tac[check_trace_add1]) 596 >- 597 fs[HD_APPEND,Abbr`ls1`,HD_MAP] 598 >> 599 unabbrev_all_tac>> 600 fs[HD_MAP,HD_APPEND,LAST_APPEND,LAST_MAP,is_val_e_def]>> 601 fs[no_step_e_add2]) 602 >> 603 last_x_assum(qspec_then`s` assume_tac)>>rfs[]>> 604 qexists_tac`(MAP (��st,e. (st,Add e e')) tr)`>> 605 fs[HD_MAP,res_rel_e_cases,LAST_MAP,is_val_e_def,check_trace_add1,no_step_e_add1]) 606 >- 607 (EVERY_CASE_TAC>>fs[res_rel_e_cases,sem_e_not_break,sem_e_not_timeout]>> 608 first_x_assum(qspec_then`s'` assume_tac)>>rfs[] 609 >- 610 (qexists_tac`(MAP (��st,e. (st,Assign s e)) tr)++[(store_var s i r).store,Num i]`>>fs[HD_MAP,HD_APPEND]>> 611 ho_match_mp_tac check_trace_append2>> 612 fs[check_trace_def,LAST_MAP,check_trace_assign]>> 613 ntac 2 (simp[Once step_e_cases,store_var_def])) 614 >> 615 (qexists_tac`(MAP (��st,e. (st,Assign s e)) tr)`>> 616 fs[HD_MAP,LAST_MAP,is_val_e_def,no_step_e_assign,check_trace_assign]))) 617 618val sem_t_for_no_break = Q.prove( 619 `���s s'. sem_t s (For e1 e2 t) ��� (Rbreak,s')`, 620 completeInduct_on`s.clock`>>fs[sem_t_def_with_stop]>> 621 rw[]>>FULL_CASE_TAC>>Cases_on`q`>> 622 fs[sem_e_not_break,sem_e_not_timeout]>> 623 IF_CASES_TAC>>fs[]>> 624 FULL_CASE_TAC>>Cases_on`q`>>fs[]>> 625 FULL_CASE_TAC>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout]>> 626 imp_res_tac sem_e_clock>>imp_res_tac sem_t_clock>>fs[]>> 627 IF_CASES_TAC>>fs[dec_clock_def]>> 628 simp[STOP_def]>> 629 simp[sem_t_def_with_stop]>> 630 fs[PULL_FORALL]>> 631 first_x_assum(qspec_then `r'' with clock := r''.clock-1` mp_tac)>> 632 fs[]>> 633 `r''.clock < 1 + r.clock ��� 0 < r.clock` by 634 DECIDE_TAC>> 635 fs[dec_clock_def]) 636 637val big_small_lem = Q.store_thm ("big_small_lem", 638`!s t r. 639 sem_t s t = r 640 ��� 641 ?tr. 642 tr ��� [] ��� 643 s.clock - (SND r).clock ��� LENGTH tr ��� 644 check_trace (\st. some st'. step_t st st') tr ��� 645 HD tr = (s.store, (t_to_small_t t)) ��� 646 res_rel_t r (LAST tr)`, 647 648 ho_match_mp_tac sem_t_ind >> 649 rw [sem_t_def_with_stop, t_to_small_t_def] 650 >- ( 651 qabbrev_tac`r = sem_e s e`>>fs[markerTheory.Abbrev_def]>> 652 pop_assum (assume_tac o SYM)>> 653 imp_res_tac sem_e_big_small_lem>> 654 Cases_on`r`>> 655 qexists_tac`MAP (��st,e. (st,Exp e)) tr`>> 656 imp_res_tac sem_e_clock>>fs[HD_MAP,LAST_MAP]>> 657 CONJ_TAC >- fs[check_trace_exp] >> 658 fs[res_rel_t_cases,res_rel_e_cases,no_step_t_exp,is_val_t_def] 659 ) 660 >- ( 661 qpat_abbrev_tac`A = (s.store,B)`>> 662 fs[store_var_def]>> 663 qexists_tac`A::tr`>>fs[Abbr`A`,check_trace_def]>> 664 TRY (CONJ_TAC >- DECIDE_TAC) >> 665 reverse (CONJ_TAC) >- fs[LAST_DEF] >> 666 Cases_on`tr`>> 667 simp[check_trace_def,optionTheory.some_def]>> 668 ntac 2 (simp[Once step_t_cases])>> 669 fs[] 670 ) 671 >- ( 672 qexists_tac`[s.store,Break]`>>fs[res_rel_t_cases,check_trace_def] 673 ) 674 >- ( 675 EVERY_CASE_TAC>>fs[] 676 >- ( 677 qpat_abbrev_tac`p = t_to_small_t t'`>> 678 qexists_tac`MAP (��st,t. (st,Seq t p)) tr ++ tr'`>> 679 fs[HD_MAP,HD_APPEND,LAST_APPEND]>>rw[] >> 680 TRY (DECIDE_TAC) 681 >- ( 682 match_mp_tac check_trace_append2>> 683 fs[check_trace_seq,LAST_MAP]>> 684 Cases_on`LAST tr`>>fs[]>> 685 `step_t (q,Seq r' p) (q,p)` by ( 686 simp[Once step_t_cases]>> 687 fs[res_rel_t_cases])>> 688 `q = r.store` by fs[res_rel_t_cases]>> 689 fs[some_def]>> 690 metis_tac[step_t_select_unique] 691 ) 692 ) 693 >- ( 694 qpat_abbrev_tac `p = t_to_small_t t'`>> 695 qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)++[r.store,Break]`>> 696 fs[HD_APPEND,HD_MAP]>>rw[] >> 697 TRY (DECIDE_TAC) 698 >- ( 699 match_mp_tac check_trace_append2>> 700 fs[check_trace_seq,LAST_MAP,check_trace_def]>> 701 fs[res_rel_t_cases]>> 702 `step_t (r.store, Seq Break p) (r.store,Break)` by 703 fs[Once step_t_cases]>> 704 metis_tac[step_t_select_unique,some_def] 705 ) 706 >- fs[Once res_rel_t_cases] 707 ) 708 >- ( 709 qpat_abbrev_tac `p = t_to_small_t t'`>> 710 qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)`>> 711 fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>> 712 fs[Once res_rel_t_cases,LAST_MAP]>> 713 rename1 `step_t _ (s',_)` >> 714 `step_t (r.store,Seq t'' p) (s',Seq t''' p)` by simp[Once step_t_cases]>> 715 metis_tac[] 716 ) 717 >- ( 718 qpat_abbrev_tac `p = t_to_small_t t'`>> 719 qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)`>> 720 fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>> 721 fs[Once res_rel_t_cases,LAST_MAP,is_val_t_def]>> 722 metis_tac[no_step_t_seq] 723 ) 724 ) 725 >- ( 726 EVERY_CASE_TAC>>fs[sem_e_not_break,sem_e_not_timeout]>> 727 imp_res_tac sem_e_big_small_lem>> 728 imp_res_tac sem_e_clock>> 729 qpat_abbrev_tac`p1 = t_to_small_t t1`>> 730 qpat_abbrev_tac`p2 = t_to_small_t t2` 731 >- ( 732 qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr') ++ tr`>> 733 fs[HD_MAP,HD_APPEND,LAST_MAP,LAST_APPEND]>>rw[] >> 734 TRY (DECIDE_TAC) >> 735 match_mp_tac check_trace_append2>>fs[res_rel_e_cases]>>CONJ_TAC 736 >- metis_tac[check_trace_if1] >> 737 match_mp_tac some_to_SOME_step_t>>fs[LAST_MAP]>> 738 simp[Once step_t_cases] 739 ) 740 >- ( 741 qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr') ++ tr`>> 742 fs[HD_MAP,HD_APPEND,LAST_MAP,LAST_APPEND]>>rw[] >> 743 TRY (DECIDE_TAC) >> 744 match_mp_tac check_trace_append2>>fs[res_rel_e_cases]>>CONJ_TAC 745 >- metis_tac[check_trace_if1] >> 746 match_mp_tac some_to_SOME_step_t>>fs[LAST_MAP]>> 747 simp[Once step_t_cases] 748 ) 749 >- ( 750 qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr)`>>rw[]>> 751 fs[HD_MAP,res_rel_t_cases,LAST_MAP,res_rel_e_cases,is_val_t_def]>> 752 metis_tac[check_trace_if1,no_step_t_if1] 753 ) 754 ) 755 >- ( 756 reverse ( 757 Cases_on`sem_e s e1`>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout] 758 ) >> 759 (*trace for e1*) 760 imp_res_tac sem_e_big_small_lem>> 761 imp_res_tac sem_e_clock>> 762 qpat_abbrev_tac`p = t_to_small_t t`>> 763 qabbrev_tac 764 `e1tr = (MAP (��st,e. (st,Handle 765 (If e (Seq p (Seq (Exp e2) (For e1 e2 p))) (Exp (Num 0))))) tr)`>> 766 `check_trace (��st. some st'. step_t st st') e1tr` by 767 metis_tac[check_trace_for1]>> 768 qabbrev_tac`ls = [s.store,For e1 e2 p]`>> 769 `check_trace (��st. some st'. step_t st st') (ls++e1tr)` by ( 770 match_mp_tac check_trace_append2>>unabbrev_all_tac>> 771 fs[check_trace_def,HD_MAP]>> 772 match_mp_tac some_to_SOME_step_t>> 773 simp[Once step_t_cases]) 774 >- ( 775 qexists_tac` ls ++ e1tr`>> 776 unabbrev_all_tac>>fs[res_rel_t_cases,LAST_DEF,LAST_MAP,HD_APPEND]>> 777 fs[LAST_APPEND,LAST_MAP,res_rel_e_cases,is_val_t_def]>> 778 match_mp_tac no_step_t_handle>>fs[is_val_t_def]>> 779 metis_tac[no_step_t_if1] 780 ) >> 781 IF_CASES_TAC>>fs[] 782 >- ( (*run out of time*) 783 fs[res_rel_t_cases,res_rel_e_cases]>> 784 qexists_tac` (ls ++ e1tr) 785 ++ [(r.store,Handle (Exp (Num 0)));(r.store,Exp (Num 0))]`>> 786 fs[LAST_APPEND,LAST_MAP]>>fs[]>>rw[] 787 >- ( 788 match_mp_tac check_trace_append2>>rw[] 789 >- ( 790 fs[check_trace_def]>> 791 match_mp_tac some_to_SOME_step_t>> 792 simp[Once step_t_cases,is_val_e_def,is_val_t_def] 793 ) 794 >- ( 795 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP]>> 796 match_mp_tac some_to_SOME_step_t>> 797 ntac 2 (simp[Once step_t_cases]) 798 ) 799 ) >> 800 unabbrev_all_tac>>fs[HD_APPEND] 801 ) >> 802 reverse (Cases_on`sem_t r t`>>Cases_on`q`>>fs[]) >> 803 qabbrev_tac`ttr = 804 (MAP (��st,t. (st,Handle (Seq t (Seq (Exp e2) (For e1 e2 p))) ))) tr'`>> 805 `check_trace (��st. some st'. step_t st st') ttr` by 806 metis_tac[check_trace_for2]>> 807 `check_trace (��st. some st'. step_t st st') (ls++e1tr++ttr)` by ( 808 match_mp_tac check_trace_append2>> 809 fs[]>> unabbrev_all_tac>> 810 fs[LAST_MAP,res_rel_e_cases,HD_MAP,LAST_DEF]>> 811 match_mp_tac some_to_SOME_step_t>> 812 ntac 2 (simp[Once step_t_cases]) 813 ) 814 >- ( 815 qexists_tac`ls++e1tr++ttr`>>unabbrev_all_tac>> 816 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>CONJ_TAC >> 817 TRY (DECIDE_TAC) >> 818 fs[is_val_t_def]>>match_mp_tac no_step_t_handle>> 819 fs[is_val_t_def]>>match_mp_tac no_step_t_seq>> 820 metis_tac[] 821 ) 822 >- ( 823 qexists_tac`ls++e1tr++ttr`>>unabbrev_all_tac>> 824 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>> 825 TRY (CONJ_TAC >> DECIDE_TAC) >> 826 ntac 2 (simp[Once step_t_cases,is_val_t_def])>> 827 metis_tac[] 828 ) 829 >- ( 830 qexists_tac 831 `ls++e1tr++ttr++[(r'.store,Handle Break);(r'.store,Exp (Num 0))]`>> 832 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>rw[]>> 833 TRY(unabbrev_all_tac>>fs[]>>DECIDE_TAC)>> 834 match_mp_tac check_trace_append2>>fs[check_trace_def]>>CONJ_TAC>> 835 match_mp_tac some_to_SOME_step_t>> 836 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>> 837 ntac 2 (simp[Once step_t_cases]) 838 ) >> 839 (* continue executing *) 840 reverse (Cases_on`sem_e r' e2`>>Cases_on`q`) >> 841 fs[sem_e_not_break,sem_e_not_timeout]>> 842 imp_res_tac sem_e_big_small_lem>> 843 imp_res_tac sem_e_clock>> 844 qabbrev_tac 845 `e2tr = (MAP (��st,e. (st,Handle (Seq (Exp e) (For e1 e2 p)) ))) tr''`>> 846 `check_trace (��st. some st'. step_t st st') e2tr` by 847 metis_tac[check_trace_for3]>> 848 `check_trace (��st. some st'. step_t st st') (ls++e1tr++ttr++e2tr)` by ( 849 match_mp_tac check_trace_append2>>fs[]>> 850 match_mp_tac some_to_SOME_step_t>> 851 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,HD_MAP,res_rel_t_cases]>> 852 ntac 2 (simp[Once step_t_cases,res_rel_e_cases]) 853 ) 854 >- ( 855 qexists_tac`ls++e1tr++ttr++e2tr`>>fs[res_rel_e_cases]>> 856 unabbrev_all_tac>> 857 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases,is_val_t_def]>>rw[] >> 858 TRY (DECIDE_TAC) >> 859 metis_tac[no_step_t_exp,no_step_t_handle, no_step_t_seq,is_val_t_def] 860 ) >> 861 (* e2 ok *) 862 reverse (IF_CASES_TAC) >>fs[] 863 >- ( (* clock ended *) 864 fs[res_rel_t_cases]>> 865 qexists_tac`ls++e1tr++ttr++e2tr`>>fs[]>>rw[]>> 866 TRY (unabbrev_all_tac>>fs[]>>DECIDE_TAC)>> 867 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,res_rel_e_cases]>> 868 ntac 2 (simp[Once step_t_cases,is_val_t_def])>> 869 metis_tac[] 870 ) >> 871 (* clock ok *) 872 simp[STOP_def]>> 873 simp[Once sem_t_def_with_stop]>> 874 fs[dec_clock_def]>> 875 (*Need a handle wrapper around rest of trace*) 876 qabbrev_tac`ftr = MAP (��st,t. (st, Handle t))tr''''` >> 877 `check_trace (��st. some st'. step_t st st') ftr` by 878 metis_tac[check_trace_handle]>> 879 `check_trace (��st. some st'. step_t st st') (ls++e1tr++ttr++e2tr++ftr)` by ( 880 match_mp_tac check_trace_append2>>fs[]>> 881 match_mp_tac some_to_SOME_step_t>> 882 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,HD_MAP]>> 883 fs[res_rel_e_cases]>> 884 ntac 2 (simp[Once step_t_cases]) 885 ) >> 886 fs[res_rel_t_cases] 887 (*Case split on the rest of loop*) 888 >- ( 889 qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr++[s'.store,Exp (Num i''')]`>> 890 fs[]>>rw[] 891 >- (unabbrev_all_tac>>fs[]>>DECIDE_TAC) 892 >- ( 893 match_mp_tac check_trace_append2>>fs[check_trace_def]>> 894 match_mp_tac some_to_SOME_step_t>>unabbrev_all_tac>> 895 fs[LAST_DEF,LAST_APPEND,LAST_MAP,res_rel_e_cases]>> 896 simp[Once step_t_cases,is_val_t_def,is_val_e_def] 897 ) 898 >- (unabbrev_all_tac>>fs[]>>DECIDE_TAC) 899 >- simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def] 900 ) 901 >- ( 902 qexists_tac`ls ++ e1tr++ttr++e2tr++ftr`>> reverse (fs[]>>rw[]) 903 >- ( 904 ntac 4 (simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def])>> 905 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,is_val_t_def]>> 906 match_mp_tac no_step_t_handle>> 907 metis_tac[] 908 ) >> 909 unabbrev_all_tac>>fs[]>>DECIDE_TAC 910 ) 911 >- ( (*break never occurs*) 912 qpat_x_assum `A = (RBreak,s')` mp_tac>> 913 FULL_CASE_TAC>> 914 Cases_on`q`>> fs[sem_e_not_timeout,sem_e_not_break]>> 915 IF_CASES_TAC>>fs[]>> 916 FULL_CASE_TAC>> 917 Cases_on`q`>> fs[sem_e_not_timeout,sem_e_not_break]>> 918 FULL_CASE_TAC>> 919 Cases_on`q`>> fs[sem_e_not_timeout,sem_e_not_break]>> 920 IF_CASES_TAC>>fs[]>> 921 simp[STOP_def]>> 922 rw[] >> fs[] >> 923 metis_tac[sem_t_for_no_break] 924 ) 925 >- ( 926 qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr`>> reverse (fs[]>>rw[]) >> 927 unabbrev_all_tac 928 >- ( 929 ntac 3 ( 930 simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def,LAST_MAP])>> 931 simp[Once step_t_cases]>>metis_tac[] 932 ) >> 933 fs[] >> DECIDE_TAC 934 ) 935 ) 936 ) 937 938val big_timeout_0 = Q.prove ( 939`!st p r. 940 sem_t st p = (Rtimeout,r) 941 ��� 942 r.clock = 0`, 943 ho_match_mp_tac sem_t_ind >> 944 conj_tac >- ( 945 rw [sem_t_def_with_stop, sem_e_not_timeout]) >> 946 conj_tac >- ( 947 rw [sem_t_def_with_stop, sem_e_not_timeout]) >> 948 conj_tac >- ( 949 rw [sem_t_def_with_stop, sem_e_not_timeout] >> 950 ect >> fs []) >> 951 conj_tac >- ( 952 rw [sem_t_def_with_stop, sem_e_not_timeout] >> 953 ect >> fs []) >> 954 conj_tac >- ( 955 rw [sem_t_def_with_stop, sem_e_not_timeout] >> 956 ect >> fs [sem_e_not_timeout]) 957 >- ( 958 rw [] >> 959 pop_assum mp_tac >> 960 simp [sem_t_def_with_stop] >> 961 ect >> 962 fs [sem_e_not_timeout, STOP_def] >> 963 rw [] >> 964 fs [])); 965 966val sem_equiv_lem = Q.store_thm ("sem_equiv_lem", 967`���prog. fbs_sem for_big_sem prog = small_sem for_small_sem prog`, 968 match_mp_tac small_fbs_equiv2 >> 969 conj_tac >- ( 970 rw [for_big_sem_def, eval_with_clock_def, for_eval_def] >> 971 ect >> 972 fs [] >> 973 metis_tac [big_timeout_0]) >> 974 qexists_tac `I` >> 975 conj_tac 976 >- ( 977 rw [unbounded_def] >> 978 qexists_tac `SUC x` >> 979 simp []) >> 980 rpt gen_tac >> 981 simp [for_big_sem_def, for_eval_def, eval_with_clock_def] >> 982 DISCH_TAC >> 983 ect >> 984 imp_res_tac big_small_lem >> 985 qexists_tac `tr` >> 986 fs [for_small_sem_def] >> 987 rw [same_result_def, for_unload_def] >> 988 fs [res_rel_t_cases, is_val_t_def, is_val_e_def, some_no_choice] >> 989 simp [] >> 990 rw [] 991 >- (rw [Once step_t_cases] >> 992 rw [Once step_e_cases]) 993 >- rw [Once step_t_cases] 994 >- (rw [some_def] >> 995 metis_tac []) 996 >- metis_tac [PAIR]); 997 998(* check traces are unique up to prefixing *) 999val check_trace_determ = Q.prove( 1000`���tr h f. 1001 check_trace f (h::tr) ��� 1002 ���tr'. 1003 LENGTH tr' ��� LENGTH tr ��� 1004 check_trace f (h::tr') ��� 1005 isPREFIX tr' tr`, 1006 Induct>>rw[]>>fs[check_clock_def,isPREFIX,LENGTH_NIL]>> 1007 Cases_on`tr'`>>fs[check_trace_def]>> 1008 metis_tac[]) 1009 1010val check_trace_prefixes = Q.prove( 1011`���tr f. 1012 tr ��� [] ��� 1013 check_trace f tr ��� 1014 ���tr'. 1015 tr' ��� [] ��� HD tr' = HD tr ��� 1016 check_trace f tr' ��� 1017 isPREFIX tr tr' ��� isPREFIX tr' tr`, 1018 rw[]>> 1019 Cases_on`tr`>>Cases_on`tr'`>>fs[]>> 1020 Cases_on`LENGTH t' ��� LENGTH t`>> 1021 TRY(`LENGTH t ��� LENGTH t'` by DECIDE_TAC)>> 1022 metis_tac[check_trace_determ]) 1023 1024val check_trace_TL = Q.prove( 1025`���tr tr'. 1026 (tr ��� [] ��� 1027 check_trace (��st. some st'. step_t st st') tr ��� 1028 (���t'. ��step_t (LAST tr) t') ��� 1029 check_trace (��st. some st'. step_t st st') tr' ��� 1030 isPREFIX tr tr') ��� 1031 tr = tr'`, 1032 Induct>>fs[check_trace_def,LAST_DEF]>>rw[]>>Cases_on`tr'`>>fs[] 1033 >- 1034 (Cases_on`t`>>fs[check_trace_def,some_def]>> 1035 metis_tac[]) 1036 >> 1037 Cases_on`tr`>>Cases_on`t`>>fs[check_trace_def]>> 1038 res_tac>>fs[]) 1039 1040val FST_SPLIT = Q.prove( 1041`FST x = y ��� ���z. x = (y,z)`, 1042Cases_on`x`>>fs[]) 1043 1044val big_val_no_errors = Q.prove( 1045`!st p v s. 1046 sem_t st p = (Rval v,s) 1047 ��� 1048 (���c. 1049 (FST (sem_t (st with clock:= c) p) ��� Rbreak) 1050 ��� (FST (sem_t (st with clock:=c) p) ��� Rfail))`, 1051 rw[]>>CCONTR_TAC>>fs[]>>imp_res_tac FST_SPLIT>> 1052 imp_res_tac big_small_lem>> 1053 `HD tr = HD tr'` by fs[]>> 1054 fs[res_rel_t_cases]>> 1055 `���t'. ��step_t (LAST tr) t'` by 1056 fs[Once step_t_cases,FORALL_PROD]>> 1057 `���t'. ��step_t (LAST tr') t'` by 1058 fs[Once step_t_cases,FORALL_PROD,Once step_e_cases]>> 1059 `isPREFIX tr tr' ��� isPREFIX tr' tr` by 1060 metis_tac[check_trace_prefixes]>> 1061 `tr = tr'` by metis_tac[check_trace_TL]>> 1062 fs[]>> 1063 qpat_assum`A=t` (SUBST_ALL_TAC o SYM)>>fs[is_val_t_def,is_val_e_def]) 1064 1065(* Prove that the straightforward definition of the semantics are the same as 1066 * the ones used in the big/small equivalence *) 1067 1068val to_obs_def = Define ` 1069 (to_obs (Terminate NONE) = Crash) ��� 1070 (to_obs (Terminate _ ) = Terminate) ��� 1071 (to_obs Diverge = Diverge) ��� 1072 (to_obs Crash = Crash)`; 1073 1074val some_SAT = Q.prove( 1075`!P y. (some x. P x) = SOME y ��� P y`, 1076rw[some_def,SELECT_THM]>> 1077metis_tac[SELECT_AX]) 1078 1079val sstac = first_assum (fn th => mp_tac (HO_MATCH_MP some_SAT th)) 1080 1081val fbs_equiv = Q.prove ( 1082`!t. for$semantics t = to_obs (fbs_sem for_big_sem t)`, 1083 rw [semantics_def, to_obs_def, fbs_sem_def, for_big_sem_def] >> 1084 fs [to_obs_def, some_no_choice, eval_with_clock_def, for_eval_def, s_with_clock_def]>>ect>> 1085 fs[to_obs_def,some_no_choice]>> 1086 TRY(sstac>>fs[]>>NO_TAC)>> 1087 TRY(first_x_assum(qspec_then`x` mp_tac)>>fs[]>>NO_TAC)>> 1088 TRY(qpat_assum`A=a` (SUBST_ALL_TAC o SYM)>>fs[to_obs_def]>>NO_TAC)>> 1089 TRY(imp_res_tac big_val_no_errors>>fs[]>>metis_tac[FST]) 1090 >- (pop_assum(qspec_then`c` mp_tac)>>fs[]) 1091 >> (pop_assum(qspec_then`c` mp_tac)>>fs[]>>ect>>fs[])) 1092 1093val check_trace_thm2 = Q.prove( 1094`���s1 s2. 1095step_t^* s1 s2 ��� (��s1 s2.(some st'.step_t s1 st')= SOME s2)^* s1 s2`, 1096rw[]>>eq_tac>>qspec_tac (`s2`,`s2`) >>qspec_tac (`s1`,`s1`) >> 1097ho_match_mp_tac RTC_INDUCT>>rw[]>>simp[Once RTC_CASES1]>> 1098DISJ2_TAC>> 1099qexists_tac`s1'`>> 1100fs[some_to_SOME_step_t,some_def,step_t_determ]>> 1101metis_tac[SELECT_THM]) 1102 1103val some_not_step_t = Q.prove( 1104`(some s'.step_t s s') = NONE ��� 1105 ���s1 t1. ��step_t s (s1,t1)`, 1106rw[some_def,FORALL_PROD]) 1107 1108val small_equiv_lem = Q.prove( 1109` 1110 (some s'. 1111 (step_t^* s s' ��� 1112 ���s2 t2. ��step_t s' (s2,t2))) 1113 = 1114 (some s'. 1115 (��s1 s2. (some st'. step_t s1 st') = SOME s2)^* 1116 s s' ��� (some st'. step_t s' st') = NONE)`, 1117fs[check_trace_thm2,check_trace_thm,some_not_step_t]) 1118 1119val small_equiv = Q.prove ( 1120`!t. semantics_small t = to_obs (small_sem for_small_sem t)`, 1121 rw [semantics_small_def, small_sem_def, for_small_sem_def] >> 1122 unabbrev_all_tac >> 1123 rw [] >> 1124 fs[small_equiv_lem]>> 1125 ect>>fs[to_obs_def,for_unload_def,is_val_t_def]>> 1126 Cases_on`e`>>fs[to_obs_def,is_val_e_def]) 1127 1128val sem_equiv_thm = Q.store_thm ("sem_equiv_thm", 1129`���prog. for$semantics prog = semantics_small prog`, 1130 rw [small_equiv, fbs_equiv] >> 1131 metis_tac [sem_equiv_lem]); 1132 1133(*Pretty printing*) 1134val hideseq_def = Define` 1135 hideseq = Seq` 1136 1137val _ = save_thm ("step_t_rules_hideseq",step_t_rules |> REWRITE_RULE[GSYM hideseq_def]) 1138 1139val _ = export_theory (); 1140