1open HolKernel Parse boolLib bossLib; 2open optionTheory pairTheory pred_setTheory finite_mapTheory stringTheory; 3open integerTheory listTheory optionTheory rich_listTheory; 4open lcsymtacs BasicProvers; 5open for_ndTheory for_nd_semTheory oracleSemTheory simple_traceTheory; 6open relationTheory; 7 8val _ = new_theory "for_osmall"; 9 10val _ = temp_tight_equality (); 11 12val ect = BasicProvers.EVERY_CASE_TAC; 13val fct = BasicProvers.FULL_CASE_TAC; 14 15val some_no_choice = Q.prove ( 16`!f. (some x. f x) = NONE ��� ��?x. f x`, 17 rw [some_def]); 18 19val some_SAT = Q.prove( 20`!P y. (some x. P x) = SOME y ��� P y`, 21rw[some_def,SELECT_THM]>> 22metis_tac[SELECT_AX]) 23 24(* A small step semantics for the non-deterministic FOR language with I/O *) 25 26(* Add AddL and AddR to model making the choice one which sub-expression to 27 * evaluate before starting the evaluation. Thus preventing switching in the 28 * middle of evaluating one of them. 29 *) 30val _ = Datatype ` 31small_e = 32 | Var string 33 | Num int 34 | Add small_e small_e 35 | AddL small_e small_e 36 | AddR small_e small_e 37 | Assign string small_e 38 | Getchar 39 | Putchar small_e`; 40 41(* Add a Handle statement that will stop breaks from propagating *) 42val _ = Datatype ` 43small_t = 44 | Dec string small_t 45 | Exp small_e 46 | Break 47 | Seq small_t small_t 48 | If small_e small_t small_t 49 | For small_e small_e small_t 50 | Handle small_t`; 51 52val _ = Datatype ` 53 lab = ND bool | W char | R char`; 54 55val e_to_small_e_def = Define ` 56(e_to_small_e ((Num i):e) = ((Num i) : small_e)) ��� 57(e_to_small_e (Var x) = Var x) ��� 58(e_to_small_e (Add e1 e2) = Add (e_to_small_e e1) (e_to_small_e e2)) ��� 59(e_to_small_e (Assign x e) = Assign x (e_to_small_e e)) ��� 60(e_to_small_e Getchar = Getchar) ��� 61(e_to_small_e (Putchar e) = Putchar (e_to_small_e e))`; 62 63val t_to_small_t_def = Define ` 64(t_to_small_t ((Dec string t):t) = ((Dec string (t_to_small_t t)) : small_t)) ��� 65(t_to_small_t (Exp e) = Exp (e_to_small_e e)) ��� 66(t_to_small_t Break = Break) ��� 67(t_to_small_t (Seq t1 t2) = Seq (t_to_small_t t1) (t_to_small_t t2)) ��� 68(t_to_small_t (If e t1 t2) = If (e_to_small_e e) (t_to_small_t t1) (t_to_small_t t2)) ��� 69(t_to_small_t (For e1 e2 t) = For (e_to_small_e e1) (e_to_small_e e2) (t_to_small_t t))`; 70 71val is_val_e_def = Define ` 72(is_val_e (Num n) = T) ��� 73(is_val_e _ = F)`; 74 75val (step_e_rules, step_e_ind, step_e_cases) = Hol_reln ` 76(!s x n. 77 FLOOKUP s.store x = SOME n 78 ��� 79 step_e (s, Var x) NONE (s, Num n)) ��� 80(!s e1 e2 o'. 81 oracle_get s.non_det_o = (F, o') 82 ��� 83 step_e (s, Add e1 e2) 84 (SOME (INR F)) 85 (s with <| non_det_o := o'; io_trace := s.io_trace ++ [INR F] |>, AddL e1 e2)) ��� 86(!s e1 e2 o'. 87 oracle_get s.non_det_o = (T, o') 88 ��� 89 step_e (s, Add e1 e2) (SOME (INR T)) (s with <| non_det_o := o'; io_trace := s.io_trace ++ [INR T] |>, AddR e1 e2)) ��� 90(!s n1 n2. 91 step_e (s, AddL (Num n1) (Num n2)) NONE (s, Num (n1 + n2))) ��� 92(!s n1 n2. 93 step_e (s, AddR (Num n1) (Num n2)) NONE (s, Num (n1 + n2))) ��� 94(!s s2 e1 e2 e3 l. 95 step_e (s, e1) l (s2, e3) 96 ��� 97 step_e (s, AddL e1 e2) l (s2, AddL e3 e2)) ��� 98(!s s2 i e1 e2 l. 99 step_e (s, e1) l (s2, e2) 100 ��� 101 step_e (s, AddL (Num i) e1) l (s2, AddL (Num i) e2)) ��� 102(!s s2 i e1 e2 l. 103 step_e (s, e1) l (s2, e2) 104 ��� 105 step_e (s, AddR e1 (Num i)) l (s2, AddR e2 (Num i))) ��� 106(!s s2 e1 e2 e3 l. 107 step_e (s, e2) l (s2, e3) 108 ��� 109 step_e (s, AddR e1 e2) l (s2, AddR e1 e3)) ��� 110(!s x n. 111 step_e (s, Assign x (Num n)) NONE (s with store := s.store |+ (x, n), Num n)) ��� 112(!s s2 x e1 e2 l. 113 step_e (s, e1) l (s2, e2) 114 ��� 115 step_e (s, Assign x e1) l (s2, Assign x e2)) ��� 116(!s i input'. 117 getchar s.input = (i,input') 118 ��� 119 step_e (s, Getchar) 120 (SOME (INL (Itag i))) 121 (s with <| input := input'; io_trace := s.io_trace ++ [INL (Itag i)] |>, Num i)) ��� 122(!s s2 e1 e2 l. 123 step_e (s, e1) l (s2, e2) 124 ��� 125 step_e (s, Putchar e1) l (s2, Putchar e2)) ��� 126(!s i. 127 step_e (s, Putchar (Num i)) 128 (SOME (INL (Otag i))) 129 (s with io_trace := s.io_trace ++ [INL (Otag i)], Num i))`; 130 131val is_val_t_def = Define ` 132(is_val_t (Exp (e : small_e)) = is_val_e e) ��� 133(is_val_t Break = T) ��� 134(is_val_t _ = F)`; 135 136val (step_t_rules, step_t_ind, step_t_cases) = Hol_reln ` 137(!s t x. 138 step_t (s, Dec x t) NONE (s with store := s.store |+ (x, 0), t)) ��� 139(!s s2 e e2 l. 140 step_e (s, e) l (s2, e2) 141 ��� 142 step_t (s, Exp e) l (s2, Exp e2)) ��� 143(!s s2 t1 t2 t1' l. 144 step_t (s, t1) l (s2, t1') 145 ��� 146 step_t (s, Seq t1 t2) l (s2, Seq t1' t2)) ��� 147(!s t. 148 step_t (s, Seq Break t) NONE (s, Break)) ��� 149(!s n t. 150 step_t (s, Seq (Exp (Num n)) t) NONE (s, t)) ��� 151(!s s2 e t1 t2 e2 l. 152 step_e (s, e) l (s2,e2) 153 ��� 154 step_t (s, If e t1 t2) l (s2, If e2 t1 t2)) ��� 155(!s t1 t2. 156 step_t (s, If (Num 0) t1 t2) NONE (s, t2)) ��� 157(!s n t1 t2. 158 n ��� 0 159 ��� 160 step_t (s, If (Num n) t1 t2) NONE (s, t1)) ��� 161(!s. 162 step_t (s, Handle Break) NONE (s, Exp (Num 0))) ��� 163(!s t. 164 is_val_t t ��� 165 t ��� Break 166 ��� 167 step_t (s, Handle t) NONE (s, t)) ��� 168(!s1 s2 t1 t2 l. 169 step_t (s1, t1) l (s2, t2) 170 ��� 171 step_t (s1, Handle t1) l (s2, Handle t2)) ��� 172(!s e1 e2 t. 173 step_t (s, For e1 e2 t) NONE (s, Handle (If e1 (Seq t (Seq (Exp e2) (For e1 e2 t))) (Exp (Num 0)))))`; 174 175val filter_map_def = Define ` 176(filter_map f [] = []) ��� 177(filter_map f (h::t) = 178 case f h of 179 | NONE => filter_map f t 180 | SOME x => x :: filter_map f t)`; 181 182val path_to_obs_def = Define ` 183 path_to_obs p = 184 if ��finite p then 185 Diverge (lfilter_map I (labels p)) 186 else if is_val_t (SND (last p)) then 187 Terminate (filter_map I (THE (toList (labels p)))) 188 else 189 Crash`; 190 191val semantics_small_def = Define ` 192 (semantics_small input prog = 193 { path_to_obs p | p,nd | 194 okpath step_t p ��� complete step_t p ��� first p = (init_st 0 nd input, t_to_small_t prog) })`; 195 196(* ----------- Connect to functional big step -------------- *) 197 198val for_small_sem_def = Define ` 199 for_small_sem input = 200 <| step := (\st. some st'. ?l. step_t st l st'); 201 is_result := (\st. is_val_t (SND st)); 202 load := (\nd t. (init_st 0 nd input , t_to_small_t t)); 203 unload := (\st. (FST st).io_trace) |>`; 204 205val for_eval_def = Define ` 206 for_eval st env t = 207 case sem_t st t of 208 (Rval v, s) => (s, Val (SOME v)) 209 | (Rbreak, s) => (s, Val NONE) 210 | (Rtimeout, s) => (s, Timeout) 211 | (Rfail, s) => (s, Error)`; 212 213val for_big_sem_def = Define ` 214 for_big_sem input = 215 <| eval := for_eval; 216 init_st := (\nd. init_st 0 nd input); 217 init_env := (); 218 get_clock := (\x. x.clock); 219 set_clock := (\c st. st with clock := c); 220 get_oracle_events := (\st. st.io_trace) |>`; 221 222val (res_rel_t_rules, res_rel_t_ind, res_rel_t_cases) = Hol_reln ` 223(!i s. 224 res_rel_t (Rval i, s) (s with clock := 0, Exp (Num i))) ��� 225(!s t. 226 (~?l s' t'. step_t (s with clock := 0, t) l (s', t')) ��� 227 ~is_val_t t 228 ��� 229 res_rel_t (Rfail, s) (s with clock := 0, t)) ��� 230(!s. 231 res_rel_t (Rbreak, s) (s with clock := 0, Break)) ��� 232(!s t. 233 (?l s' t'. step_t (s, t) l (s', t')) ��� 234 s.clock = 0 235 ��� 236 res_rel_t (Rtimeout, s) (s, t))`; 237 238val (res_rel_e_rules, res_rel_e_ind, res_rel_e_cases) = Hol_reln ` 239(!i s. 240 res_rel_e (Rval i, s) (s with clock:=0, Num i)) ��� 241(!s e. 242 (~?s' e' l. step_e (s, e) l (s', e')) ��� 243 ~is_val_e e 244 ��� 245 res_rel_e (Rfail, s) (s with clock:=0, e))` 246 247val _ = set_trace "Goalstack.print_goal_at_top" 0; 248 249val step_t_strongind = (fetch "-" "step_t_strongind") 250val step_e_strongind = (fetch "-" "step_e_strongind") 251 252val conjs_def = Define` conjs A B ��� A ��� B` 253 254val etac = (fs[Once step_t_cases]>>fs[Once step_t_cases,Once step_e_cases,conjs_def]) 255 256(* Determinism of small-step w.r.t. an oracle *) 257 258val step_e_determ = Q.prove( 259` ���se l1 se1. 260 step_e se l1 se1 ��� 261 (���l2 se2. 262 step_e se l2 se2 ��� conjs (se1 = se2) (l1 = l2))`, 263 ho_match_mp_tac step_e_strongind>>rw[]>>fs[FORALL_PROD] 264 >- (rw[conjs_def]>>fs[Once step_e_cases]>>rfs[]) 265 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 266 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 267 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 268 >- (rw[conjs_def]>>ntac 2(fs[Once step_e_cases]>>rfs[])) 269 >> 270 TRY 271 (pop_assum mp_tac>>simp[Once step_e_cases]>>rw[]>> 272 fs[Once step_e_cases]) 273 >> 274 fs[conjs_def])|>REWRITE_RULE[conjs_def] 275 276val step_t_determ = Q.prove( 277` ���st l1 st1. 278 step_t st l1 st1 ��� 279 (���l2 st2. 280 step_t st l2 st2 ��� conjs (st1 = st2) (l1 = l2))`, 281 ho_match_mp_tac step_t_strongind >>rw[] 282 >- etac 283 >- 284 (fs[Once step_t_cases]>> 285 imp_res_tac step_e_determ>> 286 fs[conjs_def]) 287 >- 288 (pop_assum mp_tac>> 289 simp[Once step_t_cases]>>fs[FORALL_PROD]>>rw[]>> 290 fs[Once step_t_cases,Once step_e_cases]) 291 >- etac 292 >- etac 293 >- 294 (fs[Once step_t_cases] 295 >- 296 (imp_res_tac step_e_determ>>fs[conjs_def]) 297 >> etac) 298 >- etac 299 >- etac 300 >- etac 301 >- 302 (fs[Once step_t_cases]>>rfs[conjs_def]>> 303 Cases_on`t`>>fs[is_val_t_def]>> 304 Cases_on`s'`>>fs[is_val_e_def]>> 305 fs[Once step_t_cases]>> 306 fs[Once step_e_cases]) 307 >- 308 (pop_assum mp_tac>> 309 simp[Once step_t_cases]>>rw[] 310 >- 311 etac 312 >- 313 (Cases_on`t1`>>fs[is_val_t_def]>>Cases_on`s`>>fs[is_val_e_def]>> 314 fs[Once step_t_cases,Once step_e_cases]) 315 >> 316 fs[FORALL_PROD]>>metis_tac[]) 317 >> 318 fs[Once step_t_cases,conjs_def])|>REWRITE_RULE[conjs_def] 319 320val step_t_select_unique = Q.prove( 321`step_t (q,r) l st' ��� 322 (@st'. ���l. step_t (q,r) l st') = st'`, 323 rw[]>> 324 metis_tac[step_t_determ]) 325 326val some_to_SOME_step_e = Q.prove( 327`step_e A l B ��� 328 (some st'. ���l. step_e A l st') = SOME B`, 329 rw[]>>fs[some_def]>> 330 metis_tac[step_e_determ]) |> GEN_ALL 331 332val some_to_SOME_step_t = Q.prove( 333`step_t A l B ��� 334 (some st'. ���l. step_t A l st') = 335 SOME B`, 336 rw[]>>fs[some_def]>>metis_tac[step_t_determ]) |>GEN_ALL 337 338(* Contextual transitions of the small step semantics *) 339val check_trace_seq = Q.prove( 340`���tr. 341 check_trace (��st. some st'. ���l. step_t st l st') tr ��� 342 check_trace (��st. some st'. ���l. step_t st l st') (MAP (��st,t. (st,Seq t p)) tr)`, 343 Induct>>rw[]>> 344 Cases_on`tr`>>fs[check_trace_def]>> 345 Cases_on`h`>>Cases_on`h'`>> 346 match_mp_tac some_to_SOME_step_t>> 347 fs[some_def]>> 348 simp[Once step_t_cases]>> 349 metis_tac[step_t_select_unique]) 350 351val check_trace_assign = Q.prove( 352`���tr. 353 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 354 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e. (st,Assign s e)) tr)`, 355 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 356 Cases_on`h`>>Cases_on`h'`>> 357 match_mp_tac some_to_SOME_step_e>> 358 fs[some_def]>> 359 simp[Once step_e_cases]>> 360 metis_tac[step_e_determ]) 361 362val check_trace_putchar = Q.prove( 363`���tr. 364 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 365 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e. (st,Putchar e)) tr)`, 366 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 367 Cases_on`h`>>Cases_on`h'`>> 368 match_mp_tac some_to_SOME_step_e>> 369 fs[some_def]>> 370 simp[Once step_e_cases]>> 371 metis_tac[step_e_determ]) 372 373val check_trace_addl1 = Q.prove( 374`���tr. 375 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 376 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e. (st,AddL e e')) tr)`, 377 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 378 Cases_on`h`>>Cases_on`h'`>> 379 match_mp_tac some_to_SOME_step_e>> 380 fs[some_def]>> 381 simp[Once step_e_cases]>> 382 metis_tac[step_e_determ]) 383 384val check_trace_addl2 = Q.prove( 385`���tr. 386 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 387 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e'. (st,AddL (Num i) e')) tr)`, 388 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 389 Cases_on`h`>>Cases_on`h'`>> 390 match_mp_tac some_to_SOME_step_e>> 391 fs[some_def]>> 392 simp[Once step_e_cases]>> 393 metis_tac[step_e_determ]) 394 395val check_trace_addr1 = Q.prove( 396`���tr. 397 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 398 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e'. (st,AddR e e')) tr)`, 399 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 400 Cases_on`h`>>Cases_on`h'`>> 401 match_mp_tac some_to_SOME_step_e>> 402 fs[some_def]>> 403 simp[Once step_e_cases]>> 404 metis_tac[step_e_determ,is_val_e_def]) 405 406val check_trace_addr2 = Q.prove( 407`���tr. 408 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 409 check_trace (��st. some st'. ?l. step_e st l st') (MAP (��st,e'. (st,AddR e' (Num i))) tr)`, 410 Induct>>rw[]>>Cases_on`tr`>>fs[check_trace_def]>> 411 Cases_on`h`>>Cases_on`h'`>> 412 match_mp_tac some_to_SOME_step_e>> 413 fs[some_def]>> 414 simp[Once step_e_cases]>> 415 metis_tac[step_e_determ,is_val_e_def]) 416 417val check_trace_exp = Q.prove( 418`���tr. 419 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 420 check_trace (��st. some st'. ?l. step_t st l st') (MAP (��st,e'. (st,Exp e')) tr)`, 421 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 422 Cases_on`h`>>Cases_on`h'`>> 423 match_mp_tac some_to_SOME_step_t>> 424 fs[some_def]>> 425 simp[Once step_t_cases]>> 426 metis_tac[step_e_determ]) 427 428val check_trace_if1 = Q.prove( 429`���tr. 430 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 431 check_trace (��st. some st'. ?l. step_t st l st') (MAP (��st,e'. (st,If e' a b)) tr)`, 432 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 433 Cases_on`h`>>Cases_on`h'`>> 434 match_mp_tac some_to_SOME_step_t>> 435 fs[some_def]>> 436 simp[Once step_t_cases]>> 437 metis_tac[step_e_determ]) 438 439val check_trace_for1 = Q.prove( 440`���tr. 441 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 442 check_trace (��st. some st'. ?l. step_t st l st') 443 (MAP (��st,e'. (st, 444 Handle (If e' a b))) tr)`, 445 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 446 Cases_on`h`>>Cases_on`h'`>> 447 match_mp_tac some_to_SOME_step_t>> 448 fs[some_def]>> 449 simp[Once step_t_cases]>> 450 simp[Once step_t_cases]>> 451 metis_tac[step_e_determ]) 452 453val check_trace_for2 = Q.prove( 454`���tr. 455 check_trace (��st. some st'. ?l. step_t st l st') tr ��� 456 check_trace (��st. some st'. ?l. step_t st l st') 457 (MAP (��st,t'. (st, 458 Handle (Seq t' a))) tr)`, 459 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 460 Cases_on`h`>>Cases_on`h'`>> 461 match_mp_tac some_to_SOME_step_t>> 462 fs[some_def]>> 463 simp[Once step_t_cases]>> 464 simp[Once step_t_cases]>> 465 metis_tac[step_e_determ]) 466 467val check_trace_for3 = Q.prove( 468`���tr. 469 check_trace (��st. some st'. ?l. step_e st l st') tr ��� 470 check_trace (��st. some st'. ?l. step_t st l st') 471 (MAP (��st,e'. (st, 472 Handle (Seq (Exp e') a))) tr)`, 473 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 474 Cases_on`h`>>Cases_on`h'`>> 475 match_mp_tac some_to_SOME_step_t>> 476 fs[some_def]>> 477 ntac 3 (simp[Once step_t_cases])>> 478 metis_tac[step_e_determ]) 479 480val check_trace_handle = Q.prove( 481`���tr. 482 check_trace (��st. some st'. ?l. step_t st l st') tr ��� 483 check_trace (��st. some st'. ?l. step_t st l st') 484 (MAP (��st,t'. (st, 485 Handle t')) tr)`, 486 Induct>>rw[check_trace_def]>>Cases_on`tr`>>fs[check_trace_def]>> 487 Cases_on`h`>>Cases_on`h'`>> 488 match_mp_tac some_to_SOME_step_t>> 489 fs[some_def]>> 490 simp[Once step_t_cases]>> 491 Cases_on`st'`>>metis_tac[step_t_determ]) 492 493(* Non-existence of contextual transitions in small-step *) 494val no_step_e_assign = Q.prove( 495`���e. 496 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 497 ��is_val_e e 498 ��� 499 ���s' e' l. ��step_e (s,Assign v e) l (s',e')`, 500 Induct>>rw[is_val_e_def]>> 501 simp[Once step_e_cases]) 502 503val no_step_e_putchar = Q.prove( 504`���e. 505 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 506 ��is_val_e e 507 ��� 508 ���s' e' l. ��step_e (s,Putchar e) l (s',e')`, 509 Induct>>rw[is_val_e_def]>> 510 simp[Once step_e_cases]) 511 512val no_step_e_addl1 = Q.prove( 513`���e. 514 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 515 ��is_val_e e 516 ��� 517 ���s' e' l. ��step_e (s,AddL e e'') l (s',e')`, 518 Induct>>rw[is_val_e_def]>>simp[Once step_e_cases,is_val_e_def]) 519 520val no_step_e_addl2 = Q.prove( 521`���e. 522 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 523 ��is_val_e e 524 ��� 525 ���s' e' l. ��step_e (s,AddL (Num i) e) l (s',e')`, 526 Induct>>rw[is_val_e_def]>>rpt (simp[Once step_e_cases,is_val_e_def])) 527 528val no_step_e_addr1 = Q.prove( 529`���e. 530 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 531 ��is_val_e e 532 ��� 533 ���s' e' l. ��step_e (s,AddR e'' e) l (s',e')`, 534 Induct>>rw[is_val_e_def]>> 535 rpt (simp[Once step_e_cases])) 536 537val no_step_e_addr2 = Q.prove( 538`���e. 539 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 540 ��is_val_e e 541 ��� 542 ���s' e' l. ��step_e (s,AddR e (Num i)) l (s',e')`, 543 Induct>>rw[is_val_e_def]>> 544 rpt (simp[Once step_e_cases])) 545 546val no_step_t_exp = Q.prove( 547`���e. 548 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 549 ��is_val_e e 550 ��� 551 ���s' t' l. ��step_t (s,Exp e) l (s',t')`, 552 Induct>>rw[is_val_e_def]>> 553 simp[Once step_t_cases]) 554 555val no_step_t_seq = Q.prove( 556`���t. 557 (���s' t' l. ��step_t (s,t) l (s',t')) ��� 558 ��is_val_t t 559 ��� 560 ���s' t' l. ��step_t (s,Seq t p) l (s',t')`, 561 Induct>>rw[is_val_t_def]>> 562 simp[Once step_t_cases]>> 563 Cases_on`s'`>>fs[is_val_e_def]) 564 565val no_step_t_if1 = Q.prove( 566`���e. 567 (���s' e' l. ��step_e (s,e) l (s',e')) ��� 568 ��is_val_e e 569 ��� 570 ���s' t' l. ��step_t (s,If e a b) l (s',t')`, 571 Induct>>rw[is_val_e_def]>> 572 simp[Once step_t_cases]) 573 574val no_step_t_handle = Q.prove( 575`���t. 576 (���s' t' l. ��step_t (s,t) l (s',t')) ��� 577 ��is_val_t t 578 ��� 579 ���s' t' l. ��step_t (s,Handle t) l (s',t')`, 580 Induct>>rw[is_val_t_def]>> 581 simp[Once step_t_cases,is_val_t_def]) 582 583val LAST_MAP = Q.prove( 584`���ls. ls ��� [] ��� LAST (MAP f ls) = f (LAST ls)`, 585 Induct>>fs[LAST_DEF]>>rw[]) 586 587val HD_MAP = Q.prove( 588`���ls. ls ��� [] ��� HD(MAP f ls) = f (HD ls)`, 589 Induct>>rw[]) 590 591val HD_APPEND = Q.prove( 592`ls ��� [] ��� HD (ls ++ ls') = HD ls`, 593Cases_on`ls`>>fs[]) 594 595val LAST_APPEND = Q.prove( 596`ls' ��� [] ��� LAST (ls ++ ls') = LAST ls'`, 597Cases_on`ls'`>>fs[]) 598 599val sem_e_not_timeout = Q.prove ( 600`!st e r. sem_e st e ��� (Rtimeout, r)`, 601 Induct_on `e` >> 602 rw [sem_e_def, LET_THM, permute_pair_def, oracle_get_def, unpermute_pair_def, getchar_def] >> 603 ect >> 604 fs [] >> 605 metis_tac []); 606 607val sem_e_not_break = Q.prove( 608`!st e r. sem_e st e ��� (Rbreak,r)`, 609 Induct_on`e`>>srw_tac[][sem_e_def]>> 610 ect>> 611 fs[LET_THM,unpermute_pair_def,permute_pair_def,oracle_get_def]>> 612 TRY(qpat_assum`A=(fst_e,snd_e)` mp_tac)>> 613 rw[]>> 614 TRY(metis_tac[])) 615 616val LAST_HD_eq = Q.prove(` 617���ls ls'. 618 ls ��� [] ��� ls' ��� [] ��� 619 LAST ls = HD ls' ��� 620 BUTLASTN 1 ls ++ ls' = 621 ls ++ TL ls'`, 622 Induct>>fs[LAST_DEF,BUTLASTN_1]>>rw[]>> 623 Cases_on`ls'`>>fs[FRONT_DEF]) 624 625val check_trace_append3 = Q.prove(` 626 check_trace f ls ��� 627 f h = SOME (HD ls) ��� 628 check_trace f (h :: ls)`, 629 rw[]>>imp_res_tac check_trace_append2>> 630 pop_assum(qspec_then`[h]`assume_tac)>>fs[]>> 631 rfs[check_trace_def]) 632 633val check_trace_tl = Q.prove(` 634 check_trace f ls ��� ls ��� [] ��� 635 check_trace f (TL ls)`, 636 Cases_on`ls`>>fs[check_trace_def]>> 637 Cases_on`t`>>fs[check_trace_def]) 638 639(* Start connecting functional big step to small step traces *) 640local val rw = srw_tac[] val fs = fsrw_tac[] in 641val sem_e_big_small_lem = Q.prove( 642`!s e r. 643 sem_e s e = r 644 ��� 645 ?tr. 646 tr ��� [] ��� 647 check_trace (\st. some st'. ?l. step_e st l st') tr ��� 648 HD tr = (s with clock:=0, e_to_small_e e) ��� 649 res_rel_e r (LAST tr)`, 650 Induct_on`e`>>rw[]>>fs[sem_e_def,e_to_small_e_def] 651 >- 652 (fct>>fs[res_rel_e_cases] 653 >- 654 (qexists_tac`[(s' with clock:=0,Var s)]`>>fs[check_trace_def,is_val_e_def]>> 655 simp[Once step_e_cases]) 656 >- 657 (qexists_tac`[(s' with clock:=0,Var s);(s' with clock:=0,Num x)]`>> 658 fs[check_trace_def,some_def]>> 659 ntac 2 (simp[Once step_e_cases]))) 660 >- 661 (fs[res_rel_e_cases]>> 662 qexists_tac`[s with clock:=0,Num i]`>>fs[check_trace_def]) 663 >- 664 (fs[LET_THM,permute_pair_def,oracle_get_def]>>IF_CASES_TAC>>fs[] 665 >- 666 (qpat_abbrev_tac`st = s with <|io_trace:=B;non_det_o:=C|>`>> 667 first_x_assum(qspec_then`st`assume_tac)>> 668 Cases_on`sem_e st e'`>>Cases_on`q`>> 669 fs[sem_e_not_break,sem_e_not_timeout,unpermute_pair_def] 670 >- 671 (fct>>Cases_on`q`>> 672 fs[sem_e_not_break,sem_e_not_timeout]>> 673 last_x_assum(qspec_then`r` assume_tac)>>rfs[]>> 674 qpat_abbrev_tac`h =(A,B)`>> 675 qabbrev_tac`ls1 = (MAP (��st,e'. (st,AddR (e_to_small_e e) e')) tr)`>> 676 qabbrev_tac`ls2 = (MAP (��st,e'. (st,AddR e' (Num i))) tr')`>> 677 qabbrev_tac`ls = BUTLASTN 1 ls1 ++ ls2`>> 678 fs[res_rel_e_cases]>> 679 `LAST ls1 = HD ls2` by 680 (unabbrev_all_tac>>fs[LAST_MAP,HD_MAP])>> 681 `ls = ls1 ++ (TL ls2)` by 682 (unabbrev_all_tac>> 683 fs[LAST_HD_eq])>> 684 `check_trace (��st. some st'. ���l. step_e st l st') ls2` by 685 fs[Abbr`ls2`,check_trace_addr2]>> 686 `check_trace (��st. some st'. ���l. step_e st l st') ls` by 687 (fs[Abbr`ls`]>>Cases_on`ls2`>>fs[]>>Cases_on`t`>>fs[] 688 >- 689 fs[check_trace_addr1,Abbr`ls1`] 690 >> 691 match_mp_tac check_trace_append2>>rw[] 692 >- 693 fs[check_trace_addr1,Abbr`ls1`] 694 >- 695 (fs[markerTheory.Abbrev_def]>> 696 `h''::t' = TL (LAST ls1::h''::t')` by fs[]>> 697 pop_assum SUBST_ALL_TAC>> 698 match_mp_tac check_trace_tl>>fs[check_trace_addr2]) 699 >> 700 fs[check_trace_def]) 701 >- 702 (qexists_tac`[h] ++ ls ++ [(r' with clock:=0,Num(i'+i))]`>> 703 rw[]>> 704 match_mp_tac check_trace_append3>>fs[check_trace_def]>>rw[] 705 >- 706 (match_mp_tac check_trace_append2>> 707 fs[check_trace_def]>> 708 fs[markerTheory.Abbrev_def,LAST_APPEND,LAST_MAP]>> 709 match_mp_tac some_to_SOME_step_e>> 710 simp[Once step_e_cases]) 711 >> 712 match_mp_tac some_to_SOME_step_e>> 713 fs[HD_APPEND,Abbr`ls1`,HD_MAP,Abbr`h`,Abbr`st`]>> 714 simp[Once step_e_cases,oracle_get_def]) 715 >> 716 qexists_tac`[h]++ls` >>rw[] 717 >- 718 (match_mp_tac check_trace_append3>> 719 fs[HD_APPEND,Abbr`ls1`,HD_MAP]>> 720 match_mp_tac some_to_SOME_step_e>> 721 fs[Abbr`h`,Abbr`st`]>> 722 simp[Once step_e_cases,oracle_get_def]) 723 >> 724 fs[markerTheory.Abbrev_def,LAST_DEF,LAST_APPEND,LAST_MAP,is_val_e_def,no_step_e_addr2]) 725 >> 726 qpat_abbrev_tac`h =(A,B)`>> 727 qexists_tac`[h]++(MAP (��st,e'. (st,AddR (e_to_small_e e) e')) tr)`>> 728 fs[HD_MAP,res_rel_e_cases,LAST_MAP,is_val_e_def,LAST_APPEND,no_step_e_addr1]>> 729 match_mp_tac check_trace_append3>>fs[check_trace_addr1,HD_MAP]>> 730 match_mp_tac some_to_SOME_step_e>> 731 unabbrev_all_tac>> 732 simp[Once step_e_cases,oracle_get_def]) 733 >> 734 (*symmetric*) 735 (qpat_abbrev_tac`st = s with <|io_trace:=B;non_det_o:=C|>`>> 736 last_x_assum(qspec_then`st`assume_tac)>> 737 Cases_on`sem_e st e`>>Cases_on`q`>> 738 fs[sem_e_not_break,sem_e_not_timeout,unpermute_pair_def] 739 >- 740 (fct>>Cases_on`q`>> 741 fs[sem_e_not_break,sem_e_not_timeout]>> 742 last_x_assum(qspec_then`r` assume_tac)>>rfs[]>> 743 qpat_abbrev_tac`h =(A,B)`>> 744 qabbrev_tac`ls1 = (MAP (��st,e. (st,AddL e (e_to_small_e e'))) tr)`>> 745 qabbrev_tac`ls2 = (MAP (��st,e'. (st,AddL (Num i) e')) tr')`>> 746 qabbrev_tac`ls = BUTLASTN 1 ls1 ++ ls2`>> 747 fs[res_rel_e_cases]>> 748 `LAST ls1 = HD ls2` by 749 (unabbrev_all_tac>>fs[LAST_MAP,HD_MAP])>> 750 `ls = ls1 ++ (TL ls2)` by 751 (unabbrev_all_tac>> 752 fs[LAST_HD_eq])>> 753 `check_trace (��st. some st'. ���l. step_e st l st') ls2` by 754 fs[Abbr`ls2`,check_trace_addl2]>> 755 `check_trace (��st. some st'. ���l. step_e st l st') ls` by 756 (fs[Abbr`ls`]>>Cases_on`ls2`>>fs[]>>Cases_on`t`>>fs[] 757 >- 758 fs[check_trace_addl1,Abbr`ls1`] 759 >> 760 match_mp_tac check_trace_append2>>rw[] 761 >- 762 fs[check_trace_addl1,Abbr`ls1`] 763 >- 764 (fs[markerTheory.Abbrev_def]>> 765 `h''::t' = TL (LAST ls1::h''::t')` by fs[]>> 766 pop_assum SUBST_ALL_TAC>> 767 match_mp_tac check_trace_tl>>fs[check_trace_addr2]) 768 >> 769 fs[check_trace_def]) 770 >- 771 (qexists_tac`[h] ++ ls ++ [(r' with clock:=0,Num(i+i'))]`>> 772 rw[]>> 773 match_mp_tac check_trace_append3>>fs[check_trace_def]>>rw[] 774 >- 775 (match_mp_tac check_trace_append2>> 776 fs[check_trace_def]>> 777 fs[markerTheory.Abbrev_def,LAST_APPEND,LAST_MAP]>> 778 match_mp_tac some_to_SOME_step_e>> 779 simp[Once step_e_cases]) 780 >> 781 match_mp_tac some_to_SOME_step_e>> 782 fs[HD_APPEND,Abbr`ls1`,HD_MAP,Abbr`h`,Abbr`st`]>> 783 simp[Once step_e_cases,oracle_get_def]) 784 >> 785 qexists_tac`[h]++ls` >>rw[] 786 >- 787 (match_mp_tac check_trace_append3>> 788 fs[HD_APPEND,Abbr`ls1`,HD_MAP]>> 789 match_mp_tac some_to_SOME_step_e>> 790 fs[Abbr`h`,Abbr`st`]>> 791 simp[Once step_e_cases,oracle_get_def]) 792 >> 793 fs[markerTheory.Abbrev_def,LAST_DEF,LAST_APPEND,LAST_MAP,is_val_e_def,no_step_e_addl2]) 794 >> 795 qpat_abbrev_tac`h =(A,B)`>> 796 qexists_tac`[h]++(MAP (��st,e. (st,AddL e (e_to_small_e e'))) tr)`>> 797 fs[HD_MAP,res_rel_e_cases,LAST_MAP,is_val_e_def,LAST_APPEND,no_step_e_addl1]>> 798 match_mp_tac check_trace_append3>>fs[check_trace_addl1,HD_MAP]>> 799 match_mp_tac some_to_SOME_step_e>> 800 unabbrev_all_tac>> 801 simp[Once step_e_cases,oracle_get_def])) 802 >- 803 (EVERY_CASE_TAC>>fs[res_rel_e_cases,sem_e_not_break,sem_e_not_timeout]>> 804 first_x_assum(qspec_then`s'` assume_tac)>>rfs[] 805 >- 806 (qexists_tac`(MAP (��st,e. (st,Assign s e)) tr)++[r with <|store :=r.store |+ (s,i); clock:=0|>,Num i]`>>fs[HD_MAP,HD_APPEND]>> 807 ho_match_mp_tac check_trace_append2>> 808 fs[check_trace_def,LAST_MAP,check_trace_assign]>> 809 ntac 2 (simp[Once step_e_cases])) 810 >> 811 (qexists_tac`(MAP (��st,e. (st,Assign s e)) tr)`>> 812 fs[HD_MAP,LAST_MAP,is_val_e_def,no_step_e_assign,check_trace_assign])) 813 >- 814 (Cases_on`getchar s.input`>>fs[LET_THM,res_rel_e_cases]>> 815 qpat_abbrev_tac`t = (A,B)`>> 816 qpat_abbrev_tac`t' = (A,B)`>> 817 qexists_tac`[t;t']`>>unabbrev_all_tac>>fs[check_trace_def]>> 818 match_mp_tac some_to_SOME_step_e>> 819 simp[Once step_e_cases]) 820 >- 821 (first_x_assum(qspec_then`s` assume_tac)>>fs[]>> 822 Cases_on`sem_e s e`>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout]>> 823 qpat_abbrev_tac`t = (A,B)`>> 824 qpat_abbrev_tac`t' = (A,B)` 825 >- 826 (qexists_tac`MAP (��st,e. (st,Putchar e)) tr ++ [(r with <|io_trace := r.io_trace ++ [INL(Otag i)];clock:=0|>,Num i)]`>> 827 fs[HD_MAP,HD_APPEND,Abbr`t'`,res_rel_e_cases]>> 828 ho_match_mp_tac check_trace_append2>> 829 fs[check_trace_def,LAST_MAP,check_trace_putchar]>> 830 ntac 2 (simp[Once step_e_cases])) 831 >> 832 qexists_tac`MAP (��st,e. (st,Putchar e)) tr`>>unabbrev_all_tac>> 833 fs[HD_MAP,res_rel_e_cases,LAST_MAP,is_val_e_def,check_trace_putchar,no_step_e_putchar])) 834end 835 836val sem_t_for_no_break = Q.prove( 837 `���s s'. sem_t s (For e1 e2 t) ��� (Rbreak,s')`, 838 completeInduct_on`s.clock`>>fs[sem_t_def_with_stop]>> 839 rw[]>>fct>>Cases_on`q`>> 840 fs[sem_e_not_break,sem_e_not_timeout]>> 841 IF_CASES_TAC>>fs[]>> 842 fct>>Cases_on`q`>>fs[]>> 843 fct>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout]>> 844 imp_res_tac sem_e_clock>>imp_res_tac sem_t_clock>>fs[]>> 845 IF_CASES_TAC>>fs[dec_clock_def]>> 846 simp[STOP_def]>> 847 simp[sem_t_def_with_stop]>> 848 fs[PULL_FORALL]>> 849 first_x_assum(qspec_then `r'' with clock := r''.clock-1` mp_tac)>> 850 fs[]>> 851 `r''.clock < 1 + r.clock ��� 0 < r.clock` by 852 DECIDE_TAC>> 853 fs[dec_clock_def]) 854 855val step_e_clock = Q.prove(` 856 ���se l1 se'. 857 step_e se l1 se' ��� 858 ���s e s' e'. 859 se = (s,e) ��� 860 se' = (s',e') ��� 861 (���c. 862 step_e (s with clock:=c,e) l1 (s' with clock:=c,e'))`, 863 ho_match_mp_tac step_e_strongind>>rw[]>> 864 simp[Once step_e_cases]) 865 866val step_e_zero_clock = Q.prove( 867 `(���s e l. ��step_e (r,e') l (s,e))��� 868 ���s e l. ��step_e (r with clock:=0,e') l (s,e)`, 869 rw[]>>CCONTR_TAC>>fs[]>>imp_res_tac step_e_clock>>fs[]>> 870 pop_assum(qspec_then`r.clock`assume_tac)>>fs[]>> 871 `r with clock:= r.clock = r` by fs[state_component_equality]>> 872 metis_tac[]) 873 874local val rw = srw_tac[] val fs = fsrw_tac[] in 875val big_small_lem = Q.prove ( 876`!s t r. 877 sem_t s t = r 878 ��� 879 ?tr. 880 tr ��� [] ��� 881 s.clock - (SND r).clock ��� LENGTH tr ��� 882 check_trace (\st. some st'. ?l. step_t st l st') tr ��� 883 HD tr = (s with clock := 0, (t_to_small_t t)) ��� 884 res_rel_t r (LAST tr)`, 885 ho_match_mp_tac sem_t_ind >> 886 rw [sem_t_def_with_stop, t_to_small_t_def] 887 >- 888 (qabbrev_tac`r = sem_e s e`>>fs[markerTheory.Abbrev_def]>> 889 pop_assum (assume_tac o SYM)>> 890 imp_res_tac sem_e_big_small_lem>> 891 Cases_on`r`>> 892 qexists_tac`MAP (��st,e. (st,Exp e)) tr`>> 893 imp_res_tac sem_e_clock>>fs[HD_MAP,LAST_MAP]>> 894 CONJ_TAC>- 895 fs[check_trace_exp] 896 >> 897 fs[res_rel_t_cases,res_rel_e_cases,is_val_t_def]>> 898 imp_res_tac step_e_zero_clock>> 899 fs[Once step_t_cases]) 900 >- 901 (qpat_abbrev_tac`A = (s with clock:=0,D)`>> 902 qexists_tac`A::tr`>>fs[Abbr`A`,check_trace_def]>> 903 CONJ_TAC >- DECIDE_TAC>> 904 CONJ_TAC >- 905 (Cases_on`tr`>> 906 simp[check_trace_def,optionTheory.some_def]>> 907 ntac 2 (simp[Once step_t_cases])>> 908 fs[])>> 909 fs[LAST_DEF]) 910 >- 911 (qexists_tac`[s with clock:=0,Break]`>> 912 fs[res_rel_t_cases,check_trace_def]) 913 >- 914 (EVERY_CASE_TAC>>fs[] 915 >- 916 (qpat_abbrev_tac`p = t_to_small_t t'`>> 917 qexists_tac`MAP (��st,t. (st,Seq t p)) tr ++ tr'`>> 918 fs[HD_MAP,HD_APPEND,LAST_APPEND]>>rw[] 919 >- 920 DECIDE_TAC 921 >- 922 (match_mp_tac check_trace_append2>> 923 fs[check_trace_seq,LAST_MAP]>> 924 Cases_on`LAST tr`>>fs[]>> 925 match_mp_tac some_to_SOME_step_t>> 926 simp[Once step_t_cases]>>fs[Abbr`p`,res_rel_t_cases]>> 927 metis_tac[])) 928 >- 929 (qpat_abbrev_tac `p = t_to_small_t t'`>> 930 qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)++[r with clock:=0,Break]`>> 931 fs[HD_APPEND,HD_MAP]>>rw[] 932 >- 933 DECIDE_TAC 934 >- 935 (match_mp_tac check_trace_append2>> 936 fs[check_trace_seq,LAST_MAP,check_trace_def]>> 937 fs[res_rel_t_cases]>> 938 match_mp_tac some_to_SOME_step_t>> 939 simp[Once step_t_cases]>>fs[Abbr`p`,res_rel_t_cases]) 940 >- 941 fs[Once res_rel_t_cases]) 942 >- 943 (qpat_abbrev_tac `p = t_to_small_t t'`>> 944 qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)`>> 945 fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>> 946 fs[Once res_rel_t_cases,LAST_MAP]>> 947 `step_t (r,Seq t'' p) l (s',Seq t''' p)` by 948 simp[Once step_t_cases]>> 949 metis_tac[]) 950 >- 951 (qpat_abbrev_tac `p = t_to_small_t t'`>> 952 qexists_tac`(MAP (��st,t. (st,Seq t p)) tr)`>> 953 fs[HD_APPEND,HD_MAP,check_trace_def,check_trace_seq]>>rw[]>> 954 fs[Once res_rel_t_cases,LAST_MAP,is_val_t_def]>> 955 metis_tac[no_step_t_seq])) 956 >- 957 (EVERY_CASE_TAC>>fs[sem_e_not_break,sem_e_not_timeout]>> 958 imp_res_tac sem_e_big_small_lem>> 959 imp_res_tac sem_e_clock>> 960 qpat_abbrev_tac`p1 = t_to_small_t t1`>> 961 qpat_abbrev_tac`p2 = t_to_small_t t2`>> 962 TRY 963 (qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr') ++ tr`>> 964 fs[HD_MAP,HD_APPEND,LAST_MAP,LAST_APPEND]>>rw[] 965 >- 966 DECIDE_TAC 967 >> 968 match_mp_tac check_trace_append2>>fs[res_rel_e_cases]>>CONJ_TAC 969 >- 970 metis_tac[check_trace_if1] 971 >> 972 match_mp_tac some_to_SOME_step_t>>fs[LAST_MAP]>> 973 simp[Once step_t_cases]>> 974 metis_tac[]) 975 >> 976 qexists_tac`(MAP (��st,e. (st,(If e p1 p2))) tr)`>>rw[]>> 977 fs[HD_MAP,res_rel_t_cases,LAST_MAP,res_rel_e_cases,is_val_t_def,check_trace_if1,no_step_t_if1]>> 978 metis_tac[check_trace_if1,no_step_t_if1,step_e_zero_clock]) 979 >- (*For*) 980 (Cases_on`sem_e s e1`>>Cases_on`q`>>fs[sem_e_not_break,sem_e_not_timeout]>> 981 qpat_abbrev_tac`e1s = e_to_small_e e1`>> 982 qpat_abbrev_tac`e2s = e_to_small_e e2`>> 983 (*trace for e1*) 984 imp_res_tac sem_e_big_small_lem>> 985 imp_res_tac sem_e_clock>> 986 qpat_abbrev_tac`p = t_to_small_t t`>> 987 qabbrev_tac`e1tr = (MAP (��st,e. (st,Handle (If e (Seq p (Seq (Exp e2s) (For e1s e2s p))) (Exp (Num 0))))) tr)`>> 988 `check_trace (��st. some st'. ���l. step_t st l st') e1tr` by metis_tac[check_trace_for1]>> 989 qabbrev_tac`ls = [s with clock:=0,For e1s e2s p]`>> 990 `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr)` by 991 (match_mp_tac check_trace_append2>>unabbrev_all_tac>> 992 fs[check_trace_def,HD_MAP]>> 993 match_mp_tac some_to_SOME_step_t>> 994 simp[Once step_t_cases]) 995 >- 996 (IF_CASES_TAC>>fs[] 997 >- 998 (*run out of time*) 999 (fs[res_rel_t_cases,res_rel_e_cases]>> 1000 qexists_tac` (ls ++ e1tr) 1001 ++ [(r with clock:=0,Handle (Exp (Num 0)));(r with clock:=0,Exp (Num 0))]`>> 1002 fs[LAST_APPEND,LAST_MAP]>>fs[]>>rw[] 1003 >- 1004 (match_mp_tac check_trace_append2>>rw[] 1005 >- 1006 (fs[check_trace_def]>> 1007 match_mp_tac some_to_SOME_step_t>> 1008 simp[Once step_t_cases,is_val_e_def,is_val_t_def]) 1009 >- 1010 (unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP]>> 1011 match_mp_tac some_to_SOME_step_t>> 1012 ntac 2 (simp[Once step_t_cases]))) 1013 >> 1014 unabbrev_all_tac>>fs[HD_APPEND]) 1015 >> 1016 Cases_on`sem_t r t`>>Cases_on`q`>>fs[]>> 1017 qabbrev_tac`ttr = (MAP (��st,t. (st,Handle (Seq t (Seq (Exp e2s) (For e1s e2s p))) ))) tr'`>> 1018 `check_trace (��st. some st'. ���l. step_t st l st') ttr` by 1019 metis_tac[check_trace_for2]>> 1020 `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr++ttr)` by 1021 (match_mp_tac check_trace_append2>> 1022 fs[]>> unabbrev_all_tac>> 1023 fs[LAST_MAP,res_rel_e_cases,HD_MAP,LAST_DEF]>> 1024 match_mp_tac some_to_SOME_step_t>> 1025 ntac 2 (simp[Once step_t_cases])) 1026 >- 1027 (*continue executing*) 1028 (Cases_on`sem_e r' e2`>>Cases_on`q`>> 1029 fs[sem_e_not_break,sem_e_not_timeout]>> 1030 imp_res_tac sem_e_big_small_lem>> 1031 imp_res_tac sem_e_clock>> 1032 qabbrev_tac`e2tr = (MAP (��st,e. (st,Handle (Seq (Exp e) (For e1s e2s p)) ))) tr''`>> 1033 `check_trace (��st. some st'. ���l. step_t st l st') e2tr` by 1034 metis_tac[check_trace_for3]>> 1035 `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr++ttr++e2tr)` by 1036 (match_mp_tac check_trace_append2>>fs[]>> 1037 match_mp_tac some_to_SOME_step_t>> 1038 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,HD_MAP,res_rel_t_cases]>> 1039 ntac 2 (simp[Once step_t_cases,res_rel_e_cases])) 1040 >- 1041 (*e2 ok*) 1042 (IF_CASES_TAC>>fs[] 1043 >- 1044 (*clock ok*) 1045 (simp[STOP_def]>> 1046 simp[Once sem_t_def_with_stop]>> 1047 fs[dec_clock_def]>> 1048 (*Need a handle wrapper around rest of trace*) 1049 qabbrev_tac`ftr = MAP (��st,t. (st, Handle t))tr''''` >> 1050 `check_trace (��st. some st'. ���l. step_t st l st') ftr` by 1051 metis_tac[check_trace_handle]>> 1052 `check_trace (��st. some st'. ���l. step_t st l st') (ls++e1tr++ttr++e2tr++ftr)` by 1053 (match_mp_tac check_trace_append2>>fs[]>> 1054 match_mp_tac some_to_SOME_step_t>> 1055 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,HD_MAP]>> 1056 fs[res_rel_e_cases]>> 1057 ntac 2 (simp[Once step_t_cases]))>> 1058 fs[res_rel_t_cases] 1059 (*Case split on the rest of loop*) 1060 >- 1061 (qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr ++[s' with clock:=0,Exp (Num i''')]`>>fs[]>>rw[]>> 1062 TRY 1063 (unabbrev_all_tac>>fs[]>> 1064 DECIDE_TAC) 1065 >- 1066 (match_mp_tac check_trace_append2>>fs[check_trace_def]>> 1067 match_mp_tac some_to_SOME_step_t>>unabbrev_all_tac>> 1068 fs[LAST_DEF,LAST_APPEND,LAST_MAP,res_rel_e_cases]>> 1069 simp[Once step_t_cases,is_val_t_def,is_val_e_def]) 1070 >> 1071 simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def]) 1072 >- 1073 (qexists_tac`ls ++ e1tr++ttr++e2tr++ftr`>>fs[]>>rw[]>> 1074 TRY(unabbrev_all_tac>>fs[]>>DECIDE_TAC)>> 1075 ntac 4 (simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def])>> 1076 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,is_val_t_def]>> 1077 match_mp_tac no_step_t_handle>> 1078 metis_tac[]) 1079 >- 1080 (*break never occurs*) 1081 (qpat_assum `A = (RBreak,s')` mp_tac>> 1082 fct>>Cases_on`q`>> 1083 fs[sem_e_not_timeout,sem_e_not_break]>> 1084 IF_CASES_TAC>>fs[]>> 1085 fct>>Cases_on`q`>> 1086 fs[]>> 1087 fct>>Cases_on`q`>> 1088 fs[sem_e_not_timeout,sem_e_not_break]>> 1089 IF_CASES_TAC>>fs[]>> 1090 simp[STOP_def]>> 1091 metis_tac[sem_t_for_no_break]) 1092 >> 1093 (qexists_tac`ls ++ e1tr ++ ttr ++ e2tr ++ ftr`>>fs[]>>rw[]>> 1094 TRY 1095 (unabbrev_all_tac>>fs[]>> 1096 DECIDE_TAC) 1097 >> 1098 unabbrev_all_tac>> 1099 ntac 3 (simp[Once sem_t_def_with_stop,LAST_APPEND,dec_clock_def,LAST_MAP])>> 1100 simp[Once step_t_cases]>>metis_tac[])) 1101 >> 1102 (*clock ended*) 1103 fs[res_rel_t_cases]>> 1104 qexists_tac`ls++e1tr++ttr++e2tr`>>fs[]>>rw[]>> 1105 TRY (unabbrev_all_tac>>fs[]>>DECIDE_TAC)>> 1106 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,res_rel_e_cases]>> 1107 `r'' with clock:=0 = r''` by fs[state_component_equality]>> 1108 ntac 2 (simp[Once step_t_cases,is_val_t_def])>> 1109 metis_tac[]) 1110 >> 1111 (*e2 fails*) 1112 (qexists_tac`ls++e1tr++ttr++e2tr`>>fs[res_rel_e_cases]>> 1113 unabbrev_all_tac>> 1114 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases,is_val_t_def]>>rw[] 1115 >- 1116 DECIDE_TAC 1117 >> 1118 imp_res_tac step_e_zero_clock>> 1119 metis_tac[no_step_t_exp,no_step_t_handle 1120 ,no_step_t_seq,is_val_t_def])) 1121 >- 1122 (qexists_tac`ls++e1tr++ttr++[(r' with clock:= 0,Handle Break);(r' with clock:=0,Exp (Num 0))]`>> 1123 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>rw[]>> 1124 TRY(unabbrev_all_tac>>fs[]>>DECIDE_TAC)>> 1125 match_mp_tac check_trace_append2>>fs[check_trace_def]>>CONJ_TAC>> 1126 match_mp_tac some_to_SOME_step_t>> 1127 unabbrev_all_tac>>fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>> 1128 ntac 2 (simp[Once step_t_cases])) 1129 >- 1130 (qexists_tac`ls++e1tr++ttr`>>unabbrev_all_tac>> 1131 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>CONJ_TAC 1132 >- 1133 DECIDE_TAC 1134 >> 1135 ntac 2 (simp[Once step_t_cases,is_val_t_def])>> 1136 metis_tac[]) 1137 >> 1138 (qexists_tac`ls++e1tr++ttr`>>unabbrev_all_tac>> 1139 fs[LAST_APPEND,LAST_MAP,res_rel_t_cases]>>CONJ_TAC 1140 >- 1141 DECIDE_TAC 1142 >> 1143 fs[is_val_t_def]>>match_mp_tac no_step_t_handle>> 1144 fs[is_val_t_def]>>match_mp_tac no_step_t_seq>> 1145 metis_tac[])) 1146 >> 1147 (*e1 fails, expand it 1 step*) 1148 qexists_tac` ls ++ e1tr`>> 1149 unabbrev_all_tac>>fs[res_rel_t_cases,LAST_DEF,LAST_MAP,HD_APPEND]>> 1150 fs[LAST_APPEND,LAST_MAP,res_rel_e_cases,is_val_t_def]>> 1151 match_mp_tac no_step_t_handle>>fs[is_val_t_def]>> 1152 imp_res_tac step_e_zero_clock>> 1153 metis_tac[no_step_t_if1])) 1154end 1155 1156val big_timeout_0 = Q.prove ( 1157`!st p r. 1158 sem_t st p = (Rtimeout,r) 1159 ��� 1160 r.clock = 0`, 1161 ho_match_mp_tac sem_t_ind >> 1162 conj_tac >- ( 1163 rw [sem_t_def_with_stop, sem_e_not_timeout]) >> 1164 conj_tac >- ( 1165 rw [sem_t_def_with_stop, sem_e_not_timeout]) >> 1166 conj_tac >- ( 1167 rw [sem_t_def_with_stop, sem_e_not_timeout] >> 1168 ect >> fs []) >> 1169 conj_tac >- ( 1170 rw [sem_t_def_with_stop, sem_e_not_timeout] >> 1171 ect >> fs []) >> 1172 conj_tac >- ( 1173 rw [sem_t_def_with_stop, sem_e_not_timeout] >> 1174 ect >> fs [sem_e_not_timeout]) 1175 >- ( 1176 rw [] >> 1177 pop_assum mp_tac >> 1178 simp [sem_t_def_with_stop] >> 1179 ect >> 1180 fs [sem_e_not_timeout, STOP_def] >> 1181 rw [] >> 1182 fs [])); 1183 1184(* check traces are unique up to prefixing *) 1185val check_trace_determ = Q.prove( 1186`���tr h f. 1187 check_trace f (h::tr) ��� 1188 ���tr'. 1189 LENGTH tr' ��� LENGTH tr ��� 1190 check_trace f (h::tr') ��� 1191 isPREFIX tr' tr`, 1192 Induct>>rw[]>>fs[check_clock_def,isPREFIX,LENGTH_NIL]>> 1193 Cases_on`tr'`>>fs[check_trace_def]>> 1194 metis_tac[]) 1195 1196val check_trace_prefixes = Q.prove( 1197`���tr f. 1198 tr ��� [] ��� 1199 check_trace f tr ��� 1200 ���tr'. 1201 tr' ��� [] ��� HD tr' = HD tr ��� 1202 check_trace f tr' ��� 1203 isPREFIX tr tr' ��� isPREFIX tr' tr`, 1204 rw[]>> 1205 Cases_on`tr`>>Cases_on`tr'`>>fs[]>> 1206 Cases_on`LENGTH t' ��� LENGTH t`>> 1207 TRY(`LENGTH t ��� LENGTH t'` by DECIDE_TAC)>> 1208 metis_tac[check_trace_determ]) 1209 1210val check_trace_TL = Q.prove( 1211`���tr tr'. 1212 (tr ��� [] ��� 1213 check_trace (��st. some st'. ?l. step_t st l st') tr ��� 1214 (���l t'. ��step_t (LAST tr) l t') ��� 1215 check_trace (��st. some st'. ?l. step_t st l st') tr' ��� 1216 isPREFIX tr tr') ��� 1217 tr = tr'`, 1218 Induct>>fs[check_trace_def,LAST_DEF]>>rw[]>>Cases_on`tr'`>>fs[] 1219 >- 1220 (Cases_on`t`>>fs[check_trace_def,some_def]>> 1221 metis_tac[]) 1222 >> 1223 Cases_on`tr`>>Cases_on`t`>>fs[check_trace_def]>> 1224 res_tac>>fs[]) 1225 1226val prefix_append = Q.prove( 1227`���ls ls'. 1228 ls ��� ls' ��� 1229 ���ls''. ls++ls'' = ls'`, 1230 metis_tac[rich_listTheory.IS_PREFIX_APPEND]) 1231 1232val res_rel_t_io_trace = Q.prove( 1233 `res_rel_t (q,r) s ��� 1234 r.io_trace = (FST s).io_trace`, 1235 simp[res_rel_t_cases]>>rw[]>>fs[]) 1236 1237(*slow*) 1238val res_rel_t_clock = Q.prove( 1239 `res_rel_t (q,r) s ��� 1240 step_t s l t ��� 1241 q = Rtimeout ��� (FST s).clock = 0`, 1242 simp[res_rel_t_cases]>>rw[] 1243 >> 1244 fs[Once step_t_cases,Once step_e_cases] 1245 >> 1246 metis_tac[PAIR,FST]) 1247 1248val step_e_io_mono = Q.prove( 1249`���s l s'. 1250 step_e s l s' ��� 1251 (FST s).io_trace ��� (FST s').io_trace`, 1252 ho_match_mp_tac step_e_strongind>>fs[]) 1253 1254val step_t_io_mono = Q.prove( 1255`���s l s'. 1256 step_t s l s' ��� 1257 (FST s).io_trace ��� (FST s').io_trace`, 1258 ho_match_mp_tac step_t_strongind>> 1259 fs[]>>metis_tac[step_e_io_mono,FORALL_PROD,FST]) 1260 1261val RTC_step_t_io_mono = Q.prove( 1262 `���x y. (��s1 s2. (some st'. ���l. step_t s1 l st') = SOME s2)^* x y ��� 1263 (FST x).io_trace ��� (FST y).io_trace`, 1264 ho_match_mp_tac RTC_INDUCT >> rw[] >> 1265 last_x_assum mp_tac >> 1266 DEEP_INTRO_TAC some_intro >> rw[] >> 1267 metis_tac[step_t_io_mono,IS_PREFIX_TRANS]) 1268 1269val check_trace_io_trace = Q.prove( 1270 `���tr ls. 1271 tr ��� [] ��� check_trace (��st. some st'. ���l. step_t st l st') (tr ++ ls) ��� 1272 (FST(LAST tr)).io_trace ��� 1273 (FST(LAST (tr++ls))).io_trace`, 1274 rw[] >> 1275 match_mp_tac RTC_step_t_io_mono >> 1276 simp[check_trace_thm] >> 1277 qexists_tac`LAST tr::ls` >> 1278 simp[] >> 1279 conj_tac >- ( Cases_on`ls`>>simp[] ) >> 1280 `LAST tr::ls = DROP (LENGTH tr - 1) (tr++ls)` suffices_by ( 1281 disch_then SUBST1_TAC >> 1282 match_mp_tac check_trace_drop >> simp[] ) >> 1283 simp[DROP_APPEND1] >> 1284 Q.ISPECL_THEN[`1n`,`tr`]mp_tac (GSYM LASTN_DROP) >> 1285 `1 ��� LENGTH tr` by ( 1286 Cases_on`tr`>>fs[] >> simp[] ) >> 1287 simp[] >> 1288 Q.ISPEC_THEN`tr`FULL_STRUCT_CASES_TAC SNOC_CASES >- fs[] >> 1289 REWRITE_TAC[arithmeticTheory.ONE,LASTN,LAST,SNOC]) 1290 1291val sem_e_ignores_clock = Q.prove( 1292 `���s e c r s'. 1293 sem_e s e = (r,s') ��� 1294 sem_e (s with clock:=c) e = (r,s' with clock:=c)`, 1295 ho_match_mp_tac sem_e_ind>>srw_tac[][sem_e_def]>>fs[LET_THM] 1296 >- 1297 (ect>>fs[]) 1298 >- 1299 (fs[permute_pair_def,LET_THM,oracle_get_def,unpermute_pair_def]>> 1300 Cases_on`switch`>>fs[]>> 1301 qpat_assum`A=(r,s')` mp_tac>> 1302 fct>>Cases_on`q`>>res_tac>> 1303 fs[sem_e_not_break,sem_e_not_timeout]>> 1304 fct>>Cases_on`q`>>res_tac>> 1305 rw[]>> 1306 fs[sem_e_not_break,sem_e_not_timeout]) 1307 >> 1308 Cases_on`sem_e s e`>>res_tac>>fs[]>> 1309 Cases_on`q`>>fs[state_component_equality]) 1310 1311val sem_e_io_mono = Q.prove( 1312 `���s e c. 1313 (SND (sem_e s e)).io_trace ��� 1314 (SND (sem_e (s with clock:= c) e)).io_trace`, 1315 rw[]>>Cases_on`sem_e s e`>>imp_res_tac sem_e_ignores_clock>> 1316 fs[]) 1317 1318val sem_e_clock_inc = Q.prove( 1319 `���s e r. 1320 sem_e s e = r ��� 1321 ���k. sem_e (s with clock:= s.clock+k) e =(FST r,(SND r)with clock:= (SND r).clock+k)`, 1322 metis_tac[sem_e_ignores_clock,sem_e_clock,FST,SND,PAIR]) 1323 1324val sem_t_clock_inc = Q.prove( 1325 `���s t r. 1326 sem_t s t = r ��� FST r ��� Rtimeout ��� 1327 ���k. sem_t (s with clock:= s.clock+k) t =(FST r,(SND r)with clock:= (SND r).clock+k)`, 1328 ho_match_mp_tac sem_t_ind>>rw[]>>fs[sem_e_clock]>> 1329 TRY(fs[sem_t_def_with_stop]>>NO_TAC) 1330 >- 1331 (fs[sem_t_def_with_stop]>> 1332 Cases_on`sem_e s e`>> 1333 imp_res_tac sem_e_ignores_clock>> 1334 fs[]>>metis_tac[sem_e_clock]) 1335 >- 1336 (fs[sem_t_def_with_stop]>>Cases_on`sem_t s t`>>Cases_on`q`>>fs[]) 1337 >- 1338 (fs[sem_t_def_with_stop]>>Cases_on`sem_e s e`>>Cases_on`q`>>fs[sem_e_res]>> 1339 imp_res_tac sem_e_clock_inc>> 1340 pop_assum(qspec_then`k` assume_tac)>>fs[]>> 1341 IF_CASES_TAC>>fs[]) 1342 >> 1343 pop_assum mp_tac>> 1344 simp[sem_t_def_with_stop]>> 1345 Cases_on`sem_e s e1`>>Cases_on`q`>>fs[]>> 1346 imp_res_tac sem_e_clock_inc>>fs[]>> 1347 TRY(pop_assum(qspec_then`k` assume_tac))>> 1348 fs[DECIDE ``(A:num)+B = B+A``]>> 1349 IF_CASES_TAC>>fs[]>> 1350 Cases_on`sem_t r t`>>Cases_on`q`>>fs[]>> 1351 Cases_on`sem_e r' e2`>>Cases_on`q`>>fs[]>> 1352 TRY(metis_tac[sem_e_res])>> 1353 imp_res_tac sem_e_clock_inc>>fs[]>> 1354 TRY(pop_assum(qspec_then`k` assume_tac))>> 1355 fs[DECIDE ``(A:num)+B = B+A``]>> 1356 IF_CASES_TAC>>fs[]>>rw[]>> 1357 fs[dec_clock_def,STOP_def]>> 1358 `1 ��� r''.clock` by DECIDE_TAC>> 1359 metis_tac[arithmeticTheory.LESS_EQ_ADD_SUB]) 1360 1361val check_trace_io_trace_simp = Q.prove( 1362 `tr ��� [] ��� 1363 check_trace (��st.some st'. ���l. step_t st l st') tr ��� 1364 (FST(HD tr)).io_trace ��� (FST (LAST tr)).io_trace`, 1365 Cases_on`tr`>>rw[]>> 1366 `FST h = FST(LAST [h])` by fs[]>> 1367 pop_assum SUBST1_TAC>> 1368 `h::t = [h]++t` by fs[]>> 1369 pop_assum SUBST1_TAC>> 1370 ho_match_mp_tac check_trace_io_trace>> 1371 rw[]) 1372 1373val sem_t_sing_io_mono = Q.prove( 1374 `���s t res s'. 1375 sem_t s t = (res,s') ��� 1376 s.io_trace ��� s'.io_trace`, 1377 rw[]>>imp_res_tac big_small_lem>> 1378 imp_res_tac check_trace_io_trace_simp>> 1379 fs[res_rel_t_cases]>> 1380 rfs[]) 1381 1382val sem_e_sing_io_mono = Q.prove( 1383`���s e res s'. 1384 sem_e s e = (res,s') ��� 1385 s.io_trace ��� s'.io_trace`, 1386 CCONTR_TAC>>fs[]>> 1387 `sem_t s (Exp e) = (res,s')` by 1388 fs[sem_t_def_with_stop]>> 1389 metis_tac[sem_t_sing_io_mono]) 1390 1391(* Monotonicity of io_trace w.r.t. to clock *) 1392val sem_t_io_mono_lem = Q.prove( 1393 `���s t k. 1394 (SND (sem_t s t)).io_trace ��� 1395 (SND (sem_t (s with clock:=s.clock+k) t)).io_trace`, 1396 ho_match_mp_tac sem_t_ind>>rw[]>> 1397 TRY(fs[sem_t_def_with_stop,sem_e_io_mono]>>NO_TAC) 1398 >- 1399 (fs[sem_t_def_with_stop]>> 1400 fct>>Cases_on`q`>>fs[]>> 1401 imp_res_tac sem_t_clock_inc>>fs[]>> 1402 fct>>Cases_on`q`>>fs[]>> 1403 first_x_assum(qspec_then`k` assume_tac)>>rfs[]>> 1404 Cases_on`sem_t r' t'`>> 1405 imp_res_tac sem_t_sing_io_mono>> 1406 fs[]>> 1407 metis_tac[IS_PREFIX_TRANS]) 1408 >- 1409 (fs[sem_t_def_with_stop]>> 1410 fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>> 1411 imp_res_tac sem_e_clock_inc>>fs[]>> 1412 IF_CASES_TAC>>fs[]) 1413 >> 1414 simp[Once sem_t_def_with_stop]>> 1415 simp[Once sem_t_def_with_stop]>> 1416 fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>> 1417 imp_res_tac sem_e_clock_inc>> 1418 pop_assum(qspec_then`k` assume_tac)>> 1419 fs[DECIDE ``(A:num)+B = B+A``]>> 1420 IF_CASES_TAC>>fs[]>> 1421 fct>>Cases_on`q`>>fs[]>> 1422 TRY(imp_res_tac sem_t_clock_inc>>fs[]>> 1423 pop_assum(qspec_then`k` assume_tac))>>rfs[]>> 1424 fs[DECIDE ``(A:num)+B = B+A``] 1425 >- 1426 (fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>> 1427 imp_res_tac sem_e_clock_inc>> 1428 pop_assum(qspec_then`k` assume_tac)>> 1429 fs[DECIDE ``(A:num)+B = B+A``]>> 1430 IF_CASES_TAC>>fs[] 1431 >- 1432 (fs[dec_clock_def,STOP_def]>> 1433 `1 ��� r''.clock` by DECIDE_TAC>> 1434 metis_tac[arithmeticTheory.LESS_EQ_ADD_SUB]) 1435 >> 1436 IF_CASES_TAC>>fs[]>> 1437 qpat_abbrev_tac`A = sem_t B C`>> 1438 Cases_on`A`>>fs[markerTheory.Abbrev_def]>> 1439 pop_assum (assume_tac o SYM)>>imp_res_tac sem_t_sing_io_mono>> 1440 fs[dec_clock_def]) 1441 >> 1442 first_x_assum(qspec_then`k` assume_tac)>> 1443 fct>>Cases_on`q`>>fs[]>> 1444 fct>>Cases_on`q`>>fs[]>>TRY(metis_tac[sem_e_res])>> 1445 imp_res_tac sem_e_sing_io_mono 1446 >- 1447 (IF_CASES_TAC>>fs[dec_clock_def]>> 1448 TRY(qpat_abbrev_tac`A = sem_t B C`>> 1449 Cases_on`A`>>fs[markerTheory.Abbrev_def]>> 1450 pop_assum (assume_tac o SYM)>>imp_res_tac sem_t_sing_io_mono)>> 1451 fs[]>>metis_tac[IS_PREFIX_TRANS]) 1452 >> 1453 metis_tac[IS_PREFIX_TRANS]) 1454 1455val sem_t_io_mono = Q.prove ( 1456`k1 ��� k2 ��� 1457 (SND (sem_t (init_st 0 nd input with clock := k1) p)).io_trace ��� 1458 (SND (sem_t (init_st 0 nd input with clock := k2) p)).io_trace`, 1459 qpat_abbrev_tac `st = init_st A B C`>> 1460 rw[]>>imp_res_tac arithmeticTheory.LESS_EQUAL_ADD >> 1461 Q.ISPECL_THEN [`st with clock:=k1`,`p`,`p'`] assume_tac sem_t_io_mono_lem>> 1462 fs[]) 1463 1464val sem_equiv_lem = Q.store_thm ("sem_equiv_lem", 1465`���input prog r. ofbs_sem (for_big_sem input) prog r ��� osmall_sem (for_small_sem input) prog r`, 1466 gen_tac >> 1467 match_mp_tac osmall_fbs_equiv2 >> 1468 conj_tac >- ( 1469 rw [for_small_sem_def] >> 1470 match_mp_tac step_t_io_mono>> 1471 Q.ISPEC_THEN `��st. ���l. step_t s1 l st` assume_tac some_SAT>> 1472 fs[ETA_AX])>> 1473 conj_tac >- ( 1474 rw [for_big_sem_def] >> 1475 rw [eval_with_clock_def, for_eval_def] >> 1476 every_case_tac >> 1477 fs [] >> 1478 metis_tac [sem_t_io_mono, SND]) >> 1479 conj_tac >- ( 1480 rw [for_big_sem_def, eval_with_clock_def, for_eval_def] >> 1481 ect >> 1482 fs [] >> 1483 metis_tac [big_timeout_0]) >> 1484 qexists_tac `I` >> 1485 conj_tac 1486 >- ( 1487 rw [unbounded_def] >> 1488 qexists_tac `SUC x` >> 1489 simp []) >> 1490 rpt gen_tac >> 1491 simp [for_big_sem_def, for_eval_def, eval_with_clock_def] >> 1492 DISCH_TAC >> 1493 ect >> 1494 imp_res_tac big_small_lem >> 1495 fs [] >> 1496 qexists_tac `tr` >> 1497 fs [for_small_sem_def] >> 1498 rw [same_result_def] >> 1499 fs [res_rel_t_cases, is_val_t_def, is_val_e_def, some_no_choice, init_st_def] >> 1500 simp [] >> 1501 rw [] 1502 >- (rw [Once step_t_cases] >> 1503 rw [Once step_e_cases]) 1504 >- rw [Once step_t_cases] 1505 >- (rw [some_def] >> 1506 metis_tac []) 1507 >- metis_tac [PAIR]); 1508 1509val FST_SPLIT = Q.prove( 1510`FST x = y ��� ���z. x = (y,z)`, 1511Cases_on`x`>>fs[]) 1512 1513val big_val_no_errors = Q.prove( 1514`!st p v s. 1515 sem_t st p = (Rval v,s) 1516 ��� 1517 (���c. 1518 (FST (sem_t (st with clock:= c) p) ��� Rbreak) 1519 ��� (FST (sem_t (st with clock:=c) p) ��� Rfail))`, 1520 rw[]>>CCONTR_TAC>>fs[]>>imp_res_tac FST_SPLIT>> 1521 imp_res_tac big_small_lem>> 1522 `HD tr = HD tr'` by fs[]>> 1523 fs[res_rel_t_cases]>> 1524 `���l t'. ��step_t (LAST tr) l t'` by 1525 fs[Once step_t_cases,FORALL_PROD]>> 1526 `���l t'. ��step_t (LAST tr') l t'` by 1527 fs[Once step_t_cases,FORALL_PROD,Once step_e_cases]>> 1528 `isPREFIX tr tr' ��� isPREFIX tr' tr` by 1529 metis_tac[check_trace_prefixes]>> 1530 `tr = tr'` by metis_tac[check_trace_TL]>> 1531 fs[]>> 1532 qpat_assum`A=t` (SUBST_ALL_TAC o SYM)>>fs[is_val_t_def,is_val_e_def]) 1533 1534(* we can prove an alternative characterisation of the semantics, now that we 1535 know sem_t's io_trace is a chain *) 1536 1537val over_all_def = Define`over_all f = GSPEC (��c. f c,T)`; 1538 1539val init_st_with_clock = Q.prove( 1540 `init_st a b c with clock := d = init_st d b c`, 1541 EVAL_TAC) 1542 1543val prefix_chain_sem_t_io_trace_over_all_c = Q.store_thm("lprefix_chain_sem_t_io_trace_over_all_c", 1544 `prefix_chain (over_all (��c. (SND (sem_t (init_st c nd input) t)).io_trace))`, 1545 rw[lprefix_lubTheory.prefix_chain_def,over_all_def] >> 1546 qspecl_then[`c`,`c'`]strip_assume_tac arithmeticTheory.LESS_EQ_CASES >|[disj1_tac,disj2_tac] >> 1547 imp_res_tac sem_t_io_mono >> fs[init_st_with_clock]) 1548 1549val image_intro = Q.prove( 1550 `{fromList (FILTER P (Q c)) | c | T} = IMAGE fromList (IMAGE (FILTER P) (over_all Q))`, 1551 rw[EXTENSION,over_all_def,PULL_EXISTS]) 1552 1553val IMAGE_over_all = Q.store_thm("IMAGE_over_all", 1554 `IMAGE P (over_all f) = over_all (P o f)`, 1555 rw[EXTENSION,over_all_def,PULL_EXISTS]) 1556 1557(* Pretty Printing *) 1558val BIGSUP_def = Define`BIGSUP f = build_lprefix_lub (over_all f)` 1559 1560val _ = Parse.add_rule{term_name="BIGSUP",fixity=Parse.Binder,pp_elements=[TOK"BIGSUP"], 1561 block_style=(NoPhrasing,(PP.CONSISTENT,0)),paren_style=OnlyIfNecessary} 1562 1563val semantics_alt = save_thm("semantics_alt", 1564 semantics_def 1565 |> SIMP_RULE bool_ss [image_intro] 1566 |> SIMP_RULE bool_ss [prefix_chain_sem_t_io_trace_over_all_c,lprefix_lubTheory.prefix_chain_FILTER,lprefix_lubTheory.prefix_chain_lprefix_chain,lprefix_lubTheory.build_prefix_lub_intro] 1567 |> SIMP_RULE bool_ss [IMAGE_over_all] 1568 |> SIMP_RULE bool_ss [prove(``f o g = ��c. f (g c)``,rw[FUN_EQ_THM])] 1569 |> SIMP_RULE bool_ss [GSYM BIGSUP_def]) 1570 1571val oracle_upd_def = Define` 1572 oracle_upd s (b,a) = 1573 s with <|non_det_o := a; io_trace:=s.io_trace ++[INR b]|>` 1574 1575val _ = save_thm ("step_e_rules_oracle_upd",step_e_rules|>REWRITE_RULE[GSYM oracle_upd_def]) 1576 1577val _ = export_theory (); 1578