1open HolKernel boolLib bossLib Parse BasicProvers 2 integerTheory stringTheory alistTheory listTheory pred_setTheory 3 pairTheory optionTheory finite_mapTheory arithmeticTheory 4 5fun term_rewrite tms = let 6 fun f tm = ASSUME (list_mk_forall(free_vars tm,tm)) 7 in rand o concl o QCONV (REWRITE_CONV (map f tms)) end 8 9(* 10In this file, we demonstrate that the Functional Big-Step semantics 11style is suitable for proofs of type soundness. In particular, we 12define an ML-like language, heavily inspired by Core ML in Wright and 13Felleisen's "A Syntactic Approach to Type Soundness" (1992) (hereafter 14W&F), using functional big-step semantics rather than small-step 15semantics. We then prove the type soundness using the induction 16theorem generated from the definition of the functional big-step 17semantics. 18*) 19 20(* TODO: from CakeML's miscLib.sml *) 21val SWAP_IMP = PROVE[]``(P ==> Q ==> R) ==> (Q ==> P ==> R)`` 22val IMP_IMP = METIS_PROVE[]``(P /\ (Q ==> R)) ==> ((P ==> Q) ==> R)`` 23val discharge_hyps = match_mp_tac IMP_IMP >> conj_tac 24fun match_exists_tac tm (g as (_,w)) = 25 let 26 val (vs,b) = strip_exists w 27 val vs = map (fst o dest_var o variant (free_vars tm)) vs 28 fun k (g as (_,w)) = 29 let 30 val (_,b) = strip_exists w 31 val cs = strip_conj b val c = hd cs 32 val (tms,_) = match_term c tm 33 val xs = map #redex tms 34 val ys = map #residue tms 35 fun sorter ls = xs@(List.filter(not o Lib.C tmem xs)ls) 36 in 37 CONV_TAC(RESORT_EXISTS_CONV sorter) >> 38 map_every exists_tac ys 39 end g 40 in 41 CONV_TAC(RENAME_VARS_CONV vs) >> k 42 end g 43(* -- *) 44 45val _ = new_theory"typeSound" 46 47(* TODO: move to HOL standard lib *) 48val LUPDATE_ID = store_thm("LUPDATE_ID", 49 ``���n ls. n < LENGTH ls ��� (LUPDATE (EL n ls) n ls = ls)``, 50 rw[LIST_EQ_REWRITE,EL_LUPDATE] >> rw[]) 51 52val FLOOKUP_f_o_f = store_thm("FLOOKUP_f_o_f", 53 ``FLOOKUP (f1 f_o_f f2) k = 54 case FLOOKUP f2 k of 55 | NONE => NONE 56 | SOME v => FLOOKUP f1 v``, 57 simp[FLOOKUP_DEF] >> 58 simp[f_o_f_DEF] >> rw[] >> fs[]) 59(* -- *) 60 61(* Syntax *) 62 63val _ = Datatype`lit = 64 Int int | Unit` 65 66val _ = Datatype`exp = 67 | Lit lit 68 | Var string 69 | App exp exp 70 | Let string exp exp 71 | Fun string exp 72 | Funrec string string exp 73 | Ref exp 74 | Deref exp 75 | Assign exp exp 76 | Letexn string exp 77 | Raise exp exp 78 | Handle exp exp exp` 79 80(* Differences from W&F: 81 - we have specific constants (ints and unit) 82 - we bind one exception at a time 83 - we use Funrec rather than Y 84 - we use explicit syntactic forms for applications of primitives like Ref, 85 Raise, whereas they treat them as curried function values and re-use App to 86 apply them; in our syntax we can of course achieve the same in e by: 87 Let "ref" (Fun "x" (Ref (Var "x"))) e. *) 88 89(* 90The major difference is our separate class of values, which are not in mutual 91recursion with expressions, and include closures. Using closures/environments 92is a stylistic choice that works well with functional big-step and lets us 93avoid defining capture-avoiding substitution over terms (which W&F gloss over 94anyway). 95*) 96 97(* Values *) 98 99val _ = Datatype`v = 100 | Litv lit 101 | Clos ((string,v) alist) string exp 102 | Closrec ((string,v) alist) string string exp 103 | Loc num 104 | Exn num` 105 106val v_induction = theorem"v_induction" 107val v_ind = 108 v_induction 109 |> Q.SPECL[`P`,`EVERY (P o SND)`,`P o SND`] 110 |> SIMP_RULE (srw_ss()) [] 111 |> UNDISCH |> CONJUNCT1 |> DISCH_ALL 112 |> GEN_ALL 113 |> curry save_thm "v_ind" 114val v_size_def = definition"v_size_def" 115 116val _ = type_abbrev("env",``:(string,v) alist``) 117 118(* Semantics *) 119 120(* 121The semantics has a state containing the clock, the store, and the number of 122exceptions that have been created. Whereas W&F's treatment of exceptions is 123intimately tied up with the mechanics of their small-step semantics, we simply 124generate a new exception value for every (dynamic) Letexn expression. 125*) 126 127val _ = Datatype` 128 state = <| clock : num; refs : v list; next_exn : num |>` 129 130val state_component_equality = theorem"state_component_equality" 131 132(* machinery for the functional big-step definition *) 133 134val check_clock_def = Define ` 135 check_clock s' s = 136 s' with clock := (if s'.clock ��� s.clock then s'.clock else s.clock)`; 137 138val check_clock_id = prove( 139 ``!s s'. s.clock ��� s'.clock ��� check_clock s s' = s``, 140 rw [check_clock_def, state_component_equality]); 141 142val dec_clock_def = Define ` 143 dec_clock s = s with clock := s.clock - 1`; 144 145val dec_clock_refs = store_thm("dec_clock_refs[simp]", 146 ``(dec_clock s).refs = s.refs``, 147 rw[dec_clock_def]) 148 149val dec_clock_next_exn = store_thm("dec_clock_next_exn[simp]", 150 ``(dec_clock s).next_exn = s.next_exn``, 151 rw[dec_clock_def]) 152 153val is_closure_def = Define` 154 is_closure (Clos _ _ _) = T ��� 155 is_closure (Closrec _ _ _ _) = T ��� 156 is_closure _ = F` 157val _ = export_rewrites["is_closure_def"] 158 159(* results *) 160 161val _ = Datatype` 162 r = Rval v 163 | Rraise num v 164 | Rfail 165 | Rtimeout` 166 167(* big-step semantics as a function *) 168 169val sem_def = tDefine"sem"` 170 (sem env s (Lit i) = (Rval (Litv i), s)) ��� 171 (sem env s (Var x) = 172 case ALOOKUP env x of 173 | NONE => (Rfail, s) 174 | SOME v => (Rval v, s)) ��� 175 (sem env s (App e1 e2) = 176 case sem env s e1 of 177 | (Rval v1, s1) => 178 (case sem env (check_clock s1 s) e2 of 179 | (Rval v2, s2) => 180 if s.clock ��� 0 ��� s2.clock ��� 0 then 181 (case v1 of 182 | Clos env' x e => 183 sem ((x,v2)::env') (dec_clock (check_clock s2 s)) e 184 | Closrec env' f x e => 185 sem ((x,v2)::(f,v1)::env') (dec_clock (check_clock s2 s)) e 186 | _ => (Rfail, s2)) 187 else (Rtimeout, s2) 188 | res => res) 189 | res => res) ��� 190 (sem env s (Let x e1 e2) = 191 case sem env s e1 of 192 | (Rval v1, s1) => sem ((x,v1)::env) (check_clock s1 s) e2 193 | res => res) ��� 194 (sem env s (Fun x e) = (Rval (Clos env x e), s)) ��� 195 (sem env s (Funrec f x e) = (Rval (Closrec env f x e), s)) ��� 196 (sem env s (Ref e) = 197 case sem env s e of 198 | (Rval v, s) => (Rval (Loc (LENGTH s.refs)), s with refs := s.refs ++ [v]) 199 | res => res) ��� 200 (sem env s (Deref e) = 201 case sem env s e of 202 | (Rval (Loc n), s) => (if n < LENGTH s.refs then Rval (EL n s.refs) else Rfail, s) 203 | (Rval _, s) => (Rfail, s) 204 | res => res) ��� 205 (sem env s (Assign e1 e2) = 206 case sem env s e1 of 207 | (Rval v1, s1) => 208 (case sem env (check_clock s1 s) e2 of 209 | (Rval v2, s2) => 210 (case v1 of 211 | Loc n => 212 if n < LENGTH s2.refs then 213 (Rval (Litv Unit), s2 with refs := LUPDATE v2 n s2.refs) 214 else (Rfail, s2) 215 | _ => (Rfail, s2)) 216 | res => res) 217 | res => res) ��� 218 (sem env s (Letexn x e) = 219 sem ((x,Exn (s.next_exn))::env) (s with next_exn := s.next_exn + 1) e) ��� 220 (sem env s (Raise e1 e2) = 221 case sem env s e1 of 222 | (Rval v1, s1) => 223 (case sem env (check_clock s1 s) e2 of 224 | (Rval v2, s2) => 225 (case v1 of 226 | Exn n => (Rraise n v2, s2) 227 | _ => (Rfail, s2)) 228 | res => res) 229 | res => res) ��� 230 (sem env s (Handle e3 e1 e2) = 231 case sem env s e1 of 232 | (Rval v1, s1) => 233 (case v1 of 234 | Exn n => 235 (case sem env (check_clock s1 s) e2 of 236 | (Rval v2, s2) => 237 if is_closure v2 then 238 (case sem env (check_clock s2 s) e3 of 239 | (Rraise n3 v3, s3) => 240 if n3 = n then 241 if s.clock ��� 0 ��� s3.clock ��� 0 then 242 (case v2 of 243 | Clos env' x e => 244 sem ((x,v3)::env') (dec_clock (check_clock s3 s)) e 245 | Closrec env' f x e => 246 sem ((x,v3)::(f,v2)::env') (dec_clock (check_clock s3 s)) e) 247 else (Rtimeout, s3) 248 else (Rraise n3 v3, s3) 249 | res => res) 250 else (Rfail, s2) 251 | res => res) 252 | _ => (Rfail, s1)) 253 | res => res)` 254(WF_REL_TAC`inv_image (measure I LEX measure exp_size) 255 (��(env,s,e). (s.clock,e))` >> 256 rpt strip_tac >> TRY DECIDE_TAC >> 257 fs[check_clock_def,dec_clock_def] >> 258 rw[] >> fsrw_tac[ARITH_ss][]) 259 260(* 261clean-up of the definition and induction theorem, removing the check_clock 262machinery that was used to get the function through the termination checker 263*) 264 265val sem_ind = theorem"sem_ind" 266 267val sem_clock = store_thm("sem_clock", 268 ``���env s e r s'. sem env s e = (r, s') ��� s'.clock ��� s.clock``, 269 ho_match_mp_tac sem_ind >> 270 rpt conj_tac >> 271 simp[sem_def] >> 272 rpt gen_tac >> 273 BasicProvers.EVERY_CASE_TAC >> 274 simp[check_clock_def,dec_clock_def] >> 275 rpt(IF_CASES_TAC >> simp[]) >> 276 rpt strip_tac >> res_tac >> simp[] >> fs[]) 277 278val r = term_rewrite [``check_clock s1 s = s1``, 279 ``s.clock <> 0 /\ s1.clock <> 0 <=> s1.clock <> 0``] 280 281val sem_def = store_thm("sem_def", 282 sem_def |> concl |> r, 283 rpt strip_tac >> 284 rw[Once sem_def] >> 285 BasicProvers.CASE_TAC >> 286 imp_res_tac sem_clock >> 287 simp[check_clock_id] >> 288 BasicProvers.CASE_TAC >> 289 imp_res_tac sem_clock >> 290 simp[check_clock_id] >> 291 BasicProvers.EVERY_CASE_TAC >> fs[] >> 292 imp_res_tac sem_clock >> 293 simp[check_clock_id] >> 294 `F` suffices_by rw[] >> 295 DECIDE_TAC) 296 297val sem_ind = store_thm("sem_ind", 298 sem_ind |> concl |> r, 299 ntac 2 strip_tac >> 300 ho_match_mp_tac sem_ind >> 301 rw[] >> 302 first_x_assum match_mp_tac >> 303 rw[] >> fs[] >> 304 res_tac >> 305 imp_res_tac sem_clock >> 306 fsrw_tac[ARITH_ss][check_clock_id] >> rfs[] >> 307 fsrw_tac[ARITH_ss][check_clock_id]) 308 309(* alternative un-clocked relational big-step semantics for comparison *) 310 311val dest_closure_def = Define` 312 (dest_closure v (Clos env x e) = SOME (((x,v)::env),e)) ��� 313 (dest_closure v (Closrec env f x e) = SOME (((x,v)::(f,Closrec env f x e)::env),e)) ��� 314 (dest_closure _ _ = NONE)`; 315val _ = export_rewrites["dest_closure_def"]; 316 317val (eval_rules,eval_ind,eval_cases) = Hol_reln` 318 (eval env s (Lit i) (Rval (Litv i), s)) ��� 319 (ALOOKUP env x = NONE ��� 320 eval env s (Var x) (Rfail, s)) ��� 321 (ALOOKUP env x = (SOME v) ��� 322 eval env s (Var x) (Rval v, s)) ��� 323 (eval env s e1 (Rval v1, s1) ��� 324 eval env s1 e2 (Rval v2, s2) ��� 325 dest_closure v2 v1 = SOME (env',e) ��� 326 eval env' (dec_clock s2) e res 327 ��� 328 eval env s (App e1 e2) res) ��� 329 (eval env s e1 (Rval v1, s1) ��� 330 eval env s1 e2 (Rval v2, s2) ��� 331 dest_closure v2 v1 = NONE 332 ��� 333 eval env s (App e1 e2) (Rfail,s2)) ��� 334 (eval env s e1 (Rval v1, s1) ��� 335 eval env s1 e2 res ��� (���v. FST res ��� Rval v) 336 ��� 337 eval env s (App e1 e2) res) ��� 338 (eval env s e1 res ��� (���v. FST res ��� Rval v) 339 ��� 340 eval env s (App e1 e2) res) ��� 341 (eval env s e1 (Rval v1,s1) ��� 342 eval ((x,v1)::env) s1 e2 res ��� 343 eval env s (Let x e1 e2) res) ��� 344 (eval env s e1 res ��� (���v. FST res ��� Rval v) ��� 345 eval env s (Let x e1 e2) res) ��� 346 (eval env s (Fun x e) (Rval (Clos env x e),s)) ��� 347 (eval env s (Funrec f x e) (Rval (Closrec env f x e),s)) ��� 348 (eval env s e (Rval v1,s1) ��� 349 eval env s (Ref e) (Rval (Loc (LENGTH s1.refs)), s1 with refs := s1.refs ++ [v1])) ��� 350 (eval env s e res ��� (���v. FST res ��� Rval v) ��� 351 eval env s (Ref e) res) ��� 352 (eval env s e (Rval (Loc n), s1) ��� 353 n < LENGTH s1.refs 354 ��� 355 eval env s (Deref e) (Rval (EL n s1.refs),s1)) ��� 356 (eval env s e (Rval (Loc n), s1) ��� 357 ��(n < LENGTH s1.refs) 358 ��� 359 eval env s (Deref e) (Rfail,s1)) ��� 360 (eval env s e (Rval v, s1) ��� (���n. v ��� Loc n) ��� 361 eval env s (Deref e) (Rfail, s1)) ��� 362 (eval env s e res ��� (���v. FST res ��� Rval v) ��� 363 eval env s (Deref e) res) ��� 364 (eval env s e1 (Rval v1, s1) ��� 365 eval env s1 e2 (Rval v2, s2) ��� 366 (v1 = Loc n) ��� n < LENGTH s2.refs 367 ��� 368 eval env s (Assign e1 e2) (Rval (Litv Unit), s2 with refs := LUPDATE v2 n s2.refs)) ��� 369 (eval env s e1 (Rval v1, s1) ��� 370 eval env s1 e2 (Rval v2, s2) ��� 371 (���n. v1 = Loc n ��� ��(n < LENGTH s2.refs)) 372 ��� 373 eval env s (Assign e1 e2) (Rfail, s2)) ��� 374 (eval env s e1 (Rval v1, s1) ��� 375 eval env s1 e2 res ��� (���v. FST res ��� Rval v) 376 ��� 377 eval env s (Assign e1 e2) res) ��� 378 (eval env s e1 res ��� (���v. FST res ��� Rval v) ��� 379 eval env s (Assign e1 e2) res) ��� 380 (eval ((x,Exn(s.next_exn))::env) (s with next_exn := s.next_exn + 1) e res ��� 381 eval env s (Letexn x e) res) ��� 382 (eval env s e1 (Rval v1, s1) ��� 383 eval env s1 e2 (Rval v2, s2) ��� 384 (v1 = Exn n) 385 ��� 386 eval env s (Raise e1 e2) (Rraise n v2, s2)) ��� 387 (eval env s e1 (Rval v1, s1) ��� 388 eval env s1 e2 (Rval v2, s2) ��� 389 (���n. v1 ��� Exn n) 390 ��� 391 eval env s (Raise e1 e2) (Rfail, s2)) ��� 392 (eval env s e1 (Rval v1, s1) ��� 393 eval env s1 e2 res ��� (���v. FST res ��� Rval v) 394 ��� 395 eval env s (Raise e1 e2) res) ��� 396 (eval env s e1 res ��� (���v. FST res ��� Rval v) 397 ��� 398 eval env s (Raise e1 e2) res) ��� 399 (eval env s e1 (Rval v1, s1) ��� 400 (v1 = Exn n) ��� 401 eval env s1 e2 (Rval v2, s2) ��� 402 dest_closure v3 v2 = SOME (env',e) ��� 403 eval env s2 e3 (Rraise n v3, s3) ��� 404 eval env' (dec_clock s3) e res 405 ��� 406 eval env s (Handle e3 e1 e2) res) ��� 407 (eval env s e1 (Rval v1, s1) ��� 408 (v1 = Exn n) ��� 409 eval env s1 e2 (Rval v2, s2) ��� 410 dest_closure v3 v2 = SOME (env',e) ��� 411 eval env s2 e3 (Rraise n3 v3, s3) ��� 412 (n3 ��� n) 413 ��� 414 eval env s (Handle e3 e1 e2) (Rraise n3 v3, s3)) ��� 415 (eval env s e1 (Rval v1, s1) ��� 416 (v1 = Exn n) ��� 417 eval env s1 e2 (Rval v2, s2) ��� 418 dest_closure v3 v2 = SOME (env',e) ��� 419 eval env s2 e3 res ��� (���n v. FST res ��� Rraise n v) 420 ��� 421 eval env s (Handle e3 e1 e2) res) ��� 422 (eval env s e1 (Rval v1, s1) ��� 423 (v1 = Exn n) ��� 424 eval env s1 e2 (Rval v2, s2) ��� 425 dest_closure v3 v2 = NONE 426 ��� 427 eval env s (Handle e3 e1 e2) (Rfail, s2)) ��� 428 (eval env s e1 (Rval v1, s1) ��� 429 (v1 = Exn n) ��� 430 eval env s1 e2 res ��� (���v. FST res ��� Rval v) 431 ��� 432 eval env s (Handle e3 e1 e2) res) ��� 433 (eval env s e1 (Rval v1, s1) ��� 434 (���n. v1 ��� Exn n) 435 ��� 436 eval env s (Handle e3 e1 e2) (Rfail, s1)) ��� 437 (eval env s e1 res ��� (���v. FST res ��� Rval v) 438 ��� 439 eval env s (Handle e3 e1 e2) res)` 440 441(* sanity-check: equivalence of semantics *) 442 443val v_distinct = theorem"v_distinct"; 444val v_nchotomy = theorem"v_nchotomy"; 445val v_11 = theorem"v_11"; 446val r_distinct = theorem"r_distinct"; 447 448val sem_imp_eval = Q.store_thm("sem_imp_eval", 449 `���env s e. FST (sem env s e) ��� Rtimeout ��� 450 eval env s e (sem env s e)`, 451 ho_match_mp_tac sem_ind >> rw[sem_def] 452 >- rw[Once eval_cases] 453 >- ( 454 rw[Once eval_cases] >> 455 every_case_tac >> fs[] 456 ) 457 >- ( 458 every_case_tac >> fs[] >> rw[] >> rfs[] >> 459 rw[Once eval_cases] >> 460 metis_tac[dest_closure_def] 461 ) 462 >- ( 463 every_case_tac >> fs[] >> rw[] >> 464 rw[Once eval_cases] >> 465 metis_tac[] 466 ) 467 >- rw[Once eval_cases] 468 >- rw[Once eval_cases] 469 >- ( 470 every_case_tac >> fs[] >> rw[] >> 471 rw[Once eval_cases] >> 472 metis_tac[] 473 ) 474 >- ( 475 every_case_tac >> fs[] >> rw[] >> 476 rw[Once eval_cases] >> 477 metis_tac[v_distinct] 478 ) 479 >- ( 480 every_case_tac >> fs[] >> rw[] >> rfs[] >> 481 rw[Once eval_cases] >> 482 metis_tac[v_distinct,FST,r_distinct,v_11] 483 ) 484 >- rw[Once eval_cases] 485 >- ( 486 every_case_tac >> fs[] >> rw[] >> 487 rw[Once eval_cases] >> 488 metis_tac[v_distinct,FST,r_distinct] 489 ) 490 >- ( 491 BasicProvers.CASE_TAC >> fs[] >> 492 BasicProvers.CASE_TAC >> fs[] >> 493 BasicProvers.CASE_TAC >> fs[] >> 494 BasicProvers.CASE_TAC >> fs[] >> 495 BasicProvers.CASE_TAC >> fs[] >> 496 BasicProvers.CASE_TAC >> fs[] >> 497 BasicProvers.CASE_TAC >> fs[] >> 498 rw[Once eval_cases] >> 499 every_case_tac >> fs[] >> 500 metis_tac[is_closure_def,dest_closure_def,v_distinct,v_nchotomy] 501 ) 502 ); 503 504val dest_closure_SOME_is_closure = Q.prove( 505 `dest_closure x y = SOME z ��� is_closure y`, 506 Cases_on`y`>>rw[]) 507 508val eval_imp_sem = Q.store_thm("eval_imp_sem", 509 `���env s e res. 510 eval env s e res ��� 511 FST (sem env s e) = Rtimeout ��� 512 sem env s e = res`, 513 ho_match_mp_tac eval_ind >> rw[sem_def] >> 514 BasicProvers.CASE_TAC >> fs[] >> rw[] >> 515 TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >> 516 TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >> 517 TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >> 518 TRY(BasicProvers.CASE_TAC >> fs[] >> rw[]) >> 519 imp_res_tac dest_closure_SOME_is_closure >> fs[] >> 520 every_case_tac >> fs[]); 521 522(* Typing *) 523 524(* 525Whereas W&F use two categories of type variables (applicative and imperative), 526we follow the more modern approach to making let-polymorphism sound with a 527value restriction. 528*) 529 530val is_value_def = Define` 531 is_value (Lit _) = T ��� 532 is_value (Var _) = T ��� 533 is_value (Fun _ _) = T ��� 534 is_value (Funrec _ _ _) = T ��� 535 is_value _ = F` 536val _ = export_rewrites["is_value_def"] 537 538(* syntax of types *) 539 540val _ = Datatype`tctor = 541 | TC_int 542 | TC_fn 543 | TC_ref 544 | TC_unit 545 | TC_exn` 546 547val _ = Datatype`t = 548 | Tvar string 549 | Tapp (t list) tctor` 550 551val t_size_def = definition"t_size_def" 552val t_induction = theorem"t_induction" 553 554val t_ind = 555 t_induction 556 |> Q.SPECL[`P`,`EVERY P`] 557 |> SIMP_RULE (srw_ss()) [] 558 |> UNDISCH |> CONJUNCT1 |> DISCH_ALL 559 |> GEN_ALL 560 |> curry save_thm "t_ind" 561 562val _ = overload_on("Tint",``Tapp [] TC_int``) 563val _ = overload_on("Tfn",``��t1 t2. Tapp [t1;t2] TC_fn``) 564val _ = overload_on("Tref",``��t. Tapp [t] TC_ref``) 565val _ = overload_on("Tunit",``Tapp [] TC_unit``) 566val _ = overload_on("Texn",``��t. Tapp [t] TC_exn``) 567 568(* substitution for variables in a type *) 569 570val tysubst_def = tDefine"tysubst"` 571 (tysubst s (Tvar x) = 572 (case FLOOKUP s x of 573 | SOME t => t 574 | NONE => Tvar x)) ��� 575 tysubst s (Tapp ts tc) = 576 Tapp (MAP (tysubst s) ts) tc` 577(WF_REL_TAC`measure (t_size o SND)` >> 578 rpt gen_tac >> Induct_on`ts` >> 579 rw[t_size_def] >> res_tac >>simp[]) 580val tysubst_def = 581 tysubst_def 582 |> SIMP_RULE (std_ss++boolSimps.ETA_ss)[] 583 |> curry save_thm "tysubst_def" 584val _ = export_rewrites["tysubst_def"] 585 586val tysubst_ind = theorem"tysubst_ind" 587 588(* free variables in a type *) 589 590val tyvars_def = tDefine"tyvars"` 591 (tyvars (Tvar x) = {x}) ��� 592 (tyvars (Tapp ts _) = BIGUNION (IMAGE tyvars (set ts)))` 593(WF_REL_TAC`measure (t_size)` >> 594 rpt gen_tac >> Induct_on`ts` >> 595 rw[t_size_def] >> res_tac >>simp[]) 596val tyvars_def = 597 tyvars_def 598 |> SIMP_RULE (std_ss++boolSimps.ETA_ss)[] 599 |> curry save_thm "tyvars_def" 600val _ = export_rewrites["tyvars_def"] 601 602(* 603A type environment is a map from (expression) variables to type schemes, where 604a type scheme is a type some of whose variables are considered bound. We 605represent a type scheme by (tvs:string set, t:t), which is t with the variables 606in tvs bound. 607*) 608 609(* free variables in a type environment *) 610 611val tenv_vars_def = Define` 612 tenv_vars tenv = 613 BIGUNION (IMAGE ((��(tvs,t). tyvars t DIFF tvs) o SND) (set tenv))` 614 615val tenv_vars_cons = store_thm("tenv_vars_cons", 616 ``tenv_vars ((x,tvs,t)::tenv) = 617 tyvars t DIFF tvs ��� tenv_vars tenv``, 618 rw[tenv_vars_def]) 619 620(* typing relation *) 621 622val (type_e_rules,type_e_ind,type_e_cases) = Hol_reln` 623 (type_e tenv (Lit (Int i)) Tint) ��� 624 (type_e tenv (Lit Unit) Tunit) ��� 625 (ALOOKUP tenv x = SOME (tvs,t) ��� FDOM s ��� tvs 626 ��� type_e tenv (Var x) (tysubst s t)) ��� 627 (type_e tenv e1 (Tfn t1 t2) ��� 628 type_e tenv e2 t1 629 ��� type_e tenv (App e1 e2) t2) ��� 630 (is_value e1 ��� 631 type_e tenv e1 t1 ��� 632 type_e ((x,(tyvars t1 DIFF (tenv_vars tenv),t1))::tenv) e2 t2 633 ��� type_e tenv (Let x e1 e2) t2) ��� 634 (��is_value e1 ��� 635 type_e tenv e1 t1 ��� 636 type_e ((x,({},t1))::tenv) e2 t2 637 ��� type_e tenv (Let x e1 e2) t2) ��� 638 (type_e ((x,({},t1))::tenv) e t2 639 ��� type_e tenv (Fun x e) (Tfn t1 t2)) ��� 640 (type_e ((x,({},t1))::(f,({},Tfn t1 t2))::tenv) e t2 641 ��� type_e tenv (Funrec f x e) (Tfn t1 t2)) ��� 642 (type_e tenv e t ��� 643 type_e tenv (Ref e) (Tref t)) ��� 644 (type_e tenv e (Tref t) ��� 645 type_e tenv (Deref e) t) ��� 646 (type_e tenv e1 (Tref t) ��� 647 type_e tenv e2 t ��� 648 type_e tenv (Assign e1 e2) Tunit) ��� 649 (type_e ((x,({},Texn t1))::tenv) e t2 650 ��� type_e tenv (Letexn x e) t2) ��� 651 (type_e tenv e1 (Texn t) ��� 652 type_e tenv e2 t 653 ��� type_e tenv (Raise e1 e2) t2) ��� 654 (type_e tenv e3 t3 ��� 655 type_e tenv e1 (Texn t1) ��� 656 type_e tenv e2 (Tfn t1 t3) 657 ��� type_e tenv (Handle e3 e1 e2) t3)` 658 659(* 660To state the type soundness theorem, we also need a typing relation on values. 661The typing relation on values has two parameters, rt and et, indicating the 662types of references and exceptions. 663*) 664 665val (type_v_rules,type_v_ind,type_v_cases) = Hol_reln` 666 (type_v rt et (Litv (Int i)) Tint) ��� 667 (type_v rt et (Litv (Unit)) Tunit) ��� 668 (type_env rt et env tenv ��� 669 type_e ((x,({},t1))::tenv) e t2 670 ��� type_v rt et (Clos env x e) (Tfn t1 t2)) ��� 671 (type_env rt et env tenv ��� 672 type_e ((x,({},t1))::(f,({},Tfn t1 t2))::tenv) e t2 673 ��� type_v rt et (Closrec env f x e) (Tfn t1 t2)) ��� 674 (n < LENGTH rt 675 ��� type_v rt et (Loc n) (Tref (EL n rt))) ��� 676 (n < LENGTH et 677 ��� type_v rt et (Exn n) (Texn (EL n et))) ��� 678 (type_env rt et [] []) ��� 679 (tvs ��� tyvars t ��� 680 (���s. FDOM s ��� tvs ��� type_v rt et v (tysubst s t)) ��� 681 type_env rt et env tenv 682 ��� type_env rt et ((x,v)::env) ((x,(tvs,t))::tenv))` 683 684(* abbreviation for: a value has all the types represented by a type scheme *) 685val _ = overload_on("type_v_ts",``��rt et v tvs t. ���s. FDOM s ��� tvs ��� type_v rt et v (tysubst s t)``) 686 687(* we now have a series of lemmas about the type system *) 688 689val type_e_clauses = 690 [``type_e tenv (Lit i) t`` 691 ,``type_e tenv (Var x) t`` 692 ,``type_e tenv (App e1 e2) t`` 693 ,``type_e tenv (Let x e1 e2) t`` 694 ,``type_e tenv (Fun x e) t`` 695 ,``type_e tenv (Funrec f x e) t`` 696 ,``type_e tenv (Ref e) t`` 697 ,``type_e tenv (Deref e) t`` 698 ,``type_e tenv (Assign e1 e2) t`` 699 ,``type_e tenv (Letexc x e) t`` 700 ,``type_e tenv (Raise e1 e2) t`` 701 ,``type_e tenv (Handle e3 e1 e2) t`` 702 ] 703 |> List.map (SIMP_CONV (srw_ss()) [Once type_e_cases]) 704 |> LIST_CONJ 705 706val type_v_clauses = 707 [``type_v s z (Litv i) t`` 708 ,``type_v s z (Clos env x e) t`` 709 ,``type_v s z (Closrec env f x e) t`` 710 ,``type_v s z (Loc n) t`` 711 ,``type_v s z (Exn n) t`` 712 ] 713 |> List.map (SIMP_CONV (srw_ss()) [Once type_v_cases]) 714 |> LIST_CONJ 715 716val type_env_clauses = 717 [``type_env s z [] tenv`` 718 ,``type_env s z (x::y) tenv`` 719 ] 720 |> List.map (SIMP_CONV (srw_ss()) [Once type_v_cases]) 721 |> LIST_CONJ 722 723val type_v_extend = store_thm("type_v_extend", 724 ``(���v t. type_v s e v t ��� type_v (s++s') (e++e') v t) ��� 725 (���env tenv. type_env s e env tenv ��� type_env (s++s') (e++e') env tenv)``, 726 ho_match_mp_tac type_v_ind >> 727 simp[type_v_clauses,type_env_clauses] >> 728 rw[] >> simp[rich_listTheory.EL_APPEND1] >> metis_tac[]) 729 730val FINITE_tyvars = store_thm("FINITE_tyvars[simp]", 731 ``���t. FINITE (tyvars t)``, 732 ho_match_mp_tac t_ind >> simp[] >> 733 simp[EVERY_MEM,PULL_EXISTS]) 734 735val FINITE_tenv_vars = store_thm("FINITE_tenv_vars[simp]", 736 ``FINITE (tenv_vars tenv)``, 737 rw[tenv_vars_def,EXISTS_PROD] >> rw[]) 738 739val tysubst_tysubst = store_thm("tysubst_tysubst", 740 ``���s t s'. tysubst s' (tysubst s t) = tysubst ((tysubst s' o_f s) ��� s') t``, 741 ho_match_mp_tac tysubst_ind >> 742 conj_tac >- ( 743 simp[] >> 744 rpt gen_tac >> 745 simp[FLOOKUP_o_f,FLOOKUP_FUNION] >> 746 BasicProvers.CASE_TAC >> simp[] ) >> 747 rw[MAP_MAP_o,MAP_EQ_f]) 748 749val tysubst_nil = store_thm("tysubst_nil[simp]", 750 ``���t. tysubst FEMPTY t = t``, 751 ho_match_mp_tac t_ind >> 752 simp[EVERY_MEM,LIST_EQ_REWRITE,EL_MAP,MEM_EL,PULL_EXISTS]) 753 754val tyvars_tysubst = store_thm("tyvars_tysubst", 755 ``���t. tyvars (tysubst s t) = (tyvars t DIFF FDOM s) ��� BIGUNION { tyvars u | ���x. x ��� tyvars t ��� FLOOKUP s x = SOME u }``, 756 ho_match_mp_tac t_ind >> simp[] >> rw[] >> 757 TRY BasicProvers.CASE_TAC >> 758 TRY (fs[FLOOKUP_DEF] >> NO_TAC) >> rw[] >- ( 759 rw[Once EXTENSION,PULL_EXISTS] ) >> 760 fs[PULL_EXISTS,EVERY_MEM] >> 761 fs[Once EXTENSION,PULL_EXISTS,MEM_MAP] >> 762 metis_tac[]) 763 764val tysubst_frees = store_thm("tysubst_frees", 765 ``���t. (���x. x ��� tyvars t ��� 766 FLOOKUP s1 x = FLOOKUP s2 x) ��� 767 tysubst s1 t = tysubst s2 t``, 768 ho_match_mp_tac t_ind >> simp[] >> 769 rw[LIST_EQ_REWRITE,EL_MAP] >> 770 fs[EVERY_MEM,PULL_EXISTS,MEM_EL] >> 771 metis_tac[]) 772 773val tysubst_frees_gen = store_thm("tysubst_frees_gen", 774 ``���t. (���x. x ��� tyvars t ��� 775 FLOOKUP (s1 ��� FUN_FMAP Tvar {x}) x = FLOOKUP (s2 ��� FUN_FMAP Tvar {x}) x) ��� 776 tysubst s1 t = tysubst s2 t``, 777 ho_match_mp_tac t_ind >> 778 conj_tac >- ( 779 simp[FLOOKUP_FUNION,FLOOKUP_FUN_FMAP] >> 780 gen_tac >> BasicProvers.EVERY_CASE_TAC ) >> 781 rw[LIST_EQ_REWRITE,EL_MAP] >> 782 fs[EVERY_MEM,PULL_EXISTS,MEM_EL] >> 783 metis_tac[]) 784 785(* alpha-equivalence of type schemes *) 786 787val raconv_def = tDefine"raconv"` 788 (raconv f tvs1 tvs2 (Tvar x1) (Tvar x2) ��� 789 if x1 ��� tvs1 then f x1 = x2 790 else x2 = x1 ��� x1 ��� tvs2) ��� 791 (raconv f tvs1 tvs2 (Tapp ts1 tc1) (Tapp ts2 tc2) ��� 792 tc2 = tc1 ��� LIST_REL (raconv f tvs1 tvs2) ts1 ts2) ��� 793 (raconv _ _ _ _ _ = F)` 794(WF_REL_TAC`measure (t_size o SND o SND o SND o SND)` >> 795 rpt gen_tac >> Induct_on`ts2` >> simp[t_size_def] >> 796 rw[] >> res_tac >> simp[]) 797val raconv_def = 798 raconv_def 799 |> SIMP_RULE (std_ss++boolSimps.ETA_ss) [] 800 |> curry save_thm "raconv_def" 801val _ = export_rewrites["raconv_def"] 802val raconv_ind = theorem"raconv_ind" 803 804val tsaconv_def = Define` 805 tsaconv (ftvs1,t1) (ftvs2,t2) ��� 806 let tvs1 = ftvs1 ��� tyvars t1 in 807 let tvs2 = ftvs2 ��� tyvars t2 in 808 ���f. BIJ f tvs1 tvs2 ��� 809 raconv f tvs1 tvs2 t1 t2` 810 811val raconv_refl = store_thm("raconv_refl", 812 ``���tvs t. raconv (��x. x) tvs tvs t t``, 813 gen_tac >> ho_match_mp_tac t_ind >> 814 simp[LIST_REL_EL_EQN,EVERY_MEM,MEM_EL,PULL_EXISTS]) 815 816val tsaconv_refl = store_thm("tsaconv_refl[simp]", 817 ``���ts. tsaconv ts ts``, 818 Cases >> simp[tsaconv_def] >> 819 qspec_tac(`q ��� tyvars r`,`tvs`) >> gen_tac >> 820 qexists_tac`��x. x` >> 821 conj_tac >- simp[BIJ_ID] >> 822 metis_tac[raconv_refl]) 823 824val tsaconv_sym = store_thm("tsaconv_sym", 825 ``���t1 t2. tsaconv t1 t2 ��� tsaconv t2 t1``, 826 Cases >> Cases >> simp[tsaconv_def] >> 827 qspec_tac(`q ��� tyvars r`,`tvs1`) >> gen_tac >> 828 qspec_tac(`q' ��� tyvars r'`,`tvs2`) >> gen_tac >> 829 strip_tac >> 830 qexists_tac`LINV f tvs1` >> 831 conj_tac >- simp[BIJ_LINV_BIJ] >> 832 pop_assum mp_tac >> 833 map_every qid_spec_tac[`r'`,`r`] >> 834 ho_match_mp_tac t_ind >> 835 conj_tac >- ( 836 gen_tac >> Cases >> simp[] >> 837 `INJ f tvs1 tvs2` by fs[BIJ_DEF] >> 838 rw[] >> 839 imp_res_tac LINV_DEF >> 840 imp_res_tac BIJ_LINV_INV >> 841 metis_tac[INJ_DEF]) >> 842 gen_tac >> strip_tac >> 843 gen_tac >> Cases >> simp[] >> 844 fs[EVERY_MEM,LIST_REL_EL_EQN,MEM_EL,PULL_EXISTS]) 845 846val raconv_trans = store_thm("raconv_trans", 847 ``���f1 tvs1 tvs2 t1 t2 t3. 848 BIJ f1 tvs1 tvs2 ��� 849 raconv f1 tvs1 tvs2 t1 t2 ��� 850 BIJ f2 tvs2 tvs3 ��� 851 raconv f2 tvs2 tvs3 t2 t3 ��� 852 raconv (f2 o f1) tvs1 tvs3 t1 t3``, 853 ho_match_mp_tac raconv_ind >> 854 conj_tac >- ( 855 ntac 5 gen_tac >> 856 Cases >> simp[] >> 857 rw[] >> fs[] >> 858 metis_tac[BIJ_DEF,INJ_DEF] ) >> 859 conj_tac >- ( 860 rpt gen_tac >> strip_tac >> 861 Cases >> simp[] >> rw[] >> 862 fs[LIST_REL_EL_EQN,MEM_EL,PULL_EXISTS] >> 863 rw[] >> first_x_assum (match_mp_tac o MP_CANON) >> 864 metis_tac[] ) >> 865 simp[]) 866 867val tsaconv_trans = store_thm("tsaconv_trans", 868 ``���t1 t2 t3. tsaconv t1 t2 ��� tsaconv t2 t3 ��� tsaconv t1 t3``, 869 Cases >> Cases >> Cases >> rw[tsaconv_def] >> fs[LET_THM] >> 870 PROVE_TAC[raconv_trans,BIJ_COMPOSE]) 871 872val raconv_tyvars_eq = prove( 873 ``���f tvs1 tvs2 t1 t2. 874 BIJ f tvs1 tvs2 ��� 875 raconv f tvs1 tvs2 t1 t2 ��� 876 tyvars t1 DIFF tvs1 = 877 tyvars t2 DIFF tvs2``, 878 ho_match_mp_tac raconv_ind >> reverse(rw[]) >- ( 879 fs[Once EXTENSION,PULL_EXISTS] >> 880 fs[LIST_REL_EL_EQN,MEM_EL,PULL_EXISTS] >> 881 metis_tac[] ) >> 882 fs[BIJ_DEF,INJ_DEF] >> metis_tac[] ) 883 884val tsaconv_tyvars_eq = store_thm("tsaconv_tyvars_eq", 885 ``���t1 t2. tsaconv t1 t2 ��� 886 tyvars (SND t1) DIFF (FST t1) = 887 tyvars (SND t2) DIFF (FST t2)``, 888 Cases >> Cases >> simp[tsaconv_def] >> 889 strip_tac >> imp_res_tac raconv_tyvars_eq >> 890 fs[EXTENSION] >> metis_tac[]) 891 892val raconv_imp_tysubst = store_thm("raconv_imp_tysubst", 893 ``���f tvs1 tvs2 t1 t2. 894 BIJ f tvs1 tvs2 ��� 895 FINITE tvs1 ��� 896 raconv f tvs1 tvs2 t1 t2 ��� 897 tysubst (FUN_FMAP (Tvar o f) tvs1) t1 = t2``, 898 ho_match_mp_tac raconv_ind >> 899 rw[] >> 900 simp[FUN_FMAP_DEF,FLOOKUP_FUN_FMAP] >> 901 fs[LIST_REL_EL_EQN,MEM_EL,PULL_EXISTS,LIST_EQ_REWRITE,EL_MAP]) 902 903val tsaconv_imp_tysubst = store_thm("tsaconv_imp_tysubst", 904 ``���t1 t2. tsaconv t1 t2 ��� 905 FINITE (FST t1) ��� 906 ���s. FDOM s = FST t1 ��� tyvars (SND t1) ��� 907 FRANGE s = IMAGE Tvar (FST t2 ��� tyvars (SND t2)) ��� 908 tysubst s (SND t1) = SND t2``, 909 Cases >> Cases >> simp[tsaconv_def] >> rw[] >> 910 qmatch_assum_rename_tac`BIJ f (tvs1 ��� tyvars t1) (tvs2 ��� tyvars t2)` >> 911 imp_res_tac raconv_imp_tysubst >> rfs[] >> 912 qexists_tac`FUN_FMAP (Tvar o f) (tvs1 ��� tyvars t1)` >> rw[] >> 913 fs[BIJ_DEF,IMAGE_COMPOSE,IMAGE_SURJ]) 914 915val tysubst_imp_raconv = store_thm("tysubst_imp_raconv", 916 ``���f tvs1 tvs2 t1 t2. 917 FINITE tvs1 ��� 918 tysubst (FUN_FMAP (Tvar o f) tvs1) t1 = t2 ��� 919 BIJ f tvs1 tvs2 ��� 920 DISJOINT tvs2 (tyvars t1) 921 ��� 922 raconv f tvs1 tvs2 t1 t2``, 923 ho_match_mp_tac raconv_ind >> simp[] >> 924 conj_tac >- ( 925 rw[] >> rfs[FLOOKUP_DEF,FLOOKUP_FUN_FMAP] ) >> 926 rw[] >> fs[] >- ( 927 rw[LIST_REL_EL_EQN,EL_MAP] >> 928 first_x_assum(match_mp_tac o MP_CANON) >> 929 simp[MEM_MAP,PULL_EXISTS] >> 930 qexists_tac`EL n ts1` >> 931 simp[MEM_EL] >> 932 fs[PULL_EXISTS,MEM_EL] >> 933 metis_tac[] ) >> 934 spose_not_then strip_assume_tac >> 935 rfs[FLOOKUP_FUN_FMAP] >> 936 BasicProvers.EVERY_CASE_TAC >> fs[]) 937 938val tysubst_imp_aconv = store_thm("tysubst_imp_aconv", 939 ``���f tvs1 t1 tvs2. 940 FINITE tvs1 ��� 941 BIJ f tvs1 tvs2 ��� 942 DISJOINT tvs2 (tyvars t1) 943 ��� 944 tsaconv (tvs1,t1) (tvs2,tysubst (FUN_FMAP (Tvar o f) tvs1) t1)``, 945 rw[tsaconv_def] >> 946 qexists_tac`f` >> 947 conj_asm1_tac >- ( 948 unabbrev_all_tac >> 949 fs[BIJ_IFF_INV,tyvars_tysubst,PULL_EXISTS,FLOOKUP_FUN_FMAP,IN_DISJOINT] >> 950 qexists_tac`g` >> 951 metis_tac[]) >> 952 match_mp_tac tysubst_imp_raconv >> 953 unabbrev_all_tac >> rw[] >- ( 954 match_mp_tac tysubst_frees >> 955 simp[FLOOKUP_FUN_FMAP] ) >> 956 fs[IN_DISJOINT,tyvars_tysubst,FLOOKUP_FUN_FMAP,PULL_EXISTS] >> 957 metis_tac[]) 958 959val raconv_eq = prove( 960 ``���t1 t2. raconv f ��� ��� t1 t2 ��� t1 = t2``, 961 ho_match_mp_tac t_ind >> 962 conj_tac >- ( 963 gen_tac >> Cases >> simp[] ) >> 964 gen_tac >> strip_tac >> gen_tac >> 965 Cases >> simp[] >> rw[] >> 966 fs[LIST_REL_EL_EQN,EVERY_MEM,MEM_EL,PULL_EXISTS] >> 967 rw[LIST_EQ_REWRITE]) 968 969val tsaconv_eq = store_thm("tsaconv_eq", 970 ``tsaconv ({},t1) ({},t2) ��� t1 = t2``, 971 reverse EQ_TAC >- metis_tac[tsaconv_refl] >> 972 rw[tsaconv_def] >> metis_tac[raconv_eq]) 973 974val tsaconv_empty_imp = prove( 975 ``tsaconv (���,t) ts ��� FST ts ��� tyvars (SND ts) = ���``, 976 Cases_on`ts`>> simp[tsaconv_def] >> rw[]) 977 978(* the typing rules respect alpha-equivalence *) 979 980val ALOOKUP_MAP_FST_EQ_MAP_SND_REL = store_thm("ALOOKUP_MAP_FST_EQ_MAP_SND_REL", 981 ``���l1 l2 x y1. 982 MAP FST l1 = MAP FST l2 ��� 983 LIST_REL R (MAP SND l1) (MAP SND l2) ��� 984 ALOOKUP l1 x = SOME y1 ��� 985 ���y2. ALOOKUP l2 x = SOME y2 ��� R y1 y2``, 986 Induct >> simp[] >> 987 Cases >> Cases >> simp[] >> 988 Cases_on`h`>>rw[] >> rw[]) 989 990val type_e_aconv = store_thm("type_e_aconv", 991 ``���tenv e t. type_e tenv e t ��� 992 EVERY (FINITE o FST o SND) tenv ��� 993 ���tenv'. 994 EVERY (FINITE o FST o SND) tenv' ��� 995 MAP FST tenv = MAP FST tenv' ��� 996 LIST_REL tsaconv (MAP SND tenv) (MAP SND tenv') ��� 997 type_e tenv' e t``, 998 ho_match_mp_tac type_e_ind >> 999 conj_tac >- simp[type_e_clauses] >> 1000 conj_tac >- simp[type_e_clauses] >> 1001 conj_tac >- ( 1002 simp[type_e_clauses] >> rw[] >> 1003 `���z. ALOOKUP tenv' x = SOME z ��� tsaconv (tvs,t) z` by 1004 metis_tac[ALOOKUP_MAP_FST_EQ_MAP_SND_REL] >> 1005 Cases_on`z`>>simp[]>> 1006 first_x_assum(strip_assume_tac o MATCH_MP tsaconv_sym) >> 1007 first_assum(mp_tac o MATCH_MP tsaconv_imp_tysubst) >> simp[] >> 1008 discharge_hyps >- ( 1009 imp_res_tac ALOOKUP_MEM >> 1010 fs[EVERY_MEM,FORALL_PROD] >> 1011 metis_tac[] ) >> 1012 rw[] >> rw[tysubst_tysubst] >> 1013 qexists_tac`tysubst s o_f s'` >> simp[] >> 1014 match_mp_tac tysubst_frees_gen >> 1015 simp[FLOOKUP_FUNION,FLOOKUP_o_f,FLOOKUP_FUN_FMAP] >> 1016 gen_tac >> BasicProvers.CASE_TAC >> 1017 strip_tac >> 1018 BasicProvers.CASE_TAC >> 1019 qmatch_assum_rename_tac`z ��� tyvars t` >> 1020 `z ��� q` by (rfs[FLOOKUP_DEF]>>fs[]) >> 1021 imp_res_tac tsaconv_tyvars_eq >> fs[] >> 1022 pop_assum mp_tac >> 1023 simp[EXTENSION] >> 1024 disch_then(qspec_then`z`mp_tac) >> simp[] >> 1025 `z ��� FDOM s'` by fs[FLOOKUP_DEF] >> simp[] >> 1026 simp[tyvars_tysubst] >> strip_tac >> 1027 fs[SUBSET_DEF,PULL_EXISTS,FLOOKUP_DEF] >> 1028 metis_tac[] ) >> 1029 conj_tac >- ( 1030 simp[type_e_clauses] >> 1031 rw[] >> fs[] >> metis_tac[] ) >> 1032 conj_tac >- ( 1033 simp[type_e_clauses] >> rw[] >> fs[] >> 1034 `tenv_vars tenv = tenv_vars tenv'` by ( 1035 simp[tenv_vars_def,IMAGE_COMPOSE,GSYM LIST_TO_SET_MAP] >> 1036 simp[MAP_MAP_o] >> 1037 AP_TERM_TAC >> AP_TERM_TAC >> 1038 simp[MAP_EQ_f] >> 1039 pop_assum mp_tac >> 1040 simp[LIST_REL_EL_EQN,LIST_EQ_REWRITE,EL_MAP,GSYM AND_IMP_INTRO] >> 1041 rw[] >> res_tac >> 1042 imp_res_tac tsaconv_tyvars_eq >> 1043 simp[UNCURRY] ) >> 1044 qexists_tac`t` >> simp[] >> 1045 first_x_assum match_mp_tac >> 1046 simp[] ) >> 1047 conj_tac >- ( 1048 simp[type_e_clauses] >> rw[] >> fs[] >> 1049 qexists_tac`t` >> simp[] ) >> 1050 conj_tac >- ( simp[type_e_clauses] ) >> 1051 conj_tac >- ( simp[type_e_clauses] ) >> 1052 conj_tac >- ( simp[type_e_clauses] ) >> 1053 conj_tac >- ( simp[type_e_clauses] ) >> 1054 conj_tac >- ( 1055 simp[type_e_clauses] >> 1056 rw[] >> fs[] >> 1057 metis_tac[]) >> 1058 conj_tac >- ( 1059 simp[type_e_clauses] >> rw[] >> fs[] >> 1060 `tenv_vars tenv = tenv_vars tenv'` by ( 1061 simp[tenv_vars_def,IMAGE_COMPOSE,GSYM LIST_TO_SET_MAP] >> 1062 simp[MAP_MAP_o] >> 1063 AP_TERM_TAC >> AP_TERM_TAC >> 1064 simp[MAP_EQ_f] >> 1065 pop_assum mp_tac >> 1066 simp[LIST_REL_EL_EQN,LIST_EQ_REWRITE,EL_MAP,GSYM AND_IMP_INTRO] >> 1067 rw[] >> res_tac >> 1068 imp_res_tac tsaconv_tyvars_eq >> 1069 simp[UNCURRY] ) >> 1070 qexists_tac`t1` >> simp[]) >> 1071 conj_tac >- ( 1072 simp[type_e_clauses] >> 1073 rw[] >> fs[] >> 1074 metis_tac[]) >> 1075 simp[type_e_clauses] >> 1076 rw[] >> fs[] >> 1077 metis_tac[]) 1078 1079val type_v_ts_aconv = store_thm("type_v_ts_aconv", 1080 ``FINITE tvs ��� 1081 type_v_ts rt et v tvs t ��� tsaconv (tvs,t) (tvs',t') ��� 1082 type_v_ts rt et v tvs' t'``, 1083 rw[] >> 1084 imp_res_tac tsaconv_imp_tysubst >> 1085 rfs[] >> rw[] >> 1086 rw[tysubst_tysubst] >> 1087 Q.PAT_ABBREV_TAC`ss = X ��� s` >> 1088 `tysubst ss t = tysubst (DRESTRICT ss (tyvars t)) t` by ( 1089 match_mp_tac tysubst_frees >> simp[FLOOKUP_DRESTRICT] ) >> 1090 pop_assum SUBST1_TAC >> 1091 first_x_assum match_mp_tac >> 1092 simp[FDOM_DRESTRICT,Abbr`ss`] >> 1093 imp_res_tac tsaconv_tyvars_eq >> 1094 fs[EXTENSION] >> 1095 fs[SUBSET_DEF] >> rw[] >> 1096 metis_tac[]) 1097 1098(* a type scheme that is fresh for any finite set of variables exists *) 1099 1100val fresh_def = new_specification("fresh_def",["fresh"], 1101 IN_INFINITE_NOT_FINITE 1102 |> Q.ISPECL[`UNIV:string set`,`s:string set`] 1103 |> REWRITE_RULE[INST_TYPE[alpha|->``:char``]INFINITE_LIST_UNIV,IN_UNIV] 1104 |> SIMP_RULE(srw_ss())[GSYM RIGHT_EXISTS_IMP_THM] 1105 |> Q.GEN`s` 1106 |> SIMP_RULE(srw_ss())[SKOLEM_THM]) 1107 1108val fresh_seq_def = tDefine"fresh_seq"` 1109 fresh_seq avoid n = fresh (avoid ��� (IMAGE (fresh_seq avoid) (count n)))` 1110(WF_REL_TAC`measure (I o SND)` >> simp[]) 1111val fresh_seq_def = 1112 fresh_seq_def 1113 |> SIMP_RULE (std_ss++boolSimps.ETA_ss)[] 1114 |> curry save_thm "fresh_seq_def" 1115 1116val fresh_seq_thm = store_thm("fresh_seq_thm", 1117 ``���avoid n. 1118 FINITE avoid ��� 1119 fresh_seq avoid n ��� avoid ��� 1120 ���k. k < n ��� fresh_seq avoid n ��� fresh_seq avoid k``, 1121 simp[fresh_seq_def] >> 1122 rpt gen_tac >> strip_tac >> 1123 Q.PAT_ABBREV_TAC`s = avoid ��� X` >> 1124 `FINITE s` by simp[Abbr`s`] >> 1125 qspec_then`s`mp_tac fresh_def >> 1126 simp[Abbr`s`] >> rw[] >> 1127 fs[fresh_seq_def] >> 1128 metis_tac[]) 1129 1130val ALL_DISTINCT_fresh_seq = prove( 1131 ``���n avoid. FINITE avoid ��� ALL_DISTINCT (GENLIST (fresh_seq avoid) n)``, 1132 Induct >> simp[GENLIST,ALL_DISTINCT_SNOC,MEM_GENLIST] >> 1133 metis_tac[fresh_seq_thm]) 1134 1135val DISJOINT_fresh_seq = prove( 1136 ``���n avoid. FINITE avoid ��� DISJOINT (set (GENLIST (fresh_seq avoid) n)) avoid``, 1137 Induct >> simp[GENLIST,LIST_TO_SET_SNOC] >> 1138 metis_tac[fresh_seq_thm]) 1139 1140val BIJ_UPDATE_NOTIN = store_thm("BIJ_UPDATE_NOTIN", 1141 ``BIJ f s t ��� x ��� s ��� BIJ ((x =+ y) f) s t``, 1142 rw[BIJ_DEF,INJ_DEF,SURJ_DEF,combinTheory.APPLY_UPDATE_THM] >> rw[] >> 1143 metis_tac[]) 1144 1145val BIJ_fresh_seq = prove( 1146 ``���s. FINITE s ��� ���a. FINITE a ��� 1147 ���f. BIJ f s (set (GENLIST (fresh_seq a) (CARD s)))``, 1148 ho_match_mp_tac FINITE_INDUCT >> 1149 conj_tac >- simp[] >> 1150 gen_tac >> strip_tac >> 1151 gen_tac >> strip_tac >> 1152 gen_tac >> strip_tac >> 1153 first_x_assum(qspec_then`a`(fn th => first_assum(strip_assume_tac o MATCH_MP th))) >> 1154 simp[GENLIST,LIST_TO_SET_SNOC,BIJ_INSERT] >> 1155 qexists_tac`(e =+ fresh_seq a (CARD s)) f` >> 1156 simp[combinTheory.APPLY_UPDATE_THM] >> 1157 qmatch_assum_abbrev_tac`BIJ f s t` >> 1158 simp[DELETE_INSERT] >> 1159 Q.PAT_ABBREV_TAC`n = fresh_seq a Z` >> 1160 `n ��� t` by ( 1161 simp[Abbr`t`,MEM_GENLIST,Abbr`n`] >> 1162 spose_not_then strip_assume_tac >> 1163 qspecl_then[`SUC(CARD s)`,`a`]mp_tac ALL_DISTINCT_fresh_seq >> 1164 simp[ALL_DISTINCT_GENLIST] >> 1165 qexists_tac`CARD s` >> 1166 qexists_tac`m` >> 1167 simp[]) >> 1168 pop_assum(SUBST1_TAC o REWRITE_RULE[DELETE_NON_ELEMENT]) >> 1169 match_mp_tac BIJ_UPDATE_NOTIN >> rw[]) 1170 1171val fresh_ts_exists = prove( 1172 ``���f. ���avoid ts. 1173 FINITE avoid ��� 1174 FINITE (FST ts) ��� 1175 DISJOINT avoid (FST (f avoid ts)) ��� 1176 tsaconv ts (f avoid ts) ��� 1177 FST(f avoid ts) ��� tyvars (SND(f avoid ts))``, 1178 simp[GSYM SKOLEM_THM] >> 1179 rw[RIGHT_EXISTS_IMP_THM] >> 1180 `���f tvs2. BIJ f (FST ts) tvs2 ��� DISJOINT tvs2 (tyvars (SND ts) ��� avoid)` by ( 1181 Q.PAT_ABBREV_TAC`a = X ��� avoid` >> 1182 Q.PAT_ABBREV_TAC`s = FST ts` >> 1183 qabbrev_tac`ls = GENLIST (fresh_seq a) (CARD s)` >> 1184 Q.ISPEC_THEN`s`mp_tac BIJ_fresh_seq >> simp[] >> 1185 disch_then(qspec_then`a`mp_tac) >> 1186 discharge_hyps >- simp[Abbr`a`] >> strip_tac >> 1187 first_assum(match_exists_tac o concl) >> 1188 conj_tac >- simp[] >> 1189 simp[Abbr`ls`,DISJOINT_fresh_seq,Abbr`a`] ) >> 1190 qspecl_then[`f`,`FST ts`,`SND ts`,`tvs2`]mp_tac tysubst_imp_aconv >> 1191 simp[] >> fs[] >> simp[Once DISJOINT_SYM] >> 1192 strip_tac >> 1193 simp[EXISTS_PROD] >> 1194 qmatch_assum_abbrev_tac`tsaconv ts (tvs2,t2)` >> 1195 qexists_tac`tvs2 ��� tyvars t2` >> qexists_tac`t2` >> 1196 fs[IN_DISJOINT] >> 1197 conj_tac >- metis_tac[] >> 1198 Cases_on`ts`>> fs[tsaconv_def,LET_THM] >> 1199 metis_tac[INTER_IDEMPOT,INTER_ASSOC]) 1200val fresh_ts_def = new_specification("fresh_ts_def",["fresh_ts"],fresh_ts_exists) 1201 1202(* capture-avoiding substitution on type schemes and environments *) 1203 1204val tssubst_def = Define` 1205 tssubst s (tvs,t) (tvs2,t2) ��� 1206 ���t'. 1207 tvs2 ��� tyvars t2 ��� 1208 tsaconv (tvs,t) (tvs2,t') ��� 1209 DISJOINT (BIGUNION (IMAGE tyvars (FRANGE (DRESTRICT s (tyvars t' DIFF tvs2))))) tvs2 ��� 1210 t2 = tysubst (DRESTRICT s (tyvars t' DIFF tvs2)) t'` 1211 1212val tssubst_tysubst = store_thm("tssubst_tysubst", 1213 ``tssubst s ({},t) ({},tysubst s t)``, 1214 simp[tssubst_def] >> 1215 qexists_tac`t` >> simp[] >> 1216 match_mp_tac tysubst_frees >> 1217 simp[FLOOKUP_DRESTRICT]) 1218 1219val tssubst_FINITE = store_thm("tssubst_FINITE", 1220 ``FINITE (FST ts) ��� tssubst s ts ts' ��� FINITE (FST ts')``, 1221 Cases_on`ts`>>Cases_on`ts'`>>simp[tssubst_def] >> 1222 metis_tac[FINITE_tyvars,SUBSET_FINITE]) 1223 1224val tysubst_tssubst = store_thm("tysubst_tssubst", 1225 ``FINITE tvs ��� 1226 FDOM s ��� tvs ��� 1227 tssubst s' (tvs,t) (tvs',t') 1228 ��� 1229 ���s''. FDOM s'' ��� tvs' ��� 1230 tysubst s' (tysubst s t) = tysubst s'' t'``, 1231 rw[tssubst_def,PULL_EXISTS] >> 1232 fs[tsaconv_def,LET_THM] >> 1233 imp_res_tac raconv_imp_tysubst >> rfs[] >> res_tac >> 1234 BasicProvers.VAR_EQ_TAC >> pop_assum kall_tac >> 1235 Q.PAT_ABBREV_TAC`tvs1 = tyvars (tysubst X Y)` >> 1236 `tvs1 = IMAGE f (tvs ��� tyvars t) ��� (tyvars t DIFF tvs)` by ( 1237 simp[Abbr`tvs1`,tyvars_tysubst,Once EXTENSION,PULL_EXISTS,FLOOKUP_FUN_FMAP] >> 1238 metis_tac[] ) >> 1239 BasicProvers.VAR_EQ_TAC >> 1240 pop_assum kall_tac >> 1241 qexists_tac`(tysubst s' o_f s ��� s' ��� FUN_FMAP Tvar tvs) f_o_f FUN_FMAP (LINV f (tvs ��� tyvars t)) tvs'` >> 1242 `FINITE tvs'` by metis_tac[SUBSET_FINITE,FINITE_tyvars] >> 1243 conj_tac >- ( simp[f_o_f_DEF,FUN_FMAP_DEF] ) >> 1244 simp[tysubst_tysubst] >> 1245 match_mp_tac tysubst_frees_gen >> 1246 gen_tac >> strip_tac >> 1247 simp[FLOOKUP_FUNION,FLOOKUP_o_f,FLOOKUP_FUN_FMAP,FLOOKUP_f_o_f,FLOOKUP_DRESTRICT] >> 1248 IF_CASES_TAC >> simp[FLOOKUP_FUNION,FLOOKUP_o_f,FLOOKUP_f_o_f,FLOOKUP_FUN_FMAP,FLOOKUP_DRESTRICT] >- ( 1249 `f x ��� tvs'` by fs[BIJ_DEF,INJ_DEF] >> fs[] >> 1250 `LINV f (tvs ��� tyvars t) (f x) = x` by metis_tac[LINV_DEF,BIJ_DEF,IN_INTER] >> 1251 simp[] >> 1252 BasicProvers.CASE_TAC >> simp[] >> 1253 BasicProvers.CASE_TAC >> simp[] ) >> 1254 `FLOOKUP s x = NONE` by ( 1255 fs[FLOOKUP_DEF,SUBSET_DEF,GSYM SUBSET_INTER_ABSORPTION] >> 1256 metis_tac[] ) >> 1257 simp[] >> 1258 `x ��� tvs'` by ( 1259 imp_res_tac raconv_tyvars_eq >> 1260 fs[EXTENSION] >> 1261 metis_tac[] ) >> 1262 simp[] >> 1263 BasicProvers.CASE_TAC >> simp[] >> 1264 CONV_TAC(LAND_CONV(REWR_CONV(GSYM tysubst_nil))) >> 1265 match_mp_tac tysubst_frees_gen >> 1266 simp[FLOOKUP_FUNION,FLOOKUP_FUN_FMAP,FLOOKUP_f_o_f,FLOOKUP_o_f] >> 1267 rw[] >> 1268 fs[IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,PULL_EXISTS,IN_DISJOINT] >> 1269 metis_tac[]) 1270 1271val tssubst_frees = store_thm("tssubst_frees", 1272 ``FINITE (FST ts) ��� 1273 (���x. x ��� tyvars (SND ts) DIFF (FST ts) ��� 1274 FLOOKUP s1 x = FLOOKUP s2 x) ��� 1275 tssubst s1 ts ts' ��� 1276 tssubst s2 ts ts'``, 1277 map_every Cases_on[`ts`,`ts'`] >> 1278 rw[tssubst_def,PULL_EXISTS] >> 1279 first_assum(match_exists_tac o concl) >> 1280 simp[] >> 1281 imp_res_tac tsaconv_tyvars_eq >> fs[EXTENSION] >> 1282 conj_tac >- ( 1283 fs[IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,PULL_EXISTS] >> 1284 metis_tac[] ) >> 1285 match_mp_tac tysubst_frees >> 1286 simp[FLOOKUP_DRESTRICT]) 1287 1288val tssubst_exists = store_thm("tssubst_exists", 1289 ``���s ts. FINITE (FST ts) ��� ���ts'. tssubst s ts ts'``, 1290 rw[EXISTS_PROD] >> 1291 `���tvs t. ts = (tvs,t)` by metis_tac[PAIR] >> 1292 rw[tssubst_def,PULL_EXISTS] >> 1293 qabbrev_tac`a = BIGUNION (IMAGE tyvars (FRANGE s))` >> 1294 qspecl_then[`a`,`tvs,t`]mp_tac fresh_ts_def >> 1295 discharge_hyps >- ( simp[PULL_EXISTS,Abbr`a`] ) >> 1296 strip_tac >> 1297 `���tvs' t'. fresh_ts a (tvs,t) = (tvs',t')` by metis_tac[PAIR] >> fs[] >> 1298 rw[Once CONJ_COMM] >> 1299 first_assum(match_exists_tac o concl) >> 1300 simp[IN_FRANGE_FLOOKUP,tyvars_tysubst,PULL_EXISTS,FLOOKUP_DRESTRICT,FDOM_DRESTRICT] >> 1301 fs[SUBSET_DEF,IN_DISJOINT,Abbr`a`,PULL_EXISTS,IN_FRANGE_FLOOKUP] >> 1302 metis_tac[]) 1303 1304val tenv_subst_def = Define` 1305 tenv_subst s tenv tenv' ��� 1306 MAP FST tenv = MAP FST tenv' ��� 1307 LIST_REL (tssubst s) (MAP SND tenv) (MAP SND tenv')` 1308 1309val tenv_subst_cons = store_thm("tenv_subst_cons", 1310 ``tenv_subst s tenv tenv' ��� 1311 tssubst s ts ts' 1312 ��� tenv_subst s ((x,ts)::tenv) ((x,ts')::tenv')``, 1313 rw[tenv_subst_def]) 1314 1315val tenv_subst_exists = store_thm("tenv_subst_exists", 1316 ``EVERY (FINITE o FST o SND) tenv ��� 1317 ���tenv'. tenv_subst s tenv tenv'``, 1318 rw[tenv_subst_def] >> 1319 simp[exists_list_GENLIST] >> 1320 qexists_tac`LENGTH tenv` >> 1321 qexists_tac`��n. FST(EL n tenv), @ts'. tssubst s (SND (EL n tenv)) ts'` >> 1322 simp[LIST_EQ_REWRITE,EL_MAP,EVERY2_MAP] >> 1323 simp[LIST_REL_EL_EQN] >> rw[] >> 1324 SELECT_ELIM_TAC >> simp[] >> 1325 fs[EVERY_MEM,MEM_EL,PULL_EXISTS] >> 1326 metis_tac[tssubst_exists]) 1327 1328val tyvars_tssubst_eq = store_thm("tyvars_tssubst_eq", 1329 ``tssubst s ts (bvs,b) ��� FINITE (FST ts) ��� 1330 tyvars b DIFF bvs = 1331 (tyvars (SND ts) DIFF (FST ts ��� FDOM s)) ��� 1332 BIGUNION (IMAGE tyvars (FRANGE (DRESTRICT s (tyvars (SND ts) DIFF (FST ts)))))``, 1333 `���tvs t. ts = (tvs,t)` by metis_tac[PAIR] >> 1334 simp[tssubst_def,PULL_EXISTS] >> rw[] >> 1335 simp[Once EXTENSION,PULL_EXISTS,tyvars_tysubst,FLOOKUP_DRESTRICT,FDOM_DRESTRICT,IN_FRANGE_FLOOKUP] >> 1336 imp_res_tac tsaconv_tyvars_eq >> fs[] >> 1337 fs[tyvars_tysubst,SUBSET_DEF,PULL_EXISTS,FDOM_DRESTRICT,FLOOKUP_DRESTRICT,EXTENSION,IN_FRANGE_FLOOKUP,IN_DISJOINT] >> 1338 metis_tac[] ) 1339 1340val tenv_vars_tenv_subst_eq = store_thm("tenv_vars_tenv_subst_eq", 1341 ``EVERY (FINITE o FST o SND) tenv ��� 1342 tenv_subst s tenv tenv' ��� 1343 tenv_vars tenv' = 1344 (tenv_vars tenv DIFF FDOM s) ��� 1345 BIGUNION (IMAGE tyvars (FRANGE (DRESTRICT s (tenv_vars tenv))))``, 1346 qid_spec_tac`tenv'` >> 1347 Induct_on`tenv` >- simp[tenv_subst_def,tenv_vars_def,DRESTRICT_IS_FEMPTY] >> 1348 simp[FORALL_PROD] >> 1349 qx_genl_tac[`x`,`tvs`,`t`] >> 1350 fs[tenv_subst_def] >> 1351 Cases>>simp[]>> 1352 PairCases_on`h`>>simp[] >> rw[] >> fs[] >> 1353 first_x_assum(qspec_then`t'`mp_tac) >> 1354 rw[tenv_vars_cons] >> 1355 imp_res_tac tyvars_tssubst_eq >> 1356 simp[] >> 1357 pop_assum kall_tac >> 1358 fs[Once EXTENSION,PULL_EXISTS] >> 1359 fs[IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,PULL_EXISTS] >> 1360 `���k v. FLOOKUP s k = SOME v ��� k ��� FDOM s` by simp[FLOOKUP_DEF] >> 1361 metis_tac[]) 1362 1363val tssubst_id = store_thm("tssubst_id", 1364 ``FST ts ��� tyvars (SND ts) ��� 1365 DISJOINT (FDOM s) (tyvars (SND ts) DIFF (FST ts)) 1366 ��� tssubst s ts ts``, 1367 Cases_on`ts`>>simp[tssubst_def] >> rw[] >> 1368 qexists_tac`r` >> rw[] >- ( 1369 fs[IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,IN_DISJOINT] >> 1370 fs[FLOOKUP_DEF] >> metis_tac[] ) >> 1371 `DRESTRICT s (tyvars r DIFF q) = FEMPTY` by ( 1372 simp[FLOOKUP_EXT,FUN_EQ_THM,FLOOKUP_DRESTRICT] >> 1373 fs[IN_DISJOINT,FLOOKUP_DEF] >> 1374 metis_tac[] ) >> 1375 rw[]) 1376 1377val tenv_subst_id = store_thm("tenv_subst_id", 1378 ``EVERY (��(tvs,t). tvs ��� tyvars t) (MAP SND tenv) ��� 1379 DISJOINT (FDOM s) (tenv_vars tenv) 1380 ��� 1381 tenv_subst s tenv tenv``, 1382 Induct_on`tenv`>-simp[tenv_subst_def] >> 1383 Cases >> rw[] >> fs[] >> 1384 match_mp_tac tenv_subst_cons >> 1385 Cases_on`r` >> fs[tenv_vars_cons] >> 1386 conj_tac >- ( 1387 first_x_assum match_mp_tac >> 1388 fs[IN_DISJOINT,SUBSET_DEF] >> 1389 metis_tac[] ) >> 1390 match_mp_tac tssubst_id >> 1391 fs[IN_DISJOINT] >> 1392 metis_tac[]) 1393 1394(* lemmas about type environment and its relationship to value environment *) 1395 1396val type_env_EVERY_SUBSET = prove( 1397 ``type_env rt et env tenv ��� 1398 EVERY (��(tvs,t). tvs ��� tyvars t) (MAP SND tenv)``, 1399 qid_spec_tac`tenv`>> 1400 Induct_on`env`>> simp[type_env_clauses] >> 1401 simp[PULL_EXISTS] >> rw[]) 1402 1403val type_env_EVERY_FINITE = prove( 1404 ``type_env rt et env tenv ��� 1405 EVERY (FINITE o FST o SND) tenv``, 1406 rw[] >> 1407 imp_res_tac type_env_EVERY_SUBSET >> 1408 fs[EVERY_MEM,MEM_MAP,PULL_EXISTS,FORALL_PROD] >> 1409 metis_tac[FINITE_tyvars,SUBSET_FINITE]) 1410 1411val type_env_ALOOKUP_tenv_SOME = prove( 1412 ``���env tenv. type_env rt et env tenv ��� 1413 ���x tvs t. 1414 ALOOKUP tenv x = SOME (tvs,t) ��� 1415 ���v. ALOOKUP env x = SOME v ��� 1416 ���s. FDOM s ��� tvs ��� 1417 type_v rt et v (tysubst s t)``, 1418 Induct >> simp[type_env_clauses] >> 1419 Cases >> simp[] >> 1420 Cases >> simp[] >> 1421 PairCases_on`h`>>simp[] >> 1422 rw[] >> rw[] >> fs[] >> 1423 metis_tac[]) 1424 1425val type_env_ALOOKUP_env_SOME = prove( 1426 ``���env tenv. type_env rt et env tenv ��� 1427 ���x v. 1428 ALOOKUP env x = SOME v ��� 1429 ���tvs t. ALOOKUP tenv x = SOME (tvs,t) ��� 1430 ���s. FDOM s ��� tvs ��� 1431 type_v rt et v (tysubst s t)``, 1432 Induct >> simp[type_env_clauses] >> 1433 Cases >> simp[] >> 1434 Cases >> simp[] >> 1435 PairCases_on`h`>>simp[] >> 1436 rw[] >> rw[] >> fs[] >> 1437 metis_tac[]) 1438 1439(* substitution lemma: typing rules respect substitution *) 1440 1441val tysubst_Tfn = SIMP_CONV(srw_ss())[]``tysubst s (Tfn t1 t2)`` 1442val tysubst_Texn = SIMP_CONV(srw_ss())[]``tysubst s (Texn t1)`` 1443 1444val type_e_subst = store_thm("type_e_subst", 1445 ``���tenv e t. type_e tenv e t ��� EVERY (FINITE o FST o SND) tenv 1446 ��� ���s tenv'. tenv_subst s tenv tenv' ��� type_e tenv' e (tysubst s t)``, 1447 ho_match_mp_tac type_e_ind >> 1448 rpt conj_tac >> 1449 (* most cases *) 1450 TRY ( 1451 simp[type_e_clauses] >> rw[] >> fs[] >> 1452 PROVE_TAC[tenv_subst_cons,tssubst_tysubst,tysubst_Tfn,tysubst_Texn]) >> 1453 (* var *) 1454 TRY ( 1455 simp[type_e_clauses] >> rw[] >> 1456 fs[tenv_subst_def] >> 1457 imp_res_tac ALOOKUP_MAP_FST_EQ_MAP_SND_REL >> 1458 fs[] >> rw[] >> fs[] >> rw[] >> 1459 `���tvs' t'. y2 = (tvs',t')` by metis_tac[PAIR] >> 1460 simp[] >> 1461 `FINITE tvs` by ( 1462 imp_res_tac ALOOKUP_MEM >> 1463 fs[EVERY_MEM,FORALL_PROD] >> 1464 metis_tac[] ) >> 1465 metis_tac[tysubst_tssubst] ) >> 1466 (* let value *) 1467 TRY ( 1468 qx_genl_tac[`e1`,`e2`,`t1`,`t2`] >> 1469 simp[type_e_clauses] >> rw[] >> fs[] >> 1470 qabbrev_tac`s1 = DRESTRICT s (tenv_vars tenv)` >> 1471 qabbrev_tac`a = BIGUNION (IMAGE tyvars (FRANGE s1)) ��� tenv_vars tenv` >> 1472 qspecl_then[`a`,`tyvars t1 DIFF tenv_vars tenv,t1`]mp_tac fresh_ts_def >> 1473 discharge_hyps >- ( 1474 simp[Abbr`a`,PULL_EXISTS] ) >> 1475 Q.PAT_ABBREV_TAC`tvs = tyvars t1 DIFF _` >> 1476 `���tvs' t'. fresh_ts a (tvs,t1) = (tvs',t')` by metis_tac[PAIR] >> 1477 simp[] >> strip_tac >> 1478 `FINITE tvs` by simp[Abbr`tvs`] >> 1479 imp_res_tac tsaconv_imp_tysubst >> rfs[] >> 1480 qmatch_assum_rename_tac`FDOM r = _` >> 1481 qexists_tac`tysubst (s1 ��� r) t1` >> 1482 conj_tac >- ( 1483 first_x_assum match_mp_tac >> 1484 fs[tenv_subst_def] >> 1485 match_mp_tac EVERY2_MEM_MONO >> 1486 qexists_tac`tssubst s` >> 1487 imp_res_tac LIST_REL_LENGTH >> fs[] >> 1488 simp[ZIP_MAP,MEM_MAP,PULL_EXISTS,FORALL_PROD] >> 1489 rw[] >> 1490 match_mp_tac (GEN_ALL tssubst_frees) >> simp[] >> 1491 simp[RIGHT_EXISTS_AND_THM] >> 1492 conj_tac >- ( 1493 rfs[MEM_ZIP,EVERY_MEM,MEM_EL,PULL_EXISTS] >> 1494 metis_tac[FST,SND] ) >> 1495 simp[Once CONJ_COMM] >> 1496 first_assum(match_exists_tac o concl) >> simp[] >> 1497 simp[FLOOKUP_FUNION] >> rw[] >> 1498 simp[Abbr`s1`,FLOOKUP_DRESTRICT] >> 1499 IF_CASES_TAC >> simp[] >- ( 1500 BasicProvers.CASE_TAC >> 1501 simp[FLOOKUP_DEF,Abbr`tvs`] ) >> 1502 imp_res_tac MEM_ZIP_MEM_MAP >> rfs[] >> 1503 fs[tenv_vars_def,FORALL_PROD,PULL_EXISTS] >> 1504 metis_tac[]) >> 1505 `tvs' ��� tyvars (tysubst (s1 ��� r) t1)` by ( 1506 BasicProvers.VAR_EQ_TAC >> 1507 fs[tyvars_tysubst,SUBSET_DEF,PULL_EXISTS,Abbr`s1`,FDOM_DRESTRICT,FLOOKUP_DRESTRICT,FLOOKUP_FUNION] >> 1508 qx_gen_tac`z` >> strip_tac >> 1509 fs[IN_DISJOINT,Abbr`a`,PULL_EXISTS,IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,Abbr`tvs`] >> 1510 first_x_assum(qspec_then`z`mp_tac) >> simp[] >> 1511 imp_res_tac tsaconv_tyvars_eq >> 1512 fs[EXTENSION,PULL_EXISTS,tyvars_tysubst] >> 1513 strip_tac >- metis_tac[] >> 1514 disj2_tac >> 1515 first_assum(match_exists_tac o concl) >> simp[] >> 1516 first_assum(match_exists_tac o concl) >> simp[] >> 1517 IF_CASES_TAC >> simp[] >> 1518 fs[FLOOKUP_DEF] >> 1519 metis_tac[] ) >> 1520 `tssubst s (tvs,t1) (tvs',tysubst (s1 ��� r) t1)` by ( 1521 simp[tssubst_def,PULL_EXISTS] >> 1522 qexists_tac`t'` >> simp[] >> 1523 conj_tac >- ( 1524 BasicProvers.VAR_EQ_TAC >> 1525 imp_res_tac tsaconv_tyvars_eq >> 1526 simp[IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,PULL_EXISTS] >> 1527 fs[IN_DISJOINT,Abbr`a`,PULL_EXISTS,Abbr`s1`,IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT] >> rw[] >> 1528 first_x_assum match_mp_tac >> 1529 qexists_tac`k` >> simp[] >> 1530 fs[EXTENSION,Abbr`tvs`] >> 1531 metis_tac[] ) >> 1532 BasicProvers.VAR_EQ_TAC >> 1533 simp[tysubst_tysubst] >> 1534 match_mp_tac tysubst_frees >> 1535 simp[FLOOKUP_FUNION,FLOOKUP_DRESTRICT,FLOOKUP_o_f] >> 1536 qx_gen_tac`z` >> strip_tac >> 1537 simp[Abbr`s1`,FLOOKUP_DRESTRICT] >> 1538 IF_CASES_TAC >- ( 1539 `FLOOKUP r z = NONE` by ( 1540 simp[FLOOKUP_DEF,Abbr`tvs`] ) >> 1541 simp[] >> 1542 BasicProvers.CASE_TAC >> simp[] >> 1543 simp[tyvars_tysubst,PULL_EXISTS,Abbr`tvs`] >> 1544 fs[Abbr`a`,IN_DISJOINT,PULL_EXISTS,IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT] >> 1545 metis_tac[] ) >> 1546 simp[] >> 1547 BasicProvers.CASE_TAC >- ( 1548 IF_CASES_TAC >> simp[] >> 1549 imp_res_tac tsaconv_tyvars_eq >> 1550 fs[Abbr`tvs`] >> 1551 fs[EXTENSION] >> 1552 metis_tac[] ) >> 1553 CONV_TAC(LAND_CONV(REWR_CONV(GSYM tysubst_nil))) >> 1554 match_mp_tac tysubst_frees >> 1555 simp[FLOOKUP_DRESTRICT] >> 1556 imp_res_tac tsaconv_tyvars_eq >> 1557 fs[Abbr`tvs`] >> 1558 qmatch_assum_rename_tac`FLOOKUP r z = SOME u` >> 1559 `u ��� FRANGE r` by (simp[IN_FRANGE_FLOOKUP]>>metis_tac[])>> 1560 rfs[] ) >> 1561 first_x_assum match_mp_tac >> 1562 match_mp_tac tenv_subst_cons >> 1563 simp[] >> 1564 BasicProvers.VAR_EQ_TAC >> 1565 `tyvars (tysubst (s1 ��� r) t1) DIFF tenv_vars tenv' = tvs'` suffices_by simp[] >> 1566 simp[SET_EQ_SUBSET] >> 1567 conj_tac >- ( 1568 imp_res_tac tsaconv_tyvars_eq >> 1569 pop_assum mp_tac >> 1570 qpat_assum`DISJOINT a tvs'`mp_tac >> 1571 simp[tyvars_tysubst,SUBSET_DEF,PULL_EXISTS,FLOOKUP_FUNION,Abbr`s1`,FLOOKUP_DRESTRICT,FDOM_DRESTRICT] >> 1572 simp[Abbr`a`,IN_DISJOINT,EXTENSION,IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,PULL_EXISTS,Abbr`tvs`] >> 1573 rw[] >> 1574 pop_assum mp_tac >> 1575 imp_res_tac tenv_vars_tenv_subst_eq >> 1576 simp[PULL_EXISTS] >> 1577 simp[IN_FRANGE_FLOOKUP,FLOOKUP_DRESTRICT,PULL_EXISTS] >> 1578 pop_assum kall_tac >> 1579 pop_assum mp_tac >> 1580 IF_CASES_TAC >> simp[] >- ( 1581 qmatch_assum_rename_tac`y ��� tenv_vars tenv` >> 1582 `FLOOKUP r y = NONE` by ( 1583 simp[FLOOKUP_DEF] ) >> 1584 BasicProvers.CASE_TAC >> simp[] >> 1585 strip_tac >> BasicProvers.VAR_EQ_TAC >> 1586 metis_tac[] ) >> 1587 qmatch_assum_rename_tac`y ��� tenv_vars tenv` >> 1588 strip_tac >> 1589 `u ��� FRANGE r` by ( 1590 simp[IN_FRANGE_FLOOKUP] >> 1591 metis_tac[] ) >> 1592 pop_assum mp_tac >> simp[PULL_EXISTS] >> 1593 gen_tac >> strip_tac >> fs[] ) >> 1594 fs[SUBSET_DEF] >> 1595 imp_res_tac tenv_vars_tenv_subst_eq >> 1596 spose_not_then strip_assume_tac >> 1597 pop_assum mp_tac >> simp[] >> 1598 fs[IN_DISJOINT,Abbr`a`,PULL_EXISTS,IN_FRANGE_FLOOKUP,Abbr`s1`,FLOOKUP_DRESTRICT] >> 1599 metis_tac[] )) 1600 1601(* 1602We prove type soundness by induction on the semantics. This works because both 1603the typing relation and the semantics are syntax-directed. We establish that 1604well-typed expressions do not fail, if they terminate with a value then the 1605value has the same type as the original expression, and if they terminate with 1606an exception, the exception's parameter matches the type of the exception. 1607*) 1608 1609val type_soundness = Q.store_thm("type_soundness", 1610 `���env s e tenv rt et t r s'. type_e tenv e t ��� 1611 LIST_REL (type_v rt et) s.refs rt ��� 1612 type_env rt et env tenv ��� 1613 LENGTH et = s.next_exn ��� 1614 sem env s e = (r,s') ��� 1615 ���rt' et'. 1616 LIST_REL (type_v (rt++rt') (et++et')) s'.refs (rt++rt') ��� 1617 type_env (rt++rt') (et++et') env tenv ��� 1618 LENGTH (et++et') = s'.next_exn ��� 1619 case r of 1620 | Rfail => F 1621 | Rval v => type_v (rt++rt') (et++et') v t 1622 | Rraise n v => 1623 n < LENGTH (et++et') ��� 1624 type_v (rt++rt') (et++et') v (EL n (et++et')) 1625 | _ => T`, 1626 ho_match_mp_tac sem_ind >> 1627 (* Lit *) 1628 conj_tac >- ( simp[sem_def,type_v_clauses,type_e_clauses,LENGTH_NIL] >> metis_tac[APPEND_NIL]) >> 1629 (* Var *) 1630 conj_tac >- ( 1631 rw[sem_def,type_e_clauses] >> 1632 every_case_tac >> fs[] >> rw[] >> 1633 imp_res_tac type_env_ALOOKUP_tenv_SOME >> 1634 imp_res_tac type_env_ALOOKUP_env_SOME >> fs[LENGTH_NIL] >> 1635 metis_tac[APPEND_NIL] ) >> 1636 (* App *) 1637 conj_tac >- ( 1638 rw[type_e_clauses,sem_def] >> pop_assum mp_tac >> 1639 ntac 6 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >> 1640 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1641 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1642 simp[type_v_clauses] >> strip_tac >> 1643 last_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1644 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1645 simp[] >> strip_tac >> 1646 TRY ( 1647 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1648 first_assum(match_exists_tac o concl) >> simp[] >> 1649 NO_TAC) >> 1650 last_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1651 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1652 simp[AND_IMP_INTRO] >> 1653 (discharge_hyps >- ( 1654 simp[type_env_clauses,FDOM_EQ_EMPTY,type_v_clauses] >> 1655 metis_tac[type_v_extend])) >> 1656 strip_tac >> 1657 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1658 first_assum(match_exists_tac o concl) >> simp[] >> 1659 BasicProvers.CASE_TAC >> fs[] >> simp[] >> 1660 metis_tac[type_v_extend] ) >> 1661 (* Let *) 1662 conj_tac >- ( 1663 rw[type_e_clauses,sem_def] >> pop_assum mp_tac >> 1664 ntac 2 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >> 1665 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1666 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1667 simp[] >> strip_tac >> 1668 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1669 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1670 simp[type_env_clauses,FDOM_EQ_EMPTY] >> 1671 TRY(discharge_hyps >- ( 1672 rw[] >> 1673 qmatch_assum_rename_tac`FDOM ss ��� _` >> 1674 `tenv_subst ss tenv tenv` by ( 1675 match_mp_tac tenv_subst_id >> 1676 conj_tac >- metis_tac[type_env_EVERY_SUBSET] >> 1677 fs[SUBSET_DEF,IN_DISJOINT] >> 1678 metis_tac[] ) >> 1679 `type_e tenv e (tysubst ss t1)` by ( 1680 match_mp_tac (MP_CANON type_e_subst) >> 1681 metis_tac[type_env_EVERY_FINITE] ) >> 1682 Cases_on`e`>>fs[sem_def]>>BasicProvers.EVERY_CASE_TAC>>fs[]>> 1683 rw[]>>fs[type_v_clauses,LENGTH_NIL]>>rw[]>>fs[]>> 1684 fs[type_e_clauses] >- ( 1685 imp_res_tac type_env_ALOOKUP_tenv_SOME >> 1686 fs[] >> rw[] ) >> 1687 metis_tac[])) >> 1688 strip_tac >> 1689 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1690 first_assum(match_exists_tac o concl) >> simp[] >> 1691 BasicProvers.CASE_TAC >> fs[] >> simp[]) >> 1692 (* Fun *) 1693 conj_tac >- ( 1694 simp[type_e_clauses,sem_def,type_v_clauses] >> 1695 rw[LENGTH_NIL] >> metis_tac[APPEND_NIL] ) >> 1696 (* Funrec *) 1697 conj_tac >- ( 1698 simp[type_e_clauses,sem_def,type_v_clauses] >> 1699 rw[LENGTH_NIL] >> metis_tac[APPEND_NIL]) >> 1700 (* Ref *) 1701 conj_tac >- ( 1702 rw[type_e_clauses,sem_def] >> pop_assum mp_tac >> 1703 ntac 2 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >> 1704 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1705 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1706 simp[] >> strip_tac >> 1707 qexists_tac`rt'++[t']` >> 1708 qexists_tac`et'` >> 1709 conj_tac >- ( 1710 ONCE_REWRITE_TAC[APPEND_ASSOC] >> 1711 match_mp_tac rich_listTheory.EVERY2_APPEND_suff >> 1712 simp[] >> 1713 reverse conj_tac >- metis_tac[type_v_extend,APPEND_NIL] >> 1714 match_mp_tac(MP_CANON(GEN_ALL LIST_REL_mono)) >> 1715 metis_tac[type_v_extend,APPEND_NIL] ) >> 1716 imp_res_tac LIST_REL_LENGTH >> 1717 simp[rich_listTheory.EL_APPEND2,type_v_clauses] >> 1718 metis_tac[type_v_extend,APPEND_NIL]) >> 1719 (* Deref *) 1720 conj_tac >- ( 1721 rw[type_e_clauses,sem_def] >> pop_assum mp_tac >> 1722 ntac 3 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >> 1723 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1724 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1725 simp[type_v_clauses] >> strip_tac >> 1726 TRY ( 1727 first_assum(match_exists_tac o concl) >> simp[] >> 1728 fs[LIST_REL_EL_EQN] >> NO_TAC) >> 1729 spose_not_then strip_assume_tac >> 1730 fs[LIST_REL_EL_EQN] ) >> 1731 (* Assign *) 1732 conj_tac >- ( 1733 rw[type_e_clauses,sem_def] >> pop_assum mp_tac >> 1734 ntac 5 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >> 1735 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1736 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1737 simp[type_v_clauses] >> strip_tac >> 1738 TRY ( qmatch_rename_tac`$! _` >> spose_not_then strip_assume_tac ) >> 1739 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1740 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1741 simp[type_v_clauses] >> strip_tac >> 1742 TRY ( 1743 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1744 first_assum(match_exists_tac o concl) >> simp[] >> 1745 fs[LIST_REL_EL_EQN] >> NO_TAC) >> 1746 TRY ( qmatch_rename_tac`$! _` >> 1747 spose_not_then strip_assume_tac >> 1748 fsrw_tac[ARITH_ss][LIST_REL_EL_EQN] >> NO_TAC) >> 1749 Cases_on`n < LENGTH rt` >- ( 1750 qexists_tac`rt' ++ rt''` >> 1751 qexists_tac`et' ++ et''` >> simp[] >> 1752 fs[LIST_REL_EL_EQN,EL_LUPDATE] >> rw[] >> 1753 fs[rich_listTheory.EL_APPEND1] ) >> 1754 qexists_tac`LUPDATE t' (n-LENGTH rt) (rt' ++ rt'')` >> 1755 qexists_tac`et'++et''` >> simp[] >> 1756 reverse conj_tac >- metis_tac[type_v_extend,APPEND_ASSOC] >> 1757 simp[GSYM rich_listTheory.LUPDATE_APPEND2] >> 1758 match_mp_tac EVERY2_LUPDATE_same >> 1759 simp[rich_listTheory.EL_APPEND1,rich_listTheory.EL_APPEND2] >> 1760 simp[rich_listTheory.LUPDATE_APPEND1,rich_listTheory.LUPDATE_APPEND2] >> 1761 simp[LUPDATE_ID] >> rw[] >> 1762 qpat_assum`type_v A X Y Z`mp_tac >> 1763 fs[arithmeticTheory.NOT_LESS] >> 1764 fs[rich_listTheory.EL_APPEND2] 1765 ) >> 1766 (* Letexn *) 1767 conj_tac >- ( 1768 rw[type_e_clauses,sem_def] >> 1769 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1770 disch_then(qspecl_then[`rt`,`et++[t1]`]mp_tac) >> 1771 simp[] >> 1772 discharge_hyps >- ( 1773 match_mp_tac(MP_CANON(GEN_ALL LIST_REL_mono)) >> 1774 metis_tac[type_v_extend,APPEND_NIL] ) >> 1775 discharge_hyps >- ( 1776 simp[type_env_clauses,FDOM_EQ_EMPTY,type_v_clauses,rich_listTheory.EL_APPEND2] >> 1777 metis_tac[type_v_extend,APPEND_NIL] ) >> 1778 strip_tac >> 1779 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1780 first_assum(match_exists_tac o concl) >> simp[] >> 1781 fs[type_env_clauses] >> 1782 BasicProvers.CASE_TAC >> fs[] >> simp[]) >> 1783 (* Raise *) 1784 conj_tac >- ( 1785 rw[type_e_clauses,sem_def] >> pop_assum mp_tac >> 1786 ntac 5 (BasicProvers.CASE_TAC >> fs[]) >> rw[] >> 1787 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1788 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1789 simp[type_v_clauses] >> strip_tac >> 1790 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1791 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1792 simp[] >> strip_tac >> 1793 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1794 first_assum(match_exists_tac o concl) >> simp[] >> 1795 rev_full_simp_tac(srw_ss()++ARITH_ss)[rich_listTheory.EL_APPEND1] ) >> 1796 (* Handle *) 1797 rw[type_e_clauses,sem_def] >> pop_assum mp_tac >> 1798 ntac 8 (BasicProvers.CASE_TAC >> fs[]) >> TRY(BasicProvers.CASE_TAC >> fs[]) >> rw[] >> 1799 qpat_assum`type_e tenv e' _`(fn th => first_x_assum(mp_tac o C MATCH_MP th)) >> 1800 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1801 simp[type_v_clauses] >> strip_tac >> 1802 TRY ( qmatch_rename_tac`$! _` >> spose_not_then strip_assume_tac ) >> 1803 qpat_assum`type_e tenv e'' _`(fn th => first_x_assum(mp_tac o C MATCH_MP th)) >> 1804 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1805 simp[type_v_clauses] >> strip_tac >> 1806 TRY ( qmatch_rename_tac`$! _` >> spose_not_then strip_assume_tac ) >> 1807 TRY ( 1808 qpat_assum`type_e tenv e _`(fn th => first_x_assum(mp_tac o C MATCH_MP th)) >> 1809 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1810 simp[type_v_clauses] >> strip_tac >> fs[]) >> 1811 TRY ( 1812 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1813 first_assum(match_exists_tac o concl) >> simp[] >> 1814 NO_TAC) >> 1815 TRY ( Cases_on`v`>>fs[type_v_clauses]>>NO_TAC) >> 1816 TRY ( Cases_on`v'`>>fs[type_v_clauses]>>NO_TAC) >> 1817 first_x_assum(fn th => last_assum(mp_tac o MATCH_MP th)) >> 1818 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1819 simp[] >> 1820 (discharge_hyps >- ( 1821 fs[type_env_clauses,FDOM_EQ_EMPTY] >> 1822 rev_full_simp_tac(srw_ss()++ARITH_ss)[rich_listTheory.EL_APPEND1] >> 1823 simp[type_v_clauses] >> 1824 metis_tac[type_v_extend] )) >> 1825 strip_tac >> 1826 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 1827 first_assum(match_exists_tac o concl) >> simp[] >> 1828 BasicProvers.CASE_TAC >> fs[] >> simp[] >> 1829 metis_tac[type_v_extend]); 1830 1831(* 1832"Type soundness" on the un-clocked relational semantics, for comparison. 1833*) 1834 1835val eval_strongind = theorem"eval_strongind"; 1836 1837val eval_type_soundness = Q.store_thm("eval_type_soundness", 1838 `���env s e res. eval env s e res ��� 1839 ���tenv t rt et r s'. 1840 type_e tenv e t ��� 1841 LIST_REL (type_v rt et) s.refs rt ��� 1842 type_env rt et env tenv ��� 1843 LENGTH et = s.next_exn ��� 1844 res = (r,s') 1845 ��� 1846 ���rt' et'. 1847 LIST_REL (type_v (rt++rt') (et++et')) s'.refs (rt++rt') ��� 1848 type_env (rt++rt') (et++et') env tenv ��� 1849 LENGTH (et++et') = s'.next_exn ��� 1850 case r of 1851 | Rval v => type_v (rt ++ rt') (et++et') v t 1852 | Rraise n v' => 1853 n < LENGTH (et++et') ��� 1854 type_v (rt++rt') (et++et') v' (EL n (et++et')) 1855 | _ => F`, 1856 ho_match_mp_tac eval_strongind >> 1857 (* Lit *) 1858 conj_tac >- ( simp[sem_def,type_v_clauses,type_e_clauses,LENGTH_NIL] >> metis_tac[APPEND_NIL]) >> 1859 (* Var *) 1860 conj_tac >- ( 1861 rw[] >> 1862 simp[type_e_clauses] >> 1863 spose_not_then strip_assume_tac >> 1864 imp_res_tac type_env_ALOOKUP_tenv_SOME >> fs[] ) >> 1865 conj_tac >- ( 1866 simp[type_e_clauses] >> 1867 rw[] >> 1868 imp_res_tac type_env_ALOOKUP_tenv_SOME >> fs[] >> 1869 simp[LENGTH_NIL] >> 1870 qexists_tac`[]`>>rw[]) >> 1871 (* App *) 1872 conj_tac >- ( 1873 rw[Once type_e_clauses] >> 1874 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1875 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1876 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1877 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1878 Cases_on`v1`>>fs[type_v_clauses]>>rw[]>> 1879 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1880 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> simp[] >> 1881 (discharge_hyps >- ( 1882 simp[type_env_clauses,type_v_clauses,FDOM_EQ_EMPTY] >> 1883 metis_tac[type_v_extend] )) >> rw[] >> 1884 BasicProvers.CASE_TAC >> fs[] >> 1885 qexists_tac`rt'++rt''++rt'''` >> 1886 qexists_tac`et'++et''++et'''` >> 1887 simp[] >> 1888 metis_tac[type_v_extend]) >> 1889 conj_tac >- ( 1890 rw[Once type_e_clauses] >> 1891 spose_not_then strip_assume_tac >> 1892 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1893 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1894 spose_not_then strip_assume_tac >> 1895 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1896 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1897 Cases_on`v1`>>fs[type_v_clauses]) >> 1898 conj_tac >- ( 1899 rw[Once type_e_clauses] >> 1900 spose_not_then strip_assume_tac >> 1901 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1902 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1903 spose_not_then strip_assume_tac >> 1904 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1905 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1906 spose_not_then strip_assume_tac >> 1907 first_x_assum(qspecl_then[`rt'++rt''`,`et'++et''`]mp_tac) >> 1908 simp[] >> BasicProvers.CASE_TAC >> fs[] >> simp[] ) >> 1909 conj_tac >- ( 1910 rw[Once type_e_clauses] >> 1911 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1912 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1913 first_assum(match_exists_tac o concl) >> simp[] >> 1914 BasicProvers.CASE_TAC >> fs[] >> simp[] ) >> 1915 (* Let *) 1916 conj_tac >- ( 1917 rw[Once type_e_clauses] >> 1918 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1919 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1920 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1921 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> 1922 simp[GSYM AND_IMP_INTRO,type_env_clauses,FDOM_EQ_EMPTY] >> 1923 TRY( discharge_hyps >- ( 1924 rw[] >> 1925 qmatch_assum_rename_tac`FDOM ss ��� _` >> 1926 `tenv_subst ss tenv tenv` by ( 1927 match_mp_tac tenv_subst_id >> 1928 conj_tac >- metis_tac[type_env_EVERY_SUBSET] >> 1929 fs[SUBSET_DEF,IN_DISJOINT] >> 1930 metis_tac[] ) >> 1931 `type_e tenv e (tysubst ss t1)` by ( 1932 match_mp_tac (MP_CANON type_e_subst) >> 1933 metis_tac[type_env_EVERY_FINITE] ) >> 1934 last_x_assum mp_tac >> 1935 Cases_on`e`>>simp[Once eval_cases]>>fs[]>>rw[]>> 1936 fs[type_v_clauses,LENGTH_NIL]>>rw[]>>fs[]>> 1937 fs[type_e_clauses] >- ( 1938 imp_res_tac type_env_ALOOKUP_tenv_SOME >> 1939 fs[] >> rw[] ) >> 1940 metis_tac[])) >> 1941 strip_tac >> 1942 BasicProvers.CASE_TAC >> fs[] >> 1943 qexists_tac`rt'++rt''` >> 1944 qexists_tac`et'++et''` >> 1945 simp[]) >> 1946 conj_tac >- ( 1947 rw[Once type_e_clauses] >> 1948 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1949 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1950 first_assum(match_exists_tac o concl) >> simp[] >> 1951 BasicProvers.CASE_TAC >> fs[] >> simp[] ) >> 1952 (* Fun *) 1953 conj_tac >- ( 1954 simp[type_e_clauses,type_v_clauses] >> 1955 rw[LENGTH_NIL] >> metis_tac[APPEND_NIL]) >> 1956 (* Funrec *) 1957 conj_tac >- ( 1958 simp[type_e_clauses,type_v_clauses] >> 1959 rw[LENGTH_NIL] >> metis_tac[APPEND_NIL]) >> 1960 (* Ref *) 1961 conj_tac >- ( 1962 rw[type_e_clauses] >> 1963 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1964 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1965 qexists_tac`rt'++[t']` >> 1966 qexists_tac`et'` >> 1967 conj_tac >- ( 1968 ONCE_REWRITE_TAC[APPEND_ASSOC] >> 1969 match_mp_tac rich_listTheory.EVERY2_APPEND_suff >> 1970 simp[] >> 1971 reverse conj_tac >- metis_tac[type_v_extend,APPEND_NIL] >> 1972 match_mp_tac(MP_CANON(GEN_ALL LIST_REL_mono)) >> 1973 metis_tac[type_v_extend,APPEND_NIL] ) >> 1974 imp_res_tac LIST_REL_LENGTH >> 1975 simp[type_v_clauses] >> 1976 simp[rich_listTheory.EL_APPEND2] >> 1977 metis_tac[type_v_extend,APPEND_NIL] ) >> 1978 conj_tac >- ( 1979 rw[type_e_clauses] >> 1980 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1981 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1982 first_assum(match_exists_tac o concl) >> simp[] >> 1983 BasicProvers.CASE_TAC >> fs[] >> simp[] ) >> 1984 (* Deref *) 1985 conj_tac >- ( 1986 rw[type_e_clauses] >> 1987 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1988 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1989 first_assum(match_exists_tac o concl) >> simp[] >> 1990 fs[type_v_clauses] >> 1991 fs[LIST_REL_EL_EQN]) >> 1992 conj_tac >- ( 1993 rw[type_e_clauses] >> 1994 spose_not_then strip_assume_tac >> 1995 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 1996 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 1997 spose_not_then strip_assume_tac >> 1998 fs[type_v_clauses] >> 1999 fs[LIST_REL_EL_EQN] ) >> 2000 conj_tac >- ( 2001 rw[type_e_clauses] >> 2002 spose_not_then strip_assume_tac >> 2003 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2004 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2005 Cases_on`v`>>fs[type_v_clauses]) >> 2006 conj_tac >- ( 2007 rw[type_e_clauses] >> 2008 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2009 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2010 first_assum(match_exists_tac o concl) >> simp[] >> 2011 BasicProvers.CASE_TAC >> fs[] >> simp[] ) >> 2012 (* Assign *) 2013 conj_tac >- ( 2014 rw[type_e_clauses] >> 2015 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2016 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2017 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2018 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2019 rw[type_v_clauses] >> 2020 Cases_on`n < LENGTH rt` >- ( 2021 qexists_tac`rt' ++ rt''` >> 2022 qexists_tac`et' ++ et''` >> simp[] >> 2023 fs[type_v_clauses] >> 2024 fs[LIST_REL_EL_EQN,EL_LUPDATE] >> rw[] >> 2025 fs[rich_listTheory.EL_APPEND1] ) >> 2026 qexists_tac`LUPDATE t' (n-LENGTH rt) (rt' ++ rt'')` >> 2027 qexists_tac`et'++et''` >> 2028 imp_res_tac LIST_REL_LENGTH >> fs[] >> simp[] >> 2029 reverse conj_tac >- metis_tac[type_v_extend,APPEND_ASSOC] >> 2030 simp[GSYM rich_listTheory.LUPDATE_APPEND2] >> 2031 match_mp_tac EVERY2_LUPDATE_same >> 2032 fs[type_v_clauses] >> 2033 simp[rich_listTheory.EL_APPEND1,rich_listTheory.EL_APPEND2] >> 2034 simp[rich_listTheory.LUPDATE_APPEND1,rich_listTheory.LUPDATE_APPEND2] >> 2035 simp[LUPDATE_ID] >> rw[] >> 2036 qpat_assum`type_v A X Y Z`mp_tac >> 2037 fs[arithmeticTheory.NOT_LESS] >> 2038 fs[rich_listTheory.EL_APPEND2]) >> 2039 conj_tac >- ( 2040 rw[type_e_clauses] >> 2041 spose_not_then strip_assume_tac >> 2042 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2043 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2044 spose_not_then strip_assume_tac >> 2045 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2046 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2047 Cases_on`v1`>>fs[type_v_clauses] >> 2048 spose_not_then strip_assume_tac >> 2049 imp_res_tac LIST_REL_LENGTH >> fs[] >> 2050 DECIDE_TAC ) >> 2051 conj_tac >- ( 2052 rw[type_e_clauses] >> 2053 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2054 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2055 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2056 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2057 BasicProvers.CASE_TAC >> fs[] >> 2058 qexists_tac`rt' ++ rt''` >> 2059 qexists_tac`et' ++ et''` >> simp[]) >> 2060 conj_tac >- ( 2061 rw[type_e_clauses] >> 2062 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2063 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2064 BasicProvers.CASE_TAC >> fs[] >> 2065 first_assum(match_exists_tac o concl) >> simp[]) >> 2066 (* Letexn *) 2067 conj_tac >- ( 2068 rw[type_e_clauses] >> 2069 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2070 disch_then(qspecl_then[`rt`,`et++[t1]`]mp_tac) >> 2071 simp[AND_IMP_INTRO] >> 2072 discharge_hyps >- ( 2073 simp[type_env_clauses,FDOM_EQ_EMPTY,type_v_clauses,rich_listTheory.EL_APPEND2] >> 2074 conj_tac >- ( 2075 match_mp_tac(MP_CANON(GEN_ALL LIST_REL_mono)) >> 2076 metis_tac[type_v_extend,APPEND_NIL] ) >> 2077 metis_tac[type_v_extend,APPEND_NIL] ) >> 2078 strip_tac >> 2079 qexists_tac`rt'` >> 2080 qexists_tac`[t1]++et'` >> 2081 simp[] >> 2082 BasicProvers.CASE_TAC >> fs[] >> 2083 fs[type_env_clauses] >> simp[] ) >> 2084 (* Raise *) 2085 conj_tac >- ( 2086 rw[type_e_clauses] >> 2087 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2088 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2089 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2090 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2091 fs[type_v_clauses] >> 2092 qexists_tac`rt'++rt''`>> 2093 qexists_tac`et'++et''`>> 2094 rw[] >> simp[rich_listTheory.EL_APPEND1]) >> 2095 conj_tac >- ( 2096 rw[type_e_clauses] >> 2097 spose_not_then strip_assume_tac >> 2098 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2099 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2100 spose_not_then strip_assume_tac >> 2101 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2102 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2103 Cases_on`v1`>>fs[type_v_clauses] ) >> 2104 conj_tac >- ( 2105 rw[type_e_clauses] >> 2106 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2107 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2108 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2109 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2110 qexists_tac`rt'++rt''`>> 2111 qexists_tac`et'++et''`>> 2112 Cases_on`r`>>fs[] >> simp[] ) >> 2113 conj_tac >- ( 2114 rw[type_e_clauses] >> 2115 last_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2116 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2117 Cases_on`r`>>fs[] >> 2118 first_assum(match_exists_tac o concl) >> simp[] ) >> 2119 (* Handle *) 2120 conj_tac >- ( 2121 rw[type_e_clauses] >> 2122 qpat_assum`type_e tenv e' _`(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2123 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2124 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2125 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2126 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2127 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2128 Cases_on`v2`>>fs[]>>rw[]>>fs[type_v_clauses]>> 2129 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2130 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> simp[] >> 2131 (discharge_hyps >- ( 2132 fs[type_env_clauses,FDOM_EQ_EMPTY] >> 2133 rev_full_simp_tac(srw_ss()++ARITH_ss)[rich_listTheory.EL_APPEND1] >> 2134 fs[type_v_clauses] >> 2135 metis_tac[type_v_extend] )) >> 2136 strip_tac >> 2137 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 2138 first_assum(match_exists_tac o concl) >> simp[] >> 2139 Cases_on`r`>>fs[] >> simp[] >> 2140 metis_tac[type_v_extend]) >> 2141 conj_tac >- ( 2142 rw[type_e_clauses] >> 2143 qpat_assum`type_e tenv e' _`(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2144 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2145 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2146 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2147 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2148 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2149 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 2150 first_assum(match_exists_tac o concl) >> simp[]) >> 2151 conj_tac >- ( 2152 rw[type_e_clauses] >> 2153 qpat_assum`type_e tenv e' _`(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2154 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2155 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2156 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2157 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2158 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2159 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 2160 first_assum(match_exists_tac o concl) >> simp[] >> 2161 BasicProvers.CASE_TAC >> fs[] ) >> 2162 conj_tac >- ( 2163 rw[type_e_clauses] >> 2164 spose_not_then strip_assume_tac >> 2165 qpat_assum`type_e tenv e _`(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2166 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2167 spose_not_then strip_assume_tac >> 2168 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2169 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2170 Cases_on`v2`>>fs[type_v_clauses] ) >> 2171 conj_tac >- ( 2172 rw[type_e_clauses] >> 2173 qpat_assum`type_e tenv e _`(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2174 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2175 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2176 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2177 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 2178 first_assum(match_exists_tac o concl) >> simp[] >> 2179 BasicProvers.CASE_TAC >> fs[] >> simp[] ) >> 2180 conj_tac >- ( 2181 rw[type_e_clauses] >> 2182 spose_not_then strip_assume_tac >> 2183 qpat_assum`type_e tenv e _`(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2184 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2185 Cases_on`v1`>>fs[type_v_clauses] ) >> 2186 rw[type_e_clauses] >> 2187 first_assum(fn th => first_x_assum(mp_tac o C MATCH_MP th o REWRITE_RULE[GSYM AND_IMP_INTRO])) >> 2188 disch_then(fn th => first_assum(mp_tac o MATCH_MP th)) >> rw[] >> 2189 full_simp_tac std_ss [GSYM APPEND_ASSOC] >> 2190 first_assum(match_exists_tac o concl) >> simp[] >> 2191 BasicProvers.CASE_TAC >> fs[] >> simp[]) 2192 2193val _ = export_theory() 2194