1open HolKernel Parse boolLib bossLib; 2 3val _ = new_theory "for"; 4 5(* 6 7This file defines a simple FOR language that's very similar to the FOR 8language used by Arthur Chargu��raud in his ESOP'13 paper: 9 10 Pretty-Big-Step Semantics 11 http://www.chargueraud.org/research/2012/pretty/ 12 13This file defines: 14 - the syntax of the language, 15 - a functional big-step semantics (an interpreter with a clock), 16 - a very simple type checker (that is proved sound) 17 - a clocked relational big-step semantics (and equivalence proof) and 18 - a conventional (unclocked) relational big-step semantics (inductive and co-inductive) 19*) 20 21open optionTheory pairTheory pred_setTheory finite_mapTheory stringTheory; 22open integerTheory lcsymtacs; 23 24val _ = temp_tight_equality (); 25 26val ect = BasicProvers.EVERY_CASE_TAC; 27 28 29(* === Syntax === *) 30 31val _ = Datatype ` 32e = Var string 33 | Num int 34 | Add e e 35 | Assign string e`; 36 37val _ = Datatype ` 38t = 39 | Dec string t 40 | Exp e 41 | Break 42 | Seq t t 43 | If e t t 44 | For e e t`; 45 46val _ = Datatype ` 47r = Rval int 48 | Rbreak 49 | Rtimeout 50 | Rfail`; 51 52val r_distinct = fetch "-" "r_distinct"; 53val r_11 = fetch "-" "r_11"; 54 55 56(* === Functional big-step semantics === *) 57 58val _ = Datatype ` 59state = <| store : string |-> int; clock : num |>`; 60 61val state_component_equality = fetch "-" "state_component_equality"; 62 63val store_var_def = Define ` 64 store_var v x s = s with store := s.store |+ (v,x)`; 65 66val _ = augment_srw_ss[rewrites[store_var_def]]; 67 68val state_rw = Q.prove ( 69`(!s c. <| store := s; clock := c |>.store = s) ��� 70 (!s. <| store := s.store; clock := s.clock |> = s)`, 71 rw [state_component_equality]); 72 73(* Expression evaluation *) 74 75val sem_e_def = Define ` 76(sem_e s (Var x) = 77 case FLOOKUP s.store x of 78 | NONE => (Rfail, s) 79 | SOME n => (Rval n, s)) ��� 80(sem_e s (Num num) = 81 (Rval num, s)) ��� 82(sem_e s (Add e1 e2) = 83 case sem_e s e1 of 84 | (Rval n1, s1) => 85 (case sem_e s1 e2 of 86 | (Rval n2, s2) => 87 (Rval (n1 + n2), s2) 88 | r => r) 89 | r => r) ��� 90(sem_e s (Assign x e) = 91 case sem_e s e of 92 | (Rval n1, s1) => 93 (Rval n1, store_var x n1 s1) 94 | r => r)`; 95 96(* HOL4's definition requires a little help with the definition. In 97 particular, we need to help it see that the clock does not 98 decrease. To do this, we add a few redundant checks (check_clock) 99 to the definition of the sem_t function. These redundant checks are 100 removed later in the script. *) 101 102val sem_e_clock = Q.store_thm ("sem_e_clock", 103`!s e r s'. sem_e s e = (r, s') ��� s.clock = s'.clock`, 104 Induct_on `e` >> rw [sem_e_def] >> ect >> 105 fs [] >> rw [] >> metis_tac []); 106 107val sem_e_store = Q.prove ( 108`!s e r s'. sem_e s e = (r, s') ��� FDOM s.store ��� FDOM s'.store`, 109 Induct_on `e` >> rw [sem_e_def] >> ect >> 110 fs [SUBSET_DEF] >> rw [] >> metis_tac []); 111 112val sem_e_res = Q.prove ( 113`!s e r s'. sem_e s e = (r, s') ��� r ��� Rbreak ��� r ��� Rtimeout`, 114 Induct_on `e` >> rw [sem_e_def] >> ect >> 115 fs [] >> rw [] >> metis_tac []); 116 117val check_clock_def = Define ` 118check_clock s' s = 119 s' with clock := (if s'.clock ��� s.clock then s'.clock else s.clock)`; 120 121val dec_clock_def = Define ` 122dec_clock s = s with clock := s.clock - 1`; 123 124val dec_clock_store = Q.store_thm ("dec_clock_store[simp]", 125`!s. (dec_clock s).store = s.store`, 126 rw [dec_clock_def]); 127 128(* Statement evaluation -- with redundant check_clock *) 129 130val sem_t_def = tDefine "sem_t" ` 131(sem_t s (Exp e) = sem_e s e) ��� 132(sem_t s (Dec x t) = 133 sem_t (store_var x 0 s) t) ��� 134(sem_t s Break = (Rbreak, s)) ��� 135(sem_t s (Seq t1 t2) = 136 case sem_t s t1 of 137 | (Rval _, s1) => 138 sem_t (check_clock s1 s) t2 139 | r => r) ��� 140(sem_t s (If e t1 t2) = 141 case sem_e s e of 142 | (Rval n1, s1) => sem_t s1 (if n1 = 0 then t2 else t1) 143 | r => r) ��� 144(sem_t s (For e1 e2 t) = 145 case sem_e s e1 of 146 | (Rval n1, s1) => 147 if n1 = 0 then 148 (Rval 0, s1) 149 else 150 (case sem_t s1 t of 151 | (Rval _, s2) => 152 (case sem_e s2 e2 of 153 | (Rval _, s3) => 154 if s.clock ��� 0 ��� s3.clock ��� 0 then 155 sem_t (dec_clock (check_clock s3 s)) (For e1 e2 t) 156 else 157 (Rtimeout, s3) 158 | r => r) 159 | (Rbreak, s2) => 160 (Rval 0, s2) 161 | r => r) 162 | r => r)` 163 (WF_REL_TAC `(inv_image (measure I LEX measure t_size) 164 (\(s,t). (s.clock,t)))` 165 \\ REPEAT STRIP_TAC \\ TRY DECIDE_TAC 166 \\ fs [check_clock_def, dec_clock_def, LET_THM] 167 \\ rw [] 168 \\ imp_res_tac sem_e_clock 169 \\ DECIDE_TAC); 170 171val sem_t_clock = Q.store_thm ("sem_t_clock", 172`!s t r s'. sem_t s t = (r, s') ��� s'.clock ��� s.clock`, 173 ho_match_mp_tac (fetch "-" "sem_t_ind") >> 174 reverse (rpt strip_tac) >> 175 pop_assum mp_tac >> 176 rw [Once sem_t_def] >> 177 ect >> 178 imp_res_tac sem_e_clock >> 179 fs [] >> 180 fs [check_clock_def, dec_clock_def, LET_THM] >> 181 TRY decide_tac >> 182 rfs [] >> 183 res_tac >> 184 decide_tac); 185 186val check_clock_id = Q.prove ( 187`!s s'. s.clock ��� s'.clock ��� check_clock s s' = s`, 188 rw [check_clock_def, state_component_equality]); 189 190val STOP_def = Define ` 191 STOP x = x`; 192 193(* Statement evaluation -- without any redundant checks *) 194 195fun term_rewrite tms = let 196 fun f tm = ASSUME (list_mk_forall(free_vars tm,tm)) 197 in rand o concl o QCONV (REWRITE_CONV (map f tms)) end 198 199val sem_t_def_with_stop = store_thm ("sem_t_def_with_stop", 200 sem_t_def |> concl |> term_rewrite [``check_clock s3 s = s3``, 201 ``s.clock <> 0 /\ s3.clock <> 0 <=> s3.clock <> 0``, 202 ``sem_t (dec_clock s3) (For e1 e2 t) = 203 sem_t (dec_clock s3) (STOP (For e1 e2 t))``], 204 rpt strip_tac >> 205 rw [Once sem_t_def,STOP_def] >> 206 ect >> 207 fs [] >> 208 imp_res_tac sem_t_clock >> 209 fs [dec_clock_def, LET_THM, check_clock_id] >> 210 rpt (AP_TERM_TAC ORELSE AP_THM_TAC) >> 211 rw [state_component_equality] >> 212 rw [check_clock_def] >> 213 imp_res_tac sem_e_clock >> 214 fs [] >> 215 `F` by decide_tac); 216 217val sem_t_def = 218 save_thm("sem_t_def",REWRITE_RULE [STOP_def] sem_t_def_with_stop); 219 220(* We also remove the redundant checks from the induction theorem. *) 221 222val sem_t_ind = store_thm("sem_t_ind", 223 fetch "-" "sem_t_ind" 224 |> concl |> term_rewrite [``check_clock s3 s = s3``, 225 ``s.clock <> 0 /\ s3.clock <> 0 <=> s3.clock <> 0``], 226 ntac 2 strip_tac >> 227 ho_match_mp_tac (fetch "-" "sem_t_ind") >> 228 rw [] >> 229 first_x_assum match_mp_tac >> 230 rw [] >> 231 fs [] >> 232 res_tac >> 233 imp_res_tac sem_t_clock >> 234 imp_res_tac sem_e_clock >> 235 fs [dec_clock_def, check_clock_id, LET_THM] >> 236 first_x_assum match_mp_tac >> 237 decide_tac) 238 239val sem_t_store = Q.prove ( 240`!s t r s'. sem_t s t = (r, s') ��� FDOM s.store ��� FDOM s'.store`, 241 ho_match_mp_tac sem_t_ind >> 242 rpt conj_tac >> 243 rpt gen_tac >> 244 DISCH_TAC >> 245 ONCE_REWRITE_TAC [sem_t_def] 246 >- (fs [sem_t_def] >> 247 metis_tac [sem_e_store]) 248 >- (fs [sem_t_def] >> 249 metis_tac []) 250 >- (fs [sem_t_def] >> 251 metis_tac []) 252 >- (ect >> 253 rw [] >> 254 metis_tac [sem_e_store, SUBSET_DEF]) 255 >- (ect >> 256 rw [] >> 257 metis_tac [sem_e_store, SUBSET_DEF]) 258 >- (Cases_on `sem_e s e1` >> 259 fs [] >> 260 Cases_on `q` >> 261 reverse (fs []) 262 >- (Cases_on `i = 0` >> 263 fs [] 264 >- metis_tac [sem_e_store, SUBSET_TRANS] >> 265 Cases_on `sem_t r t` >> 266 fs [] >> 267 Cases_on `q` >> 268 reverse (fs []) 269 >- (ect >> 270 fs [] >> 271 rw [] >> 272 rfs [] >> 273 metis_tac [sem_e_store, SUBSET_TRANS]) >> 274 metis_tac [sem_e_store, SUBSET_TRANS]) >> 275 metis_tac [sem_e_store, SUBSET_TRANS])); 276 277(* The top-level semantics defines what is externally observable *) 278 279val _ = Datatype ` 280 observation = Terminate | Diverge | Crash`; 281 282val s_with_clock_def = Define ` 283 s_with_clock c = <| store := FEMPTY; clock := c |>`; 284 285val semantics_def = Define ` 286 semantics t = 287 if (?c v s. sem_t (s_with_clock c) t = (Rval v,s)) then 288 Terminate 289 else if (!c. ?s. sem_t (s_with_clock c) t = (Rtimeout,s)) then 290 Diverge 291 else Crash` 292 293val semantics_thm = save_thm("semantics_thm",semantics_def); 294 295 296(* === A simple type checker === *) 297 298val type_e_def = Define ` 299(type_e s (Var x) ��� x ��� s) ��� 300(type_e s (Num num) ��� T) ��� 301(type_e s (Add e1 e2) ��� type_e s e1 ��� type_e s e2) ��� 302(type_e s (Assign x e) ��� x ��� s ��� type_e s e)`; 303 304val type_t_def = Define ` 305(type_t in_for s (Exp e) ��� type_e s e) ��� 306(type_t in_for s (Dec x t) ��� type_t in_for (x INSERT s) t) ��� 307(type_t in_for s Break ��� in_for) ��� 308(type_t in_for s (Seq t1 t2) ��� type_t in_for s t1 ��� type_t in_for s t2) ��� 309(type_t in_for s (If e t1 t2) ��� type_e s e ��� type_t in_for s t1 ��� type_t in_for s t2) ��� 310(type_t in_for s (For e1 e2 t) ��� type_e s e1 ��� type_e s e2 ��� type_t T s t)`; 311 312val type_weakening_e = Q.prove ( 313`!s e s' s1. type_e s e ��� s ��� s1 ��� type_e s1 e`, 314 Induct_on `e` >> 315 rw [type_e_def, SUBSET_DEF] >> 316 ect >> 317 fs [] >> 318 rw [EXTENSION] >> 319 metis_tac [SUBSET_DEF, NOT_SOME_NONE, SOME_11]); 320 321val type_sound_e = Q.prove ( 322`!s e s1 c. 323 type_e s e ��� s ��� FDOM s1 324 ��� 325 ?r s1'. 326 r ��� Rfail ��� 327 sem_e <| store := s1; clock := c |> e = (r, s1')`, 328 Induct_on `e` >> 329 rw [type_e_def, sem_e_def] 330 >- (ect >> 331 fs [FLOOKUP_DEF, SUBSET_DEF] >> 332 rw [] >> 333 metis_tac []) 334 >- (res_tac >> 335 ntac 2 (pop_assum (qspec_then `c` mp_tac)) >> 336 rw [] >> 337 rw [] >> 338 `type_e (FDOM s1''.store) e'` 339 by (rw [] >> 340 match_mp_tac type_weakening_e >> 341 metis_tac [sem_e_store, SUBSET_TRANS, state_rw]) >> 342 first_x_assum (fn th => pop_assum (fn th' => assume_tac (MATCH_MP (SIMP_RULE (srw_ss()) [GSYM AND_IMP_INTRO] th) th'))) >> 343 pop_assum (qspecl_then [`s1''.store`, `s1''.clock`] mp_tac) >> 344 rw [] >> 345 fs [state_rw] >> 346 ect >> 347 rw []) 348 >- (ect >> 349 fs [] >> 350 res_tac >> 351 pop_assum (qspec_then `c` mp_tac) >> 352 fs [])); 353 354val type_weakening_t = Q.prove ( 355`!in_for s t s' s1. type_t in_for s t ��� s ��� s1 ��� type_t in_for s1 t`, 356 Induct_on `t` >> 357 rw [type_t_def, SUBSET_DEF] >> 358 ect >> 359 fs [] >> 360 rw [EXTENSION] >> 361 metis_tac [SUBSET_DEF, NOT_SOME_NONE, SOME_11, type_weakening_e, INSERT_SUBSET]); 362 363val r_cases_eq = prove_case_eq_thm { 364 case_def = definition "r_case_def", 365 nchotomy = theorem "r_nchotomy" 366}; 367 368val pair_cases_eq = Q.prove( 369 ���(pair_CASE p f = v) ��� ���q r. p = (q,r) ��� v = f q r���, 370 Cases_on `p` >> simp[] >> metis_tac[]); 371 372val bool_cases_eq = Q.prove( 373 ���(if p then q else r) = v ��� p /\ q = v ��� ��p ��� r = v���, 374 Cases_on `p` >> simp[]); 375 376val sem_e_succeeds = Q.store_thm( 377 "sem_e_succeeds", 378 (* would make this an automatic rewrite except it might break old proofs *) 379 ���sem_e s0 e ��� (Rbreak, s) ��� sem_e s0 e ��� (Rtimeout, s)���, 380 metis_tac[sem_e_res]); 381 382(* Have to use sem_t_ind, and not type_t_ind or t_induction. This is different 383 * from small-step-based type soundness *) 384val type_sound_t = Q.prove ( 385`!s1 t in_for s. 386 type_t in_for s t ��� s ��� FDOM s1.store 387 ��� 388 ?r s1'. 389 r ��� Rfail ��� 390 (~in_for ��� r ��� Rbreak) ��� 391 sem_t s1 t = (r, s1')`, 392 ho_match_mp_tac sem_t_ind >> 393 rw [type_t_def] >> 394 ONCE_REWRITE_TAC [sem_t_def] >> 395 rw [] 396 >- (imp_res_tac type_sound_e >> 397 pop_assum (qspec_then `s1.clock` mp_tac) >> 398 rw [state_rw] >> 399 metis_tac [sem_e_res]) 400 >- (res_tac >> 401 fs [SUBSET_DEF]) 402 >- (res_tac >> 403 rw [] >> 404 Cases_on `r'` >> 405 rw [] >> 406 fs [] >> 407 rw [] >> 408 pop_assum match_mp_tac >> 409 metis_tac [type_weakening_t, sem_t_store]) 410 >- (imp_res_tac type_sound_e >> 411 pop_assum (qspec_then `s1.clock` mp_tac) >> 412 rw [state_rw] >> 413 rw [] >> 414 Cases_on `r` >> 415 fs [] 416 >- (Cases_on `i = 0` >> 417 fs [] >> 418 first_x_assum match_mp_tac >> 419 metis_tac [type_weakening_t, sem_e_store]) 420 >- metis_tac [sem_e_res]) 421 >- (imp_res_tac type_sound_e >> 422 rpt (pop_assum (qspec_then `s1.clock` mp_tac)) >> 423 rw [state_rw] >> 424 rw [] >> 425 rename [���r_CASE r'���] >> 426 reverse (Cases_on `r'`) >> 427 fs [] >- metis_tac[sem_e_res] >> 428 rename [���if i = 0 then _ else _���] >> Cases_on `i = 0` >> 429 fs [] >> 430 dsimp[r_cases_eq, pair_cases_eq, sem_e_succeeds, bool_cases_eq] >> 431 rename [���sem_e s0 gd = (Rval gv, s1)���, ���sem_t s1 body = (Rval _, _)���] >> 432 `type_t T (FDOM s1.store) body` 433 by (match_mp_tac type_weakening_t >> 434 metis_tac [sem_e_store, sem_t_store, SUBSET_TRANS, state_rw]) >> 435 first_x_assum (first_assum o mp_then.mp_then (mp_then.Pos hd) mp_tac) >> 436 simp[] >> strip_tac >> rename [���sem_t s1 body = (body_r, s2)���] >> 437 Cases_on ���body_r��� >> fs[] >> 438 rename [���sem_t s1 body = (Rval bi, s2)���, ���For gd post body���] >> 439 `type_e (FDOM s2.store) post` 440 by (match_mp_tac type_weakening_e >> 441 metis_tac [sem_e_store, sem_t_store, SUBSET_TRANS, state_rw]) >> 442 qspecl_then [���FDOM s2.store���, ���post���, ���s2.store���, ���s2.clock���] 443 mp_tac type_sound_e >> simp[state_rw] >> strip_tac >> 444 rename [���For gd post body���, ���sem_e s2 post = (pr, s3)���] >> 445 Cases_on ���pr��� >> fs[sem_e_succeeds] >> Cases_on ���s3.clock = 0��� >> simp[] >> 446 fs[] >> first_x_assum irule >> qexists_tac ���s��� >> simp[] >> 447 imp_res_tac sem_e_store >> imp_res_tac sem_t_store >> 448 metis_tac[SUBSET_TRANS])); 449 450(* A type checked program does not Crash. *) 451 452val type_soundness = Q.store_thm("type_soundness", 453`!t. type_t F {} t ��� semantics t ��� Crash`, 454 rw [semantics_def] >> 455 REPEAT STRIP_TAC >> 456 imp_res_tac type_sound_t >> 457 fs [] 458 \\ POP_ASSUM (MP_TAC o Q.SPEC `s_with_clock c`) 459 \\ REPEAT STRIP_TAC 460 \\ fs [] 461 \\ Cases_on `r` \\ fs[] 462 \\ METIS_TAC []); 463 464(* === A relational (optionally clocked) big-step semantics === *) 465 466val is_rval_def = Define ` 467(is_rval (Rval _) = T) ��� 468(is_rval _ = F)`; 469 470val (sem_e_reln_rules, sem_e_reln_ind, sem_e_reln_cases) = Hol_reln ` 471(!s x n. 472 FLOOKUP s.store x = SOME n 473 ��� 474 sem_e_reln s (Var x) (Rval n, s)) ��� 475(!s x. 476 FLOOKUP s.store x = NONE 477 ��� 478 sem_e_reln s (Var x) (Rfail, s)) ��� 479(!s n. 480 sem_e_reln s (Num n) (Rval n, s)) ��� 481(���s s1 s2 e1 e2 n1 n2. 482 sem_e_reln s e1 (Rval n1, s1) ��� 483 sem_e_reln s1 e2 (Rval n2, s2) 484 ��� 485 sem_e_reln s (Add e1 e2) (Rval (n1 + n2), s2)) ��� 486(���s s1 e1 e2 r. 487 ~is_rval r ��� 488 sem_e_reln s e1 (r, s1) 489 ��� 490 sem_e_reln s (Add e1 e2) (r, s1)) ��� 491(���s s1 s2 e1 e2 n1 r. 492 sem_e_reln s e1 (Rval n1, s1) ��� 493 ~is_rval r ��� 494 sem_e_reln s1 e2 (r, s2) 495 ��� 496 sem_e_reln s (Add e1 e2) (r, s2)) ��� 497(!s s1 x e n1. 498 sem_e_reln s e (Rval n1, s1) 499 ��� 500 sem_e_reln s (Assign x e) (Rval n1, s1 with store := s1.store |+ (x,n1))) ��� 501(!s s1 x e r. 502 ~is_rval r ��� 503 sem_e_reln s e (r, s1) 504 ��� 505 sem_e_reln s (Assign x e) (r, s1))`; 506 507(* The first argument indicates whether this is a clocked semantics or not *) 508val (sem_t_reln_rules, sem_t_reln_ind, sem_t_reln_cases) = Hol_reln ` 509(!s e r. 510 sem_e_reln s e r 511 ��� 512 sem_t_reln c s (Exp e) r) ��� 513(!s x t r. 514 sem_t_reln c (s with store := s.store |+ (x,0)) t r 515 ��� 516 sem_t_reln c s (Dec x t) r) ��� 517(!s. 518 sem_t_reln c s Break (Rbreak, s)) ��� 519(!s s1 t1 t2 n1 r. 520 sem_t_reln c s t1 (Rval n1, s1) ��� 521 sem_t_reln c s1 t2 r 522 ��� 523 sem_t_reln c s (Seq t1 t2) r) ��� 524(!s s1 t1 t2 r. 525 sem_t_reln c s t1 (r, s1) ��� 526 ~is_rval r 527 ��� 528 sem_t_reln c s (Seq t1 t2) (r, s1)) ��� 529(!s s1 e t1 t2 r. 530 sem_e_reln s e (Rval 0, s1) ��� 531 sem_t_reln c s1 t2 r 532 ��� 533 sem_t_reln c s (If e t1 t2) r) ��� 534(!s s1 e t1 t2 n r. 535 sem_e_reln s e (Rval n, s1) ��� 536 n ��� 0 ��� 537 sem_t_reln c s1 t1 r 538 ��� 539 sem_t_reln c s (If e t1 t2) r) ��� 540(!s s1 e t1 t2 r. 541 sem_e_reln s e (r, s1) ��� 542 ~is_rval r 543 ��� 544 sem_t_reln c s (If e t1 t2) (r, s1)) ��� 545(!s s1 e1 e2 t. 546 sem_e_reln s e1 (Rval 0, s1) 547 ��� 548 sem_t_reln c s (For e1 e2 t) (Rval 0, s1)) ��� 549(!s s1 s2 s3 e1 e2 t n1 n2 n3 r. 550 sem_e_reln s e1 (Rval n1, s1) ��� 551 n1 ��� 0 ��� 552 sem_t_reln c s1 t (Rval n2, s2) ��� 553 sem_e_reln s2 e2 (Rval n3, s3) ��� 554 sem_t_reln c (dec_clock s3) (For e1 e2 t) r ��� 555 (c ��� s3.clock ��� 0) 556 ��� 557 sem_t_reln c s (For e1 e2 t) r) ��� 558(!s s1 s2 e1 e2 t n1. 559 sem_e_reln s e1 (Rval n1, s1) ��� 560 n1 ��� 0 ��� 561 sem_t_reln c s1 t (Rbreak, s2) 562 ��� 563 sem_t_reln c s (For e1 e2 t) (Rval 0, s2)) ��� 564(!s s1 s2 s3 e1 e2 t n1 n2 n3. 565 sem_e_reln s e1 (Rval n1, s1) ��� 566 n1 ��� 0 ��� 567 sem_t_reln c s1 t (Rval n2, s2) ��� 568 sem_e_reln s2 e2 (Rval n3, s3) ��� 569 s3.clock = 0 ��� 570 c 571 ��� 572 sem_t_reln c s (For e1 e2 t) (Rtimeout, s3)) ��� 573(!s s1 s2 s3 e1 e2 t n1 n2 r. 574 sem_e_reln s e1 (Rval n1, s1) ��� 575 n1 ��� 0 ��� 576 sem_t_reln c s1 t (Rval n2, s2) ��� 577 sem_e_reln s2 e2 (r, s3) ��� 578 ~is_rval r 579 ��� 580 sem_t_reln c s (For e1 e2 t) (r, s3)) ��� 581(!s s1 s2 e1 e2 t n1 r. 582 sem_e_reln s e1 (Rval n1, s1) ��� 583 n1 ��� 0 ��� 584 sem_t_reln c s1 t (r, s2) ��� 585 ~is_rval r ��� 586 r ��� Rbreak 587 ��� 588 sem_t_reln c s (For e1 e2 t) (r, s2)) ��� 589(!s s1 e1 e2 t r. 590 sem_e_reln s e1 (r, s1) ��� 591 ~is_rval r 592 ��� 593 sem_t_reln c s (For e1 e2 t) (r, s1))`; 594 595(* Some proofs relating the clocked relational and functional semantics *) 596 597val big_sem_correct_lem1 = Q.prove ( 598`���s e r. 599 sem_e_reln s e r 600 ��� 601 sem_e s e = r`, 602 ho_match_mp_tac sem_e_reln_ind >> 603 rw [sem_e_def] >> 604 ect >> 605 fs [is_rval_def] >> 606 imp_res_tac sem_e_res >> 607 fs []); 608 609val big_sem_correct_lem2 = Q.prove ( 610`���s e r. 611 sem_e s e = r 612 ��� 613 sem_e_reln s e r`, 614 Induct_on `e` >> 615 rw [sem_e_def] >> 616 rw [Once sem_e_reln_cases] >> 617 ect >> 618 fs [is_rval_def] >> 619 imp_res_tac sem_e_res >> 620 fs [] >> 621 metis_tac []); 622 623val big_sem_correct_lem3 = Q.prove ( 624`���s e r. 625 sem_e_reln s e r 626 ��� 627 sem_e s e = r`, 628 metis_tac [big_sem_correct_lem1, big_sem_correct_lem2]); 629 630val big_sem_correct_lem4 = Q.prove ( 631`���s t r. 632 sem_t_reln T s t r 633 ��� 634 sem_t s t = r`, 635 ho_match_mp_tac sem_t_ind >> 636 rpt conj_tac 637 >- (rw [sem_t_def, Once sem_t_reln_cases] >> 638 metis_tac [big_sem_correct_lem1, big_sem_correct_lem2]) 639 >- (rw [sem_t_def] >> 640 rw [Once sem_t_reln_cases]) 641 >- (rw [sem_t_def] >> 642 rw [Once sem_t_reln_cases] >> 643 metis_tac []) 644 >- (rw [sem_t_def] >> 645 rw [Once sem_t_reln_cases] >> 646 ect >> 647 fs [] >> 648 metis_tac [is_rval_def, big_sem_correct_lem1, PAIR_EQ, r_distinct, r_11]) 649 >- (rw [sem_t_def] >> 650 rw [Once sem_t_reln_cases] >> 651 ect >> 652 fs [] >> 653 eq_tac >> 654 rw [] >> 655 imp_res_tac big_sem_correct_lem1 >> 656 fs [] >> 657 rw [] >> 658 rfs [] 659 >- metis_tac [is_rval_def, big_sem_correct_lem1, big_sem_correct_lem2, PAIR_EQ, r_distinct, r_11, pair_CASES] 660 >- (disj1_tac >> 661 imp_res_tac big_sem_correct_lem2 >> 662 qexists_tac `r'` >> 663 rw []) 664 >- metis_tac [is_rval_def, big_sem_correct_lem1, big_sem_correct_lem2, PAIR_EQ, r_distinct, r_11, pair_CASES] 665 >- (disj2_tac >> 666 disj1_tac >> 667 imp_res_tac big_sem_correct_lem2 >> 668 qexists_tac `r'` >> 669 qexists_tac `i` >> 670 rw []) >> 671 metis_tac [is_rval_def, big_sem_correct_lem1, big_sem_correct_lem2, PAIR_EQ, r_distinct, r_11, pair_CASES]) 672 >- (rw [] >> 673 rw [Once sem_t_reln_cases, Once sem_t_def] >> 674 Cases_on `sem_e s e1` >> 675 rw [] >> 676 Cases_on `q` >> 677 rw [] >> 678 PairCases_on `r` >> 679 fs [big_sem_correct_lem3] >> 680 rw [] 681 >- metis_tac [is_rval_def, big_sem_correct_lem1, big_sem_correct_lem2, PAIR_EQ, r_distinct, r_11, pair_CASES, PAIR_EQ] 682 >- (ect >> 683 rw [] >> 684 rfs [] >> 685 metis_tac [dec_clock_def, is_rval_def, big_sem_correct_lem1, big_sem_correct_lem2, PAIR_EQ, r_distinct, r_11, pair_CASES]) >> 686 metis_tac [is_rval_def, big_sem_correct_lem1, big_sem_correct_lem2, PAIR_EQ, r_distinct, r_11, pair_CASES, PAIR_EQ])); 687 688val sem_e_ignores_clock = Q.prove ( 689`!s t r. 690 sem_e_reln s t r 691 ��� 692 !c. sem_e_reln (s with clock := c) t (FST r, SND r with clock := c)`, 693 ho_match_mp_tac sem_e_reln_ind >> 694 rw [] >> 695 ONCE_REWRITE_TAC [sem_e_reln_cases] >> 696 rw [is_rval_def] 697 >- metis_tac [] 698 >- metis_tac [] >> 699 qexists_tac `s1 with clock := c` >> 700 rw []); 701 702val big_sem_correct_lem5 = Q.prove ( 703`���s e r. 704 sem_e_reln (s with clock := (SND r).clock) e r 705 ��� 706 (?c. FST r ��� Rtimeout ��� sem_e (s with clock := c) e = r)`, 707 rw [] >> 708 PairCases_on `r` >> 709 fs [] >> 710 eq_tac >> 711 rw [] >> 712 imp_res_tac sem_e_clock >> 713 fs [] >> 714 metis_tac [big_sem_correct_lem1, big_sem_correct_lem2, sem_e_ignores_clock, FST, SND, sem_e_res]); 715 716(* === A relational big-step semantics defined in terms of an inductive and co-inductive relation === *) 717 718(* Inductive relation, equivalent to the unclocked version above*) 719val (simple_sem_t_reln_rules, simple_sem_t_reln_ind, simple_sem_t_reln_cases) = 720 Hol_reln ` 721(!s e r. 722 sem_e_reln s e r 723 ��� 724 simple_sem_t_reln s (Exp e) r) ��� 725(!s x t r. 726 simple_sem_t_reln (s with store := s.store |+ (x,0)) t r 727 ��� 728 simple_sem_t_reln s (Dec x t) r) ��� 729(!s. 730 simple_sem_t_reln s Break (Rbreak, s)) ��� 731(!s s1 t1 t2 n1 r. 732 simple_sem_t_reln s t1 (Rval n1, s1) ��� 733 simple_sem_t_reln s1 t2 r 734 ��� 735 simple_sem_t_reln s (Seq t1 t2) r) ��� 736(!s s1 t1 t2 r. 737 simple_sem_t_reln s t1 (r, s1) ��� 738 ~is_rval r 739 ��� 740 simple_sem_t_reln s (Seq t1 t2) (r, s1)) ��� 741(!s s1 e t1 t2 r. 742 sem_e_reln s e (Rval 0, s1) ��� 743 simple_sem_t_reln s1 t2 r 744 ��� 745 simple_sem_t_reln s (If e t1 t2) r) ��� 746(!s s1 e t1 t2 n r. 747 sem_e_reln s e (Rval n, s1) ��� 748 n ��� 0 ��� 749 simple_sem_t_reln s1 t1 r 750 ��� 751 simple_sem_t_reln s (If e t1 t2) r) ��� 752(!s s1 e t1 t2 r. 753 sem_e_reln s e (r, s1) ��� 754 ~is_rval r 755 ��� 756 simple_sem_t_reln s (If e t1 t2) (r, s1)) ��� 757(!s s1 e1 e2 t. 758 sem_e_reln s e1 (Rval 0, s1) 759 ��� 760 simple_sem_t_reln s (For e1 e2 t) (Rval 0, s1)) ��� 761(!s s1 e1 e2 t r. 762 sem_e_reln s e1 (r, s1) ��� 763 ~is_rval r 764 ��� 765 simple_sem_t_reln s (For e1 e2 t) (r, s1)) ��� 766(!s s1 s2 s3 e1 e2 t n1 n2 n3 r. 767 sem_e_reln s e1 (Rval n1, s1) ��� 768 n1 ��� 0 ��� 769 simple_sem_t_reln s1 t (Rval n2, s2) ��� 770 sem_e_reln s2 e2 (Rval n3, s3) ��� 771 simple_sem_t_reln s3 (For e1 e2 t) r 772 ��� 773 simple_sem_t_reln s (For e1 e2 t) r) ��� 774(!s s1 s2 e1 e2 t n1. 775 sem_e_reln s e1 (Rval n1, s1) ��� 776 n1 ��� 0 ��� 777 simple_sem_t_reln s1 t (Rbreak, s2) 778 ��� 779 simple_sem_t_reln s (For e1 e2 t) (Rval 0, s2)) ��� 780(!s s1 s2 s3 e1 e2 t n1 n2 r. 781 sem_e_reln s e1 (Rval n1, s1) ��� 782 n1 ��� 0 ��� 783 simple_sem_t_reln s1 t (Rval n2, s2) ��� 784 sem_e_reln s2 e2 (r, s3) ��� 785 ~is_rval r 786 ��� 787 simple_sem_t_reln s (For e1 e2 t) (r, s3)) ��� 788(!s s1 s2 e1 e2 t n1 r. 789 sem_e_reln s e1 (Rval n1, s1) ��� 790 n1 ��� 0 ��� 791 simple_sem_t_reln s1 t (r, s2) ��� 792 ~is_rval r ��� 793 r ��� Rbreak 794 ��� 795 simple_sem_t_reln s (For e1 e2 t) (r, s2))`; 796 797(* Co-Inductive relation, which defines diverging computations *) 798val (simple_sem_t_div_rules,simple_sem_t_div_coind,simple_sem_t_div_cases) = Hol_coreln` 799(���s t x. 800 simple_sem_t_div (s with store:= s.store |+ (x,0)) t ��� 801 simple_sem_t_div s (Dec x t)) ��� 802(���s t1 t2. 803 simple_sem_t_div s t1 ��� 804 simple_sem_t_div s (Seq t1 t2)) ��� 805(���s t1 t2 n1 s1. 806 simple_sem_t_reln s t1 (Rval n1,s1) ��� 807 simple_sem_t_div s1 t2 ��� 808 simple_sem_t_div s (Seq t1 t2)) ��� 809(���s e t1 t2 s1. 810 sem_e_reln s e (Rval 0, s1) ��� 811 simple_sem_t_div s1 t2 812 ��� 813 simple_sem_t_div s (If e t1 t2)) ��� 814(���s e t1 t2 n s1. 815 sem_e_reln s e (Rval n, s1) ��� 816 n ��� 0 ��� 817 simple_sem_t_div s1 t1 818 ��� 819 simple_sem_t_div s (If e t1 t2)) ��� 820(���s e1 e2 t n1 s1. 821 sem_e_reln s e1 (Rval n1, s1) ��� 822 n1 ��� 0 ��� 823 simple_sem_t_div s1 t ��� 824 simple_sem_t_div s (For e1 e2 t)) ��� 825(���s e1 e2 t n1 s1 n2 s2 n3 s3. 826 sem_e_reln s e1 (Rval n1, s1) ��� 827 n1 ��� 0 ��� 828 simple_sem_t_reln s1 t (Rval n2, s2) ��� 829 sem_e_reln s2 e2 (Rval n3, s3) ��� 830 simple_sem_t_div s3 (For e1 e2 t) 831 ��� 832 simple_sem_t_div s (For e1 e2 t))` 833 834val init_store_def = Define` 835 init_store = <|store:=FEMPTY;clock:=0|>` 836 837(* Top observable semantics for the unclocked relational semantics *) 838val rel_semantics_def = Define ` 839 rel_semantics t = 840 if (?v s. simple_sem_t_reln init_store t (Rval v,s)) then 841 Terminate 842 else if simple_sem_t_div init_store t then 843 Diverge 844 else Crash` 845 846(* Proofs relating clocked functional big step to unclocked relational semantics *) 847val simple_sem_t_reln_strongind = fetch "-" "simple_sem_t_reln_strongind" 848 849val semttac = simp[Once simple_sem_t_reln_cases,is_rval_def] 850val semetac = simp[Once sem_e_reln_cases] 851 852(* Determinism of simple_sem_t_reln *) 853val sem_e_reln_determ = Q.store_thm("sem_e_reln_determ", 854`���s e res. 855 sem_e_reln s e res ��� 856 ���res'. sem_e_reln s e res' ��� res=res'`, 857 rw[]>> 858 fs[big_sem_correct_lem3]) 859 860val simple_sem_t_reln_determ = Q.prove( 861`���s t res. 862 simple_sem_t_reln s t res ��� 863 ���res'. simple_sem_t_reln s t res' ��� res = res'`, 864 ho_match_mp_tac simple_sem_t_reln_strongind>> 865 rw[]>>pop_assum mp_tac >> semttac>>fs[FORALL_PROD]>> 866 TRY(Cases_on`res`)>> 867 TRY(Cases_on`res'`) 868 >- metis_tac[sem_e_reln_determ] 869 >>rw[]>>fs[]>>res_tac>>fs[]>> 870 imp_res_tac sem_e_reln_determ>>fs[]>> 871 res_tac>>fs[]>>imp_res_tac sem_e_reln_determ>>fs[]>> 872 metis_tac[is_rval_def]) 873 874val _ = save_thm("simple_sem_t_reln_determ", simple_sem_t_reln_determ) 875 876(* Disjointness of simple_sem_t_reln and simple_sem_t_div*) 877val simple_sem_t_reln_not_div = Q.prove( 878`���s t res. 879 (simple_sem_t_reln s t res ��� 880 �� simple_sem_t_div s t)`, 881 ho_match_mp_tac simple_sem_t_reln_strongind>>rw[]>> 882 TRY(Cases_on`res`)>> 883 simp[Once simple_sem_t_div_cases]>> 884 fs[METIS_PROVE [] `` A ��� B ��� ��A ��� B``] 885 >> rpt 886 (rw[]>> 887 imp_res_tac sem_e_reln_determ>>fs[]>> 888 imp_res_tac simple_sem_t_reln_determ>>fs[is_rval_def])) 889 890val _ = save_thm("simple_sem_t_reln_not_div", simple_sem_t_reln_not_div) 891 892val simple_sem_t_reln_ignores_clock = Q.prove( 893`���s t res. 894 simple_sem_t_reln s t res ��� 895 ���c. simple_sem_t_reln (s with clock:=c) t (FST res,SND res with clock:=c)`, 896 ho_match_mp_tac simple_sem_t_reln_strongind>> 897 rw[]>>fs[EXISTS_PROD]>>semttac>> 898 imp_res_tac sem_e_ignores_clock>>fs[]>> 899 metis_tac[]) 900 901val clock_rm = Q.prove( 902`���s. s with clock:=s.clock = s`, fs[state_component_equality]) 903 904(* sem_t_reln wth clock imples simple_sem_t_reln *) 905val sem_t_reln_imp_simple_sem_t_reln = Q.prove( 906`���s t r. 907 sem_t_reln T s t r ��� 908 FST r ��� Rtimeout ��� 909 simple_sem_t_reln s t (FST r,SND r with clock := s.clock)`, 910 ho_match_mp_tac sem_t_reln_ind>>rw[]>> 911 semttac>>fs[]>> 912 imp_res_tac sem_e_ignores_clock>> 913 imp_res_tac simple_sem_t_reln_ignores_clock>> 914 fs[dec_clock_def,is_rval_def]>> 915 TRY(metis_tac[clock_rm,is_rval_def])) 916 917(* Functional big step not time out implies simple_sem_t_reln *) 918val sem_t_imp_simple_sem_t_reln = save_thm ("sem_t_imp_simple_sem_t_reln",sem_t_reln_imp_simple_sem_t_reln |> REWRITE_RULE[big_sem_correct_lem4,AND_IMP_INTRO]|>SIMP_RULE std_ss[FORALL_PROD]) 919 920(* simple_sem_t_reln implies there exists a clock for sem_t that does not timeout *) 921 922val inst_1 = qpat_x_assum`���c'.���c. A= (FST r,B)` (qspec_then`c'` assume_tac) 923fun inst_2 q = qpat_x_assum`���c'.���c. A= B` (qspec_then q assume_tac) 924 925val simple_sem_t_reln_imp_sem_t = Q.prove( 926`���s t r. 927 simple_sem_t_reln s t r ��� 928 ���c'. ���c. sem_t (s with clock:=c) t = (FST r,(SND r) with clock:=c')`, 929 ho_match_mp_tac simple_sem_t_reln_strongind>>rw[]>> 930 fs[sem_t_def_with_stop,GSYM big_sem_correct_lem3]>> 931 imp_res_tac sem_e_ignores_clock>> 932 fs[big_sem_correct_lem3]>> 933 TRY(metis_tac[clock_rm]) 934 >- 935 (inst_1>>fs[]>>inst_2`c`>>fs[]>> 936 qexists_tac`c''`>>fs[]) 937 >- 938 (first_x_assum(qspec_then`c'`assume_tac)>>fs[]>> 939 qexists_tac`c`>>fs[]>> 940 ect>>fs[is_rval_def]) 941 >- 942 (ect>>fs[is_rval_def]>> 943 metis_tac[clock_rm]) 944 >- 945 (ect>>fs[is_rval_def]>> 946 metis_tac[clock_rm]) 947 >- 948 (inst_1>>fs[]>>inst_2`c+1`>>fs[]>> 949 qexists_tac`c''`>>fs[dec_clock_def]>> 950 first_x_assum(qspec_then`c`assume_tac)>>fs[]>> 951 simp[Once STOP_def,Once sem_t_def_with_stop]>> 952 fs[dec_clock_def]) 953 >> 954 (inst_2`c'`>>fs[]>>qexists_tac`c`>>fs[]>>ect>>fs[is_rval_def])) 955 956(*val _ = save_thm("simple_sem_t_reln_imp_sem_t", 957simple_sem_t_reln_imp_sem_t |> SIMP_RULE std_ss [FORALL_PROD])*) 958 959val sem_e_reln_not_timeout = prove(`` 960 ���s e r. 961 sem_e_reln s e r ��� FST r ��� Rtimeout``, 962 ho_match_mp_tac sem_e_reln_ind >>rw[]) 963 964val simple_sem_t_reln_not_timeout = prove(`` 965 ���s t r. simple_sem_t_reln s t r ��� FST r ��� Rtimeout``, 966 ho_match_mp_tac simple_sem_t_reln_ind>>rw[]>> 967 TRY(metis_tac[sem_e_reln_not_timeout,FST])) 968 969val simple_sem_t_reln_iff_sem_t = store_thm("simple_sem_t_reln_iff_sem_t",`` 970 ���s t r s'. 971 simple_sem_t_reln s t (r,s' with clock:=s.clock) ��� 972 ���c'. sem_t (s with clock:=c') t = (r,s') ��� r ��� Rtimeout``, 973 rw[]>>EQ_TAC>>strip_tac>>fs[] 974 >- 975 (imp_res_tac simple_sem_t_reln_imp_sem_t>>fs[]>> 976 first_assum(qspec_then`s'.clock` assume_tac)>>fs[clock_rm]>> 977 metis_tac[simple_sem_t_reln_not_timeout,FST]) 978 >> 979 imp_res_tac sem_t_imp_simple_sem_t_reln>> 980 fs[]>> 981 imp_res_tac simple_sem_t_reln_ignores_clock>> 982 first_assum(qspec_then`s.clock` assume_tac)>>fs[clock_rm]) 983 984(* Next, we prove that simple_sem_t_div covers all diverging cases of sem_t *) 985 986val sem_e_reln_same_clock = Q.prove( 987 `sem_e_reln s e (v,r) ��� r.clock = s.clock`, 988 rw[]>>imp_res_tac sem_e_ignores_clock>> 989 pop_assum(qspec_then`s.clock` assume_tac)>>fs[clock_rm]>> 990 imp_res_tac sem_e_reln_determ>>fs[state_component_equality]) 991 992val sem_e_clock_inc = Q.prove( 993 `���s e r. 994 sem_e s e = r ��� 995 ���k. sem_e (s with clock:= s.clock+k) e =(FST r,(SND r)with clock:= (SND r).clock+k)`, 996 rw[]>>Cases_on`sem_e s e`>>Cases_on`q`>> 997 TRY (metis_tac[sem_e_res] )>> 998 fs[GSYM big_sem_correct_lem3]>> 999 imp_res_tac sem_e_ignores_clock>> 1000 imp_res_tac sem_e_reln_same_clock>> 1001 fs[]) 1002 1003val LTE_SUM = 1004 arithmeticTheory.LESS_EQ_EXISTS 1005 |> Q.SPECL[`A`,`B`] 1006 |> CONV_RULE(RAND_CONV(RAND_CONV(ALPHA_CONV``C:num``))) 1007 |> Q.GENL[`A`,`B`] 1008 1009val LT_SUM = Q.prove( 1010 `���A:num B. A < B ��� ���C. B = A+C ��� C > 0`, 1011 Induct>>fs[]>>rw[]>> 1012 Cases_on`B`>>fs[]>>res_tac>> 1013 qexists_tac`C`>>fs[]>> 1014 DECIDE_TAC) 1015 1016(* Everything above current clock gives same result if didn't time out*) 1017local val rw = srw_tac[] val fs = fsrw_tac[] in 1018val sem_t_clock_inc = Q.prove( 1019`���s t r. 1020 sem_t s t = r ��� FST r ��� Rtimeout ��� 1021 ���k. sem_t (s with clock:= s.clock+k) t =(FST r,(SND r)with clock:= (SND r).clock+k)`, 1022 ho_match_mp_tac sem_t_ind>>rw[]>>fs[sem_e_clock]>> 1023 TRY(fs[sem_t_def_with_stop]>>NO_TAC) 1024 >- 1025 (fs[sem_t_def_with_stop]>>Cases_on`sem_e s e`>>Cases_on`q`>> 1026 metis_tac[sem_e_res,sem_e_clock_inc,FST,SND]) 1027 >- 1028 (fs[sem_t_def_with_stop]>>Cases_on`sem_t s t`>>Cases_on`q`>>fs[]) 1029 >- 1030 (fs[sem_t_def_with_stop]>>Cases_on`sem_e s e`>>Cases_on`q`>>fs[sem_e_res]>> 1031 imp_res_tac sem_e_clock_inc>> 1032 pop_assum(qspec_then`k` assume_tac)>>fs[]) 1033 >> 1034 pop_assum mp_tac>> simp[sem_t_def_with_stop]>> 1035 Cases_on`sem_e s e1`>>Cases_on`q`>>fs[]>> 1036 imp_res_tac sem_e_clock_inc>>fs[]>> 1037 TRY(pop_assum(qspec_then`k` assume_tac))>> 1038 fs[DECIDE ``(A:num)+B = B+A``]>> 1039 IF_CASES_TAC>>fs[]>> 1040 Cases_on`sem_t r t`>>Cases_on`q`>>fs[]>> 1041 Cases_on`sem_e r' e2`>>Cases_on`q`>>fs[]>> 1042 imp_res_tac sem_e_clock_inc>>fs[]>> 1043 TRY(pop_assum(qspec_then`k` assume_tac))>> 1044 fs[DECIDE ``(A:num)+B = B+A``]>> 1045 IF_CASES_TAC>>fs[]>>rw[]>> 1046 fs[dec_clock_def,STOP_def]>> 1047 `1 ��� r''.clock` by DECIDE_TAC>> 1048 metis_tac[arithmeticTheory.LESS_EQ_ADD_SUB]) 1049end 1050 1051val _ = save_thm ("sem_t_clock_inc", sem_t_clock_inc |> SIMP_RULE std_ss [FORALL_PROD]); 1052 1053(* If current clock times out, everything below it timesout *) 1054val sem_t_clock_dec = Q.prove( 1055`���s t r. 1056 sem_t s t = r ��� FST r = Rtimeout ��� 1057 ���c. c ��� s.clock ��� 1058 FST(sem_t (s with clock:= c) t) = Rtimeout`, 1059 rw[]>>CCONTR_TAC>> 1060 Cases_on`sem_t (s with clock:=c) t`>>Cases_on`q`>>fs[]>> 1061 imp_res_tac sem_t_clock_inc>>fs[]>> 1062 imp_res_tac LTE_SUM>> 1063 rename [���s.clock = c0 + cdelta���] >> 1064 first_x_assum(qspec_then`cdelta` assume_tac)>>rfs[]>> 1065 qpat_x_assum`s.clock=A` (SUBST_ALL_TAC o SYM)>>fs[clock_rm]); 1066 1067(* Functional big step divergence *) 1068val sem_t_div_def = Define` 1069 sem_t_div s t ��� 1070 (���c. FST (sem_t (s with clock:=c) t) = Rtimeout)`; 1071 1072val clock_rm_simp_tac = 1073 fs[GSYM big_sem_correct_lem3]>> 1074 imp_res_tac sem_e_ignores_clock>> 1075 fs[big_sem_correct_lem3] 1076 1077(* Proof is split into two directions *) 1078val simple_sem_t_div_sem_t_div = Q.prove( 1079`���s t. 1080 simple_sem_t_div s t ��� 1081 sem_t_div s t`, 1082 rw[]>> 1083 assume_tac simple_sem_t_reln_not_div>> 1084 fs[METIS_PROVE [] ``A ��� ��B ��� B ��� ��A``]>> 1085 res_tac>>fs[sem_t_div_def]>> 1086 CCONTR_TAC>>fs[]>> 1087 Cases_on`sem_t (s with clock:=c) t`>>Cases_on`q`>>fs[]>> 1088 imp_res_tac sem_t_imp_simple_sem_t_reln>>fs[]>> 1089 imp_res_tac simple_sem_t_reln_ignores_clock>> 1090 pop_assum(qspec_then`s.clock` assume_tac)>>fs[clock_rm]>> 1091 metis_tac[]); 1092 1093val sem_t_div_simple_sem_t_div = Q.prove( 1094 `���s t. 1095 sem_t_div s t ��� 1096 simple_sem_t_div s t`, 1097 ho_match_mp_tac simple_sem_t_div_coind>> 1098 fs[sem_t_div_def]>> 1099 Cases_on`t`>> 1100 fs[Once sem_t_def_with_stop] 1101 >- 1102 (rw[]>> 1103 metis_tac[sem_e_res,FST,PAIR]) 1104 >- 1105 (fs[METIS_PROVE [] `` A ��� B ��� ��A ��� B``]>>rw[]>> 1106 Cases_on`sem_t (s with clock:=c) t'`>>Cases_on`q`>>fs[]>> 1107 TRY(first_x_assum(qspec_then`c`assume_tac)>>rfs[]>>NO_TAC)>> 1108 imp_res_tac sem_t_imp_simple_sem_t_reln>>fs[]>> 1109 imp_res_tac simple_sem_t_reln_ignores_clock>> 1110 pop_assum(qspec_then`s.clock`assume_tac)>>fs[clock_rm]>> 1111 qexists_tac`i`>> 1112 qexists_tac`r with clock:=s.clock`>>fs[is_rval_def]>> 1113 rw[]>>Cases_on`c' ��� r.clock` 1114 >- 1115 (first_x_assum(qspec_then`c`mp_tac)>>fs[]>>rw[]>> 1116 imp_res_tac sem_t_clock_dec>> 1117 metis_tac[]) 1118 >> 1119 `r.clock ��� c'` by DECIDE_TAC>> 1120 imp_res_tac LTE_SUM>> 1121 imp_res_tac sem_t_clock_inc>>fs[]>> 1122 rename [�����(cdelta + r.clock ��� r.clock)���] >> 1123 pop_assum(qspec_then`cdelta` assume_tac)>>fs[]>> 1124 first_x_assum(qspec_then`c+cdelta`mp_tac)>>fs[]>>rw[]) 1125 >- 1126 (fs[METIS_PROVE [] `` A ��� B ��� ��A ��� B``]>>rw[]>> 1127 Cases_on`sem_e s e`>>Cases_on`q`>>fs[]>> 1128 clock_rm_simp_tac>>TRY(metis_tac[sem_e_res])) 1129 >> 1130 fs[METIS_PROVE [] `` A ��� B ��� ��A ��� B``]>>rw[]>> 1131 fs[big_sem_correct_lem3]>> 1132 Cases_on`sem_e s e0`>>Cases_on`q`>>fs[]>> 1133 clock_rm_simp_tac>>TRY(metis_tac[sem_e_res])>> 1134 Cases_on`i = 0`>>fs[]>> 1135 Cases_on`sem_t (r with clock:=c) t'`>>Cases_on`q`>>fs[]>> 1136 TRY(last_x_assum(qspec_then`c`assume_tac)>>rfs[]>>NO_TAC)>> 1137 imp_res_tac sem_t_imp_simple_sem_t_reln>>fs[]>> 1138 imp_res_tac simple_sem_t_reln_ignores_clock>> 1139 pop_assum(qspec_then`r.clock`assume_tac)>>fs[clock_rm]>> 1140 Cases_on`sem_e (r' with clock:=r.clock) e`>>Cases_on`q`>>fs[]>> 1141 clock_rm_simp_tac>>TRY(metis_tac[sem_e_res])>> 1142 TRY(last_x_assum(qspec_then`c`assume_tac)>>rfs[]>> 1143 last_x_assum(qspec_then`r'.clock` assume_tac)>>fs[clock_rm]>>NO_TAC)>> 1144 qexists_tac`i'`>> 1145 qexists_tac`r' with clock:=r.clock`>>fs[]>>rw[]>> 1146 Cases_on`c' ��� r'.clock` 1147 >- 1148 (last_x_assum(qspec_then`c+1`mp_tac)>> 1149 imp_res_tac sem_t_clock_inc>>fs[]>> 1150 rw[]>> 1151 imp_res_tac sem_t_clock_dec>> 1152 fs[dec_clock_def,Once STOP_def]>> 1153 pop_assum mp_tac>> 1154 qpat_abbrev_tac`A = r'' with clock := B`>> 1155 qpat_abbrev_tac`B = For C D E`>> 1156 rw[]>>pop_assum(qspecl_then[`B`,`A`] assume_tac)>> 1157 UNABBREV_ALL_TAC>>fs[]) 1158 >> 1159 `r'.clock ��� c'` by DECIDE_TAC>> 1160 imp_res_tac LTE_SUM>> 1161 imp_res_tac sem_t_clock_inc>>fs[]>> 1162 rename [�����(cdelta + r'.clock ��� r'.clock)���] >> 1163 pop_assum(qspec_then`cdelta+1` assume_tac)>>fs[]>> 1164 last_x_assum(qspec_then`c+(cdelta+1)`mp_tac)>>fs[]>> 1165 fs[STOP_def,dec_clock_def]>> 1166 `r'.clock + (cdelta+1)-1 = r'.clock + cdelta` by DECIDE_TAC>>fs[]); 1167 1168val simple_sem_t_div_iff_sem_t_div = Q.prove( 1169`���s t. 1170 sem_t_div s t ��� 1171 simple_sem_t_div s t`, 1172 metis_tac[sem_t_div_simple_sem_t_div,simple_sem_t_div_sem_t_div]) 1173 1174val _ = save_thm("simple_sem_t_div_iff_sem_t_div",simple_sem_t_div_iff_sem_t_div|>REWRITE_RULE[sem_t_div_def]); 1175 1176(* We can transfer the type soundness proof from FBS directly *) 1177val reln_type_soundness = Q.prove( 1178`!t. type_t F {} t ��� 1179 rel_semantics t ��� Crash`, 1180 ntac 2 strip_tac>>fs[rel_semantics_def]>> 1181 imp_res_tac type_soundness>>fs[semantics_def]>>pop_assum mp_tac>> 1182 IF_CASES_TAC>>fs[s_with_clock_def,init_store_def] 1183 >- 1184 (imp_res_tac sem_t_imp_simple_sem_t_reln>>fs[]>> 1185 imp_res_tac simple_sem_t_reln_ignores_clock>> 1186 pop_assum(qspec_then`0` assume_tac)>>fs[]>> 1187 IF_CASES_TAC>>fs[]>>metis_tac[]) 1188 >> 1189 ntac 3 (IF_CASES_TAC>>fs[])>> 1190 pop_assum mp_tac>>fs[]>> 1191 match_mp_tac sem_t_div_simple_sem_t_div>>fs[sem_t_div_def]>> 1192 metis_tac[FST]) 1193 1194(* Pretty big-step semantics, inductive interpretation only *) 1195 1196(* Wrapping the datatypes *) 1197val _ = Datatype ` 1198pbr = 1199 | Ter (r#state) 1200 | Div`; 1201 1202val _ = Datatype ` 1203pbt = 1204 | Trm t 1205 | Forn num pbr e e t`; 1206 1207val abort_def = Define` 1208 (abort flag Div ��� T) ��� 1209 (abort flag (Ter (r,s)) ��� �� is_rval r ��� (flag ��� r ��� Rbreak))` 1210 1211val (pb_sem_t_reln_rules,pb_sem_t_reln_ind,pb_sem_t_reln_cases) = Hol_reln` 1212(!s e r. 1213 sem_e_reln s e r 1214 ��� 1215 pb_sem_t_reln s (Trm(Exp e)) (Ter r)) ��� 1216(!s x t r. 1217 pb_sem_t_reln (s with store := s.store |+ (x,0)) (Trm t) r 1218 ��� 1219 pb_sem_t_reln s (Trm(Dec x t)) r) ��� 1220(* Initial For runs the guard *) 1221(!s r r1 e1 e2 t. 1222 sem_e_reln s e1 r1 ��� 1223 pb_sem_t_reln s (Forn 1 (Ter r1) e1 e2 t) r 1224 ��� 1225 pb_sem_t_reln s (Trm (For e1 e2 t)) r) ��� 1226(* For 1 checks the guard value (and possibly) runs the body *) 1227(!s s' e1 e2 t. 1228 pb_sem_t_reln s' (Forn 1 (Ter (Rval 0,s)) e1 e2 t) (Ter (Rval 0,s))) ��� 1229(!s s' e1 e2 t r r3 n. 1230 pb_sem_t_reln s (Trm t) r3 ��� 1231 pb_sem_t_reln s (Forn 2 r3 e1 e2 t) r ��� 1232 n ��� 0 ��� 1233 pb_sem_t_reln s' (Forn 1 (Ter (Rval n,s)) e1 e2 t) r) ��� 1234(* For 2 checks the result of the body and runs the step *) 1235(!s s' e1 e2 t. 1236 pb_sem_t_reln s' (Forn 2 (Ter (Rbreak,s)) e1 e2 t) (Ter (Rval 0,s))) ��� 1237(!s s' r r2 e1 e2 t n. 1238 sem_e_reln s e2 r2 ��� 1239 pb_sem_t_reln s (Forn 3 (Ter r2) e1 e2 t) r ��� 1240 pb_sem_t_reln s' (Forn 2 (Ter (Rval n,s)) e1 e2 t) r) ��� 1241(* For 3 runs the loop again *) 1242(!s s' r e1 e2 t n. 1243 pb_sem_t_reln s (Trm (For e1 e2 t)) r ��� 1244 pb_sem_t_reln s' (Forn 3 (Ter (Rval n,s)) e1 e2 t) r) ��� 1245(* One rule for all the breaks and divergence *) 1246(!s r e1 e2 t i. 1247 abort (i = 2) r ��� 1248 pb_sem_t_reln s (Forn i r e1 e2 t) r) ��� 1249(!s. 1250 pb_sem_t_reln s (Trm(Break)) (Ter (Rbreak, s))) ��� 1251(*Seq and If can be changed to pretty-big-step too, although they will have a similar number of raw rules*) 1252(!s s1 t1 t2 n1 r. 1253 pb_sem_t_reln s (Trm t1) (Ter (Rval n1, s1)) ��� 1254 pb_sem_t_reln s1 (Trm t2) r 1255 ��� 1256 pb_sem_t_reln s (Trm (Seq t1 t2)) r) ��� 1257(!s t1 t2 r. 1258 pb_sem_t_reln s (Trm t1) r ��� 1259 abort F r ��� 1260 pb_sem_t_reln s (Trm (Seq t1 t2)) r) ��� 1261(!s s1 e t1 t2 r. 1262 sem_e_reln s e (Rval 0, s1) ��� 1263 pb_sem_t_reln s1 (Trm t2) r 1264 ��� 1265 pb_sem_t_reln s (Trm (If e t1 t2)) r) ��� 1266(!s s1 e t1 t2 n r. 1267 sem_e_reln s e (Rval n, s1) ��� 1268 n ��� 0 ��� 1269 pb_sem_t_reln s1 (Trm t1) r 1270 ��� 1271 pb_sem_t_reln s (Trm (If e t1 t2)) r) ��� 1272(!s s1 e t1 t2 r. 1273 sem_e_reln s e (r, s1) ��� 1274 ~is_rval r 1275 ��� 1276 pb_sem_t_reln s (Trm (If e t1 t2)) (Ter (r, s1)))`; 1277 1278(* The first argument of pb_sem_t_size_reln is used as an explicit size measure to facilitate induction on derivation trees in our proofs *) 1279val (pb_sem_t_size_reln_rules,pb_sem_t_size_reln_ind,pb_sem_t_size_reln_cases) = Hol_reln` 1280(!s e r. 1281 sem_e_reln s e r 1282 ��� 1283 pb_sem_t_size_reln 0n s (Trm(Exp e)) (Ter r)) ��� 1284(!s x t r. 1285 pb_sem_t_size_reln h (s with store := s.store |+ (x,0)) (Trm t) r 1286 ��� 1287 pb_sem_t_size_reln (h+1) s (Trm(Dec x t)) r) ��� 1288(* Initial For runs the guard *) 1289(!s r r1 e1 e2 t. 1290 sem_e_reln s e1 r1 ��� 1291 pb_sem_t_size_reln h s (Forn 1 (Ter r1) e1 e2 t) r 1292 ��� 1293 pb_sem_t_size_reln (h+1) s (Trm (For e1 e2 t)) r) ��� 1294(* For 1 checks the guard value (and possibly) runs the body *) 1295(!s s' e1 e2 t. 1296 pb_sem_t_size_reln 0 s' (Forn 1 (Ter (Rval 0,s)) e1 e2 t) (Ter (Rval 0,s))) ��� 1297(!s s' e1 e2 t r r3 n. 1298 pb_sem_t_size_reln h s (Trm t) r3 ��� 1299 pb_sem_t_size_reln h' s (Forn 2 r3 e1 e2 t) r ��� 1300 n ��� 0 ��� 1301 pb_sem_t_size_reln (h+h'+1) s' (Forn 1 (Ter (Rval n,s)) e1 e2 t) r) ��� 1302(* For 2 checks the result of the body and runs the step *) 1303(!s s' e1 e2 t. 1304 pb_sem_t_size_reln 0 s' (Forn 2 (Ter (Rbreak,s)) e1 e2 t) (Ter (Rval 0,s))) ��� 1305(!s s' r r2 e1 e2 t n. 1306 sem_e_reln s e2 r2 ��� 1307 pb_sem_t_size_reln h s (Forn 3 (Ter r2) e1 e2 t) r ��� 1308 pb_sem_t_size_reln (h+1) s' (Forn 2 (Ter (Rval n,s)) e1 e2 t) r) ��� 1309(* For 3 runs the loop again *) 1310(!s s' r e1 e2 t n. 1311 pb_sem_t_size_reln h s (Trm (For e1 e2 t)) r ��� 1312 pb_sem_t_size_reln (h+1) s' (Forn 3 (Ter (Rval n,s)) e1 e2 t) r) ��� 1313(* One rule for all the breaks and divergence *) 1314(!s r e1 e2 t i. 1315 abort (i = 2) r ��� 1316 pb_sem_t_size_reln 0 s (Forn i r e1 e2 t) r) ��� 1317(!s. 1318 pb_sem_t_size_reln 0 s (Trm(Break)) (Ter (Rbreak, s))) ��� 1319(*Seq and If can be changed to pretty-big-step too, although they will have a similar number of raw rules*) 1320(!s s1 t1 t2 n1 r. 1321 pb_sem_t_size_reln h s (Trm t1) (Ter (Rval n1, s1)) ��� 1322 pb_sem_t_size_reln h' s1 (Trm t2) r 1323 ��� 1324 pb_sem_t_size_reln (h+h'+1) s (Trm (Seq t1 t2)) r) ��� 1325(!s t1 t2 r. 1326 pb_sem_t_size_reln h s (Trm t1) r ��� 1327 abort F r ��� 1328 pb_sem_t_size_reln (h+1) s (Trm (Seq t1 t2)) r) ��� 1329(!s s1 e t1 t2 r. 1330 sem_e_reln s e (Rval 0, s1) ��� 1331 pb_sem_t_size_reln h s1 (Trm t2) r 1332 ��� 1333 pb_sem_t_size_reln (h+1) s (Trm (If e t1 t2)) r) ��� 1334(!s s1 e t1 t2 n r. 1335 sem_e_reln s e (Rval n, s1) ��� 1336 n ��� 0 ��� 1337 pb_sem_t_size_reln h s1 (Trm t1) r 1338 ��� 1339 pb_sem_t_size_reln (h+1) s (Trm (If e t1 t2)) r) ��� 1340(!s s1 e t1 t2 r. 1341 sem_e_reln s e (r, s1) ��� 1342 ~is_rval r 1343 ��� 1344 pb_sem_t_size_reln 0 s (Trm (If e t1 t2)) (Ter (r, s1)))`; 1345 1346val _ = set_trace "Goalstack.print_goal_at_top" 0; 1347 1348val pbrsem_tac = simp[Once pb_sem_t_size_reln_cases] 1349 1350(* Connect pretty-big-step to relational semantics *) 1351val reln_to_pb_reln = prove(`` 1352 ���s t r. 1353 simple_sem_t_reln s t r ��� 1354 ���h. pb_sem_t_size_reln h s (Trm t) (Ter r)``, 1355 ho_match_mp_tac simple_sem_t_reln_ind>> 1356 rw[]>>TRY(pbrsem_tac>>metis_tac[abort_def]) 1357 (*FOR equivalence*) 1358 >- metis_tac[pb_sem_t_size_reln_cases,abort_def] 1359 >- 1360 (pbrsem_tac>>pbrsem_tac>>simp[abort_def]>> 1361 metis_tac[pb_sem_t_size_reln_cases,abort_def]) 1362 >- 1363 (pbrsem_tac>> 1364 qexists_tac`h+h'+3`>> 1365 qexists_tac`Rval n1,s'`>>pbrsem_tac>> 1366 qexists_tac`h`>>qexists_tac`h'+2`>>simp[]>> 1367 qexists_tac`Ter(Rval n2,s2)`>>pbrsem_tac>> 1368 qexists_tac`h'+1`>>qexists_tac`Rval n3,s''`>>pbrsem_tac) 1369 >- 1370 (pbrsem_tac>>metis_tac[pb_sem_t_size_reln_cases]) 1371 >- 1372 (pbrsem_tac>> 1373 qexists_tac`h+2`>> 1374 qexists_tac`Rval n1,s'`>>pbrsem_tac>> 1375 qexists_tac`h`>>qexists_tac`1`>>simp[]>> 1376 qexists_tac`Ter(Rval n2,s2)`>>pbrsem_tac>> 1377 qexists_tac`0`>>qexists_tac`r,s3`>>pbrsem_tac>> 1378 metis_tac[abort_def]) 1379 >- 1380 (pbrsem_tac>> 1381 qexists_tac`h+1`>> 1382 HINT_EXISTS_TAC>>pbrsem_tac>> 1383 qexists_tac`h`>>qexists_tac`0`>>simp[]>> 1384 HINT_EXISTS_TAC>>pbrsem_tac>> 1385 metis_tac[abort_def])) 1386 1387local val fs = fsrw_tac[] in 1388val pb_reln_to_reln = prove(`` 1389 ���n s t r. 1390 pb_sem_t_size_reln n s (Trm t) (Ter r) ��� 1391 simple_sem_t_reln s t r``, 1392 completeInduct_on`n`>>simp[Once pb_sem_t_size_reln_cases]>>rw[]>> 1393 TRY(semttac>>NO_TAC)>> 1394 `h < h+1 ��� 1395 h < h+(h'+1) ��� 1396 h' < h+(h'+1)` by DECIDE_TAC>> 1397 Cases_on`r`>>TRY(semttac>>metis_tac[abort_def])>> 1398 ntac 3 (pop_assum kall_tac)>> 1399 pop_assum mp_tac>> 1400 pbrsem_tac>>rw[]>> 1401 TRY(semttac>>metis_tac[abort_def])>> 1402 qpat_x_assum`pb_sem_t_size_reln A B (Forn 2 _ _ _ _) _` mp_tac>> 1403 pbrsem_tac>>rw[]>>fs[]>> 1404 `h' < h' +1 +1` by DECIDE_TAC>> 1405 TRY(semttac>>metis_tac[abort_def])>> 1406 qpat_x_assum`pb_sem_t_size_reln A B (Forn 3 _ _ _ _) _` mp_tac>> 1407 pbrsem_tac>>rw[]>>fs[]>> 1408 `h' < h' +2 +1` by DECIDE_TAC>> 1409 `h' < h'+(h''+1+1+1)+1` by DECIDE_TAC>> 1410 `h'' < h'+(h''+1+1+1)+1` by DECIDE_TAC>> 1411 TRY(semttac>>metis_tac[abort_def])) 1412end 1413 1414val pb_sem_t_size_reln_equiv_lemma1 = prove(`` 1415 ���n s t r. 1416 pb_sem_t_size_reln n s t r ��� 1417 pb_sem_t_reln s t r``, 1418 HO_MATCH_MP_TAC pb_sem_t_size_reln_ind \\ rw [] 1419 \\ once_rewrite_tac [pb_sem_t_reln_cases] \\ fs [] 1420 \\ metis_tac []); 1421 1422val pb_sem_t_size_reln_equiv_lemma2 = prove(`` 1423 ���s t r. 1424 pb_sem_t_reln s t r ==> 1425 ?n. pb_sem_t_size_reln n s t r``, 1426 HO_MATCH_MP_TAC pb_sem_t_reln_ind \\ rw [] 1427 \\ once_rewrite_tac [pb_sem_t_size_reln_cases] \\ fs [] 1428 \\ metis_tac []); 1429 1430val pb_sem_t_size_reln_equiv = store_thm("pb_sem_t_size_reln_equiv", 1431 ``���s t r. pb_sem_t_reln s t r ��� ���n. pb_sem_t_size_reln n s t r``, 1432 metis_tac [pb_sem_t_size_reln_equiv_lemma2,pb_sem_t_size_reln_equiv_lemma1]); 1433 1434(* Pretty printing for paper *) 1435val OMIT_def = Define `OMIT x = x`; 1436 1437val OMIT_INTRO = prove( 1438 ``(P1 ==> P2 ==> Q) ==> (P1 /\ OMIT P2 ==> Q)``, 1439 fs [OMIT_def]); 1440 1441val _ = Parse.add_infix("DOWNARROWe",450,Parse.NONASSOC) 1442val _ = Parse.add_infix("DOWNARROWt",450,Parse.NONASSOC) 1443 1444val DOWNARROWe_def = Define `$DOWNARROWe (y,x) z = sem_e_reln x y z`; 1445val DOWNARROWt_def = Define `$DOWNARROWt (y,x) z = simple_sem_t_reln x y z`; 1446 1447val simple_sem_t_reln_rules = save_thm("simple_sem_t_reln_rules", 1448 simple_sem_t_reln_rules |> REWRITE_RULE [GSYM DOWNARROWe_def, 1449 GSYM DOWNARROWt_def]); 1450 1451val simple_sem_t_reln_ind = save_thm("simple_sem_t_reln_ind", 1452 simple_sem_t_reln_ind 1453 |> REWRITE_RULE [GSYM DOWNARROWe_def, GSYM DOWNARROWt_def] 1454 |> Q.SPEC `P` |> UNDISCH_ALL 1455 |> Q.SPECL [`s`,`t`,`r`] |> Q.GENL [`t`,`s`,`r`] 1456 |> DISCH_ALL |> Q.GEN `P` |> Q.SPEC `\s t r. P (t,s) r` 1457 |> SIMP_RULE std_ss [] |> Q.GEN `P` 1458 |> SPEC_ALL 1459 |> REWRITE_RULE [GSYM AND_IMP_INTRO] |> DISCH T 1460 |> MATCH_MP OMIT_INTRO 1461 |> MATCH_MP OMIT_INTRO 1462 |> MATCH_MP OMIT_INTRO 1463 |> MATCH_MP OMIT_INTRO 1464 |> MATCH_MP OMIT_INTRO 1465 |> MATCH_MP OMIT_INTRO 1466 |> MATCH_MP OMIT_INTRO 1467 |> MATCH_MP OMIT_INTRO 1468 |> REWRITE_RULE [AND_IMP_INTRO] 1469 |> UNDISCH 1470 |> Q.SPECL [`FST (ts:t # state)`,`SND (ts:t # state)`,`rs`] 1471 |> Q.GEN `rs` 1472 |> Q.GEN `ts` 1473 |> SIMP_RULE std_ss [] 1474 |> DISCH_ALL 1475 |> Q.GEN `P` 1476 |> REWRITE_RULE [GSYM CONJ_ASSOC]); 1477 1478val lemma = prove( 1479 ``b1 \/ b2 \/ b3 \/ b4 \/ b5 \/ b6 <=> 1480 OMIT b1 \/ OMIT b2 \/ OMIT b3 \/ b4 \/ b5 \/ OMIT b6``, 1481 fs [OMIT_def]); 1482 1483val lemma2 = prove( 1484 ``OMIT (b1 \/ b2) <=> OMIT b1 \/ OMIT b2``, 1485 fs [OMIT_def]); 1486 1487val sample_cases_thm = save_thm("sample_cases_thm", 1488 simple_sem_t_reln_cases 1489 |> Q.SPECL [`s`,`t`,`res`] 1490 |> Q.GENL [`s`,`t`,`res`] 1491 |> ONCE_REWRITE_RULE [lemma] 1492 |> REWRITE_RULE [lemma2]) 1493 1494val _ = export_theory (); 1495