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