1(* An untyped call-by-value lambda calculus with a functional big-step 2 * semantics, and a definition of contextual approximation for it. We 3 * use closures rather than substitution in the semantics, and use 4 * De Bruijn indices for variables. *) 5 6open HolKernel boolLib bossLib Parse; 7open integerTheory stringTheory alistTheory listTheory pred_setTheory; 8open pairTheory optionTheory finite_mapTheory arithmeticTheory; 9 10val _ = set_trace "Goalstack.print_goal_at_top" 0; 11val _ = ParseExtras.temp_tight_equality(); 12 13fun term_rewrite tms = let 14 fun f tm = ASSUME (list_mk_forall(free_vars tm,tm)) 15 in rand o concl o QCONV (REWRITE_CONV (map f tms)) end 16 17val _ = new_theory "cbv"; 18 19(* Syntax *) 20 21val _ = Datatype ` 22lit = 23 Int int`; 24 25val _ = Datatype ` 26exp = 27 | Lit lit 28 | Var num 29 | App exp exp 30 | Fun exp 31 | Tick exp`; 32 33(* Values *) 34 35val _ = Datatype ` 36v = 37 | Litv lit 38 | Clos (v list) exp`; 39 40val v_induction = theorem "v_induction"; 41 42val v_ind = 43 v_induction 44 |> Q.SPECL[`P`,`EVERY P`] 45 |> SIMP_RULE (srw_ss()) [] 46 |> UNDISCH |> CONJUNCT1 |> DISCH_ALL 47 |> GEN_ALL 48 |> curry save_thm "v_ind"; 49 50val v_size_def = definition"v_size_def" 51 52val _ = type_abbrev("env",``:v list``) 53 54(* Semantics *) 55 56(* The state of the semantics will have a clock and a store. 57 * Even though we don't have any constructs that access the store, we want the 58 * placeholder. *) 59 60val _ = Datatype ` 61state = <| clock : num; store : v list|>`; 62 63val state_component_equality = theorem "state_component_equality"; 64 65val state_clock_idem = Q.store_thm ("state_clock_idem[simp]", 66`!s. (s with clock := s.clock) = s`, 67 rw [state_component_equality]); 68 69(* machinery for the functional big-step definition *) 70 71val check_clock_def = Define ` 72 check_clock s' s = 73 s' with clock := (if s'.clock ��� s.clock then s'.clock else s.clock)`; 74 75val check_clock_id = prove( 76 ``!s s'. s.clock ��� s'.clock ��� check_clock s s' = s``, 77 rw [check_clock_def, state_component_equality]); 78 79val dec_clock_def = Define ` 80 dec_clock s = s with clock := s.clock - 1`; 81 82(* results *) 83 84val _ = Datatype` 85 r = Rval v 86 | Rfail 87 | Rtimeout`; 88 89(* big-step semantics as a function *) 90 91val sem_def = tDefine "sem" ` 92(sem env s (Lit i) = (Rval (Litv i), s)) ��� 93(sem env s (Var n) = 94 if n < LENGTH env then 95 (Rval (EL n env), s) 96 else 97 (Rfail, s)) ��� 98(sem env s (App e1 e2) = 99 case sem env s e1 of 100 | (Rval v1, s1) => 101 (case sem env (check_clock s1 s) e2 of 102 | (Rval v2, s2) => 103 if s.clock ��� 0 ��� s2.clock ��� 0 then 104 (case v1 of 105 | Clos env' e => 106 sem (v2::env') (dec_clock (check_clock s2 s)) e 107 | _ => (Rfail, s2)) 108 else 109 (Rtimeout, s2) 110 | res => res) 111 | res => res) ��� 112(sem env s (Fun e) = (Rval (Clos env e), s)) ��� 113(sem env s (Tick e) = 114 if s.clock ��� 0 then 115 sem env (dec_clock s) e 116 else 117 (Rtimeout, s))` 118(WF_REL_TAC`inv_image (measure I LEX measure exp_size) 119 (��(env,s,e). (s.clock,e))` >> 120 rpt strip_tac >> TRY DECIDE_TAC >> 121 fs[check_clock_def,dec_clock_def] >> 122 rw[] >> fsrw_tac[ARITH_ss][]); 123 124val sem_ind = theorem "sem_ind"; 125 126val sem_clock = store_thm("sem_clock", 127 ``���env s e r s'. sem env s e = (r, s') ��� s'.clock ��� s.clock``, 128 ho_match_mp_tac sem_ind >> 129 rpt conj_tac >> 130 simp[sem_def] >> 131 rpt gen_tac >> 132 BasicProvers.EVERY_CASE_TAC >> 133 simp[check_clock_def,dec_clock_def] >> 134 rpt(IF_CASES_TAC >> simp[]) >> 135 rpt strip_tac >> res_tac >> simp[] >> fs[]) 136 137(* Remove the extra check_clock calls that were used above to guide the HOL 138 * termination prover *) 139 140val r = term_rewrite [``check_clock s1 s = s1``, 141 ``s.clock <> 0 /\ s1.clock <> 0 <=> s1.clock <> 0``]; 142 143val sem_def = store_thm("sem_def", 144 sem_def |> concl |> r, 145 rpt strip_tac >> 146 rw[Once sem_def] >> 147 BasicProvers.CASE_TAC >> 148 imp_res_tac sem_clock >> 149 simp[check_clock_id] >> 150 BasicProvers.CASE_TAC >> 151 imp_res_tac sem_clock >> 152 simp[check_clock_id] >> 153 BasicProvers.EVERY_CASE_TAC >> fs[] >> 154 imp_res_tac sem_clock >> 155 simp[check_clock_id] >> 156 `F` suffices_by rw[] >> 157 DECIDE_TAC); 158 159val sem_ind = store_thm("sem_ind", 160 sem_ind |> concl |> r, 161 ntac 2 strip_tac >> 162 ho_match_mp_tac sem_ind >> 163 rw[] >> 164 first_x_assum match_mp_tac >> 165 rw[] >> fs[] >> 166 res_tac >> 167 imp_res_tac sem_clock >> 168 fsrw_tac[ARITH_ss][check_clock_id] >> rfs[] >> 169 fsrw_tac[ARITH_ss][check_clock_id]) 170 171(* Misc lemmas stating that the clock acts like a clock. These could probably be 172 * unified and simplified *) 173 174val sem_clock_add_lem = Q.prove ( 175`!env s1 e v s2 c1 c2. 176 sem env s1 e = (Rval v, s2) ��� 177 s1.clock = c1 178 ��� 179 sem env (s1 with clock := c1 + c2) e = (Rval v, s2 with clock := s2.clock + c2)`, 180 ho_match_mp_tac sem_ind >> 181 rw [sem_def, state_component_equality] >> 182 rw [] >> 183 `?res s2. sem env s1 e = (res, s2)` by metis_tac [pair_CASES] >> 184 fs [] 185 >- (Cases_on `res` >> 186 fs [] >> 187 `?res' s3. sem env s2' e' = (res', s3)` by metis_tac [pair_CASES] >> 188 fs [] >> 189 Cases_on `res'` >> 190 fs [] >> 191 Cases_on `s3.clock = 0` >> 192 fs [] >> 193 Cases_on `v'` >> 194 fs [dec_clock_def] >> 195 last_x_assum (qspec_then `c2` mp_tac) >> 196 rw [] >> 197 full_simp_tac (srw_ss()++ ARITH_ss) [] >> 198 `s3.clock ��� 1 + c2 = c2 + s3.clock ��� 1` by decide_tac >> 199 fs []) 200 >- (fs [dec_clock_def] >> 201 full_simp_tac (srw_ss()++ ARITH_ss) [] >> 202 `c2 + s1.clock ��� 1 = c2 + (s1.clock ��� 1)` by decide_tac >> 203 metis_tac [])); 204 205val sem_clock_add_fail_lem = Q.prove ( 206`!env s1 e v s2 c1 c2. 207 sem env s1 e = (Rfail, s2) ��� 208 s1.clock = c1 209 ��� 210 sem env (s1 with clock := c1 + c2) e = (Rfail, s2 with clock := s2.clock + c2)`, 211 ho_match_mp_tac sem_ind >> 212 rw [sem_def, state_component_equality] >> 213 rw [] 214 >- (`?res s2. sem env s1 e = (res, s2)` by metis_tac [pair_CASES] >> 215 fs [] >> 216 Cases_on `res` >> 217 fs [] >> 218 `?res' s3. sem env s2' e' = (res', s3)` by metis_tac [pair_CASES] >> 219 fs [] >> 220 Cases_on `res'` >> 221 fs [] >> 222 `sem env (s1 with clock := s1.clock + c2) e = (Rval v,s2' with clock := s2'.clock + c2)` 223 by metis_tac [sem_clock_add_lem] 224 >- (`sem env (s2' with clock := s2'.clock + c2) e' = (Rval v',s3 with clock := s3.clock + c2)` 225 by metis_tac [sem_clock_add_lem] >> 226 Cases_on `s3.clock = 0` >> 227 fs [] >> 228 Cases_on `v` >> 229 fs [dec_clock_def] ) 230 >- (`sem env (s2' with clock := c2 + s2'.clock) e' = (Rfail,s3 with clock := c2 + s3.clock)` 231 by metis_tac [] >> 232 fs[])) 233 >- (fs [dec_clock_def] >> 234 full_simp_tac (srw_ss()++ ARITH_ss) [] >> 235 `c2 + s1.clock ��� 1 = c2 + (s1.clock ��� 1)` by decide_tac >> 236 metis_tac [])); 237 238val sem_clock_add = Q.store_thm ("sem_clock_add", 239`!env s1 e v s2 c1 c2. 240 sem env (s1 with clock := c1) e = (Rval v, s2) 241 ��� 242 sem env (s1 with clock := c1 + c2) e = (Rval v, s2 with clock := s2.clock + c2)`, 243 srw_tac[] [] >> 244 qabbrev_tac `s1' = s1 with clock := c1` >> 245 `(s1 with clock := c1 + c2) = s1' with clock := s1'.clock + c2` 246 by fs [state_component_equality, Abbr`s1'`] >> 247 srw_tac[] [] >> 248 match_mp_tac sem_clock_add_lem >> 249 rw []); 250 251val sem_clock_add_fail = Q.store_thm ("sem_clock_add_fail", 252`!env s1 e v s2 c1 c2. 253 sem env (s1 with clock := c1) e = (Rfail, s2) 254 ��� 255 sem env (s1 with clock := c1 + c2) e = (Rfail, s2 with clock := s2.clock + c2)`, 256 srw_tac[] [] >> 257 qabbrev_tac `s1' = s1 with clock := c1` >> 258 `(s1 with clock := c1 + c2) = s1' with clock := s1'.clock + c2` 259 by fs [state_component_equality, Abbr`s1'`] >> 260 srw_tac[] [] >> 261 match_mp_tac sem_clock_add_fail_lem >> 262 rw []); 263 264val sem_clock_timeout0 = Q.store_thm ("sem_clock_timeout0", 265`!env s e s'. sem env s e = (Rtimeout, s') ��� s'.clock = 0`, 266 ho_match_mp_tac sem_ind >> 267 rw [sem_def] >> 268 BasicProvers.EVERY_CASE_TAC >> 269 fs [] >> 270 rw []); 271 272 (* This is proved, but we turn out to not need it *) 273val sem_clock_sub = Q.store_thm ("sem_clock_sub", 274`!env s1 e v s2. 275 sem env s1 e = (Rval v,s2) 276 ��� 277 sem env (s1 with clock := s1.clock - s2.clock) e = (Rval v, s2 with clock := 0)`, 278 ho_match_mp_tac sem_ind >> 279 rw [sem_def] 280 >- (Cases_on `sem env s1 e` >> 281 Cases_on `q` >> 282 fs [dec_clock_def] >> 283 rw [] >> 284 Cases_on `sem env r e'` >> 285 Cases_on `q` >> 286 fs [] >> 287 rw [] >> 288 Cases_on `r'.clock ��� 0` >> 289 fs [] >> 290 Cases_on `v'` >> 291 fs [] >> 292 rw [] >> 293 imp_res_tac sem_clock >> 294 fs [] >> 295 `sem env (s1 with clock := (s1.clock ��� r.clock) + (r.clock ��� s2.clock)) e = 296 (Rval (Clos l e''), (r with clock := 0) with clock := (r with clock := 0).clock + (r.clock ��� s2.clock))` 297 by metis_tac [sem_clock_add] >> 298 fs [] >> 299 rw [] >> 300 `s1.clock ��� r.clock + (r.clock ��� s2.clock) = s1.clock - s2.clock` by decide_tac >> 301 fs [] >> 302 `sem env (r with clock := (r.clock ��� r'.clock) + (r'.clock ��� s2.clock)) e' = 303 (Rval v'', (r' with clock := 0) with clock := (r' with clock := 0).clock + (r'.clock ��� s2.clock))` 304 by metis_tac [sem_clock_add] >> 305 fs [] >> 306 rw [] >> 307 `r.clock ��� r'.clock + (r'.clock ��� s2.clock) = r.clock - s2.clock` by intLib.ARITH_TAC >> 308 fs []) 309 >- (rw [] >> 310 fs [dec_clock_def] >> 311 imp_res_tac sem_clock >> 312 fs [] >> 313 intLib.ARITH_TAC)); 314 315(* The value doesn't depend on which clock you use to compute it *) 316val sem_clock_val_determ_lem = Q.prove ( 317`!env s e v' s' v'' s'' c. 318 sem env s e = (Rval v', s') ��� 319 sem env (s with clock := c) e = (Rval v'', s'') 320 ��� 321 v' = v'' ��� 322 s' = (s'' with clock := s'.clock)`, 323 ho_match_mp_tac sem_ind >> 324 rw [sem_def, state_component_equality] 325 >- metis_tac [] 326 >- metis_tac [] 327 >- (Cases_on `sem env s e` >> 328 Cases_on `q` >> 329 fs [] >> 330 Cases_on `sem env (s with clock := c) e` >> 331 Cases_on `q` >> 332 fs [] >> 333 `v = v''' ��� r.store = r'.store` by metis_tac [] >> 334 rw [] >> 335 Cases_on `sem env r e'` >> 336 Cases_on `q` >> 337 fs [] >> 338 Cases_on `sem env r' e'` >> 339 Cases_on `q` >> 340 fs [] >> 341 `v''' = v'''' ��� r''.store = r'''.store` 342 by (first_x_assum match_mp_tac >> 343 qexists_tac `r'.clock` >> 344 fs [] >> 345 `r' = r with clock := r'.clock` by rw [state_component_equality] >> 346 metis_tac []) >> 347 rw [] >> 348 BasicProvers.EVERY_CASE_TAC >> 349 fs [] >> 350 fs [dec_clock_def] >> 351 res_tac >> 352 fs [] >> 353 `(r''' with clock := r'''.clock - 1) = (r'' with clock := r'''.clock - 1)` by rw [state_component_equality] >> 354 metis_tac []) 355 >- (Cases_on `sem env s e` >> 356 Cases_on `q` >> 357 fs [] >> 358 Cases_on `sem env (s with clock := c) e` >> 359 Cases_on `q` >> 360 fs [] >> 361 `v = v''' ��� r.store = r'.store` by metis_tac [] >> 362 rw [] >> 363 Cases_on `sem env r e'` >> 364 Cases_on `q` >> 365 fs [] >> 366 Cases_on `sem env r' e'` >> 367 Cases_on `q` >> 368 fs [] >> 369 `v''' = v'''' ��� r''.store = r'''.store` 370 by (first_x_assum match_mp_tac >> 371 qexists_tac `r'.clock` >> 372 fs [] >> 373 `r' = r with clock := r'.clock` by rw [state_component_equality] >> 374 metis_tac []) >> 375 rw [] >> 376 BasicProvers.EVERY_CASE_TAC >> 377 fs [] >> 378 fs [dec_clock_def] >> 379 res_tac >> 380 fs [] >> 381 `(r''' with clock := r'''.clock - 1) = (r'' with clock := r'''.clock - 1)` by rw [state_component_equality] >> 382 metis_tac []) 383 >- metis_tac [] 384 >- (BasicProvers.EVERY_CASE_TAC >> 385 fs [] >> 386 fs [dec_clock_def] >> 387 metis_tac []) 388 >- (BasicProvers.EVERY_CASE_TAC >> 389 fs [] >> 390 fs [dec_clock_def] >> 391 metis_tac [])); 392 393val sem_clock_val_determ = Q.store_thm ("sem_clock_val_determ", 394`!env s e v' s' v'' s'' c1 c2. 395 sem env (s with clock := c1) e = (Rval v', s') ��� 396 sem env (s with clock := c2) e = (Rval v'', s'') 397 ��� 398 v' = v'' ��� 399 s' = (s'' with clock := s'.clock)`, 400 rpt gen_tac >> 401 DISCH_TAC >> 402 match_mp_tac sem_clock_val_determ_lem >> 403 qexists_tac `env` >> 404 qexists_tac `s with clock := c1` >> 405 rw [] >> 406 metis_tac [sem_clock_val_determ_lem]); 407 408(* The top-level semantics *) 409 410val eval_def = Define ` 411(eval e (Rval v) = 412 ?c s. sem [] <| store := []; clock := c |> e = (Rval v, s)) ��� 413(eval e Rfail = 414 ?c s. sem [] <| store := []; clock := c |> e = (Rfail, s)) ��� 415(eval e Rtimeout = 416 ���c. ���s. sem [] <| store := []; clock := c |> e = (Rtimeout, s))`; 417 418(* Contexts *) 419 420val _ = Datatype ` 421ctxt = 422 | Hole 423 | FunC ctxt 424 | App1C ctxt exp 425 | App2C exp ctxt 426 | TickC ctxt`; 427 428(* Fill the hole in a context with an expression *) 429val ctxt_to_exp_def = Define ` 430(ctxt_to_exp Hole e = e) ��� 431(ctxt_to_exp (FunC ctxt) e = Fun (ctxt_to_exp ctxt e)) ��� 432(ctxt_to_exp (App1C ctxt e1) e = App (ctxt_to_exp ctxt e) e1) ��� 433(ctxt_to_exp (App2C e1 ctxt) e = App e1 (ctxt_to_exp ctxt e)) ��� 434(ctxt_to_exp (TickC ctxt) e = Tick (ctxt_to_exp ctxt e))`; 435 436(* Contextual approximation must preserve divergence and termination, but 437 * can relate a failing computation to anything. *) 438val res_approx_def = Define ` 439(res_approx Rfail _ ��� T) ��� 440(res_approx Rtimeout Rtimeout ��� T) ��� 441(res_approx (Rval _) (Rval _) ��� T) ��� 442(res_approx _ _ ��� F)`; 443 444val ctxt_approx_def = Define ` 445ctxt_approx e1 e2 ��� 446 !ctxt r1 r2. 447 eval (ctxt_to_exp ctxt e1) r1 ��� 448 eval (ctxt_to_exp ctxt e2) r2 449 ��� 450 res_approx r1 r2`; 451 452val _ = export_theory (); 453