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