1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_semantics"; 2 3open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 4open optionTheory arithmeticTheory relationTheory; 5 6open lisp_sexpTheory lisp_parseTheory; 7 8infix \\ 9val op \\ = op THEN; 10 11 12(* abstract syntax of well-formed Lisp prorams *) 13 14val _ = Hol_datatype ` 15 func = PrimitiveFun of lisp_primitive_op 16 | Define | Print | Error | Funcall | Fun of string`; 17 18val _ = Hol_datatype ` 19 term = Const of SExp 20 | Var of string 21 | App of func => term list 22 | If of term => term => term 23 | LamApp of string list => term => term list 24 (* only macros below *) 25 | Let of (string # term) list => term 26 | LetStar of (string # term) list => term 27 | Cond of (term # term) list 28 | Or of term list | And of term list 29 | First of term | Second of term | Third of term 30 | Fourth of term | Fifth of term | List of term list 31 | Defun of string => string list => SExp`; 32 33val term_11 = fetch "-" "term_11"; 34val term_distinct = fetch "-" "term_distinct"; 35val term_size_def = fetch "-" "term_size_def"; 36val func_11 = fetch "-" "func_11"; 37 38 39(* reading a program, i.e. term, from an s-expression -- sexp2term *) 40 41val list2sexp_def = Define ` 42 (list2sexp [] = Sym "NIL") /\ 43 (list2sexp (x::xs) = Dot x (list2sexp xs))`; 44 45val sym2prim_def = Define ` 46 sym2prim s = 47 if s = "CONS" then SOME opCONS else 48 if s = "EQUAL" then SOME opEQUAL else 49 if s = "<" then SOME opLESS else 50 if s = "SYMBOL-<" then SOME opSYMBOL_LESS else 51 if s = "+" then SOME opADD else 52 if s = "-" then SOME opSUB else 53 if s = "CONSP" then SOME opCONSP else 54 if s = "NATP" then SOME opNATP else 55 if s = "SYMBOLP" then SOME opSYMBOLP else 56 if s = "CAR" then SOME opCAR else 57 if s = "CDR" then SOME opCDR else NONE`; 58 59val sexp2list_def = Define ` 60 (sexp2list (Val n) = []) /\ 61 (sexp2list (Sym s) = []) /\ 62 (sexp2list (Dot x y) = x::sexp2list y)`; 63 64val IMP_isDot = prove( 65 ``!x. ~isVal x /\ ~isSym x ==> isDot x``, 66 Cases \\ EVAL_TAC); 67 68val MEM_sexp2list_LSIZE = prove( 69 ``!b a. MEM a (sexp2list b) ==> LSIZE a < LSIZE b``, 70 Induct \\ SIMP_TAC std_ss [sexp2list_def,MEM,LSIZE_def] \\ REPEAT STRIP_TAC 71 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ DECIDE_TAC); 72 73val LSIZE_CAR_LESS = prove( 74 ``!x m. LSIZE x < m ==> LSIZE (CAR x) < m``, 75 Cases \\ SIMP_TAC std_ss [CAR_def,LSIZE_def] \\ DECIDE_TAC); 76 77val LSIZE_CDR_LESS = prove( 78 ``!x m. LSIZE x < m ==> LSIZE (CDR x) < m``, 79 Cases \\ SIMP_TAC std_ss [CDR_def,LSIZE_def] \\ DECIDE_TAC); 80 81val sexp2term_def = tDefine "sexp2term" ` 82 sexp2term x = if x = Sym "T" then Const x else 83 if x = Sym "NIL" then Const x else 84 if isVal x then Const x else 85 if isSym x then Var (getSym x) else 86 let x1 = CAR x in 87 let x2 = CAR (CDR x) in 88 let x3 = CAR (CDR (CDR x)) in 89 let x4 = CAR (CDR (CDR (CDR x))) in 90 if x1 = Sym "QUOTE" then Const x2 else 91 if x1 = Sym "IF" then 92 If (sexp2term x2) (sexp2term x3) (sexp2term x4) else 93 if ~(sym2prim (getSym x1) = NONE) then 94 App (PrimitiveFun (THE (sym2prim (getSym x1)))) 95 (MAP sexp2term (sexp2list (CDR x))) else 96 if x1 = Sym "FIRST" then First (sexp2term x2) else 97 if x1 = Sym "SECOND" then Second (sexp2term x2) else 98 if x1 = Sym "THIRD" then Third (sexp2term x2) else 99 if x1 = Sym "FOURTH" then Fourth (sexp2term x2) else 100 if x1 = Sym "FIFTH" then Fifth (sexp2term x2) else 101 if x1 = Sym "OR" then Or (MAP sexp2term (sexp2list (CDR x))) else 102 if x1 = Sym "AND" then And (MAP sexp2term (sexp2list (CDR x))) else 103 if x1 = Sym "LIST" then List (MAP sexp2term (sexp2list (CDR x))) else 104 if x1 = Sym "DEFUN" then 105 Defun (getSym x2) (MAP getSym (sexp2list x3)) x4 else 106 if x1 = Sym "COND" then 107 Cond (MAP (\y. (sexp2term (CAR y), sexp2term (CAR (CDR y)))) 108 (sexp2list (CDR x))) else 109 if x1 = Sym "LET" then 110 Let (MAP (\y. (getSym (CAR y), sexp2term (CAR (CDR y)))) 111 (sexp2list x2)) (sexp2term x3) else 112 if x1 = Sym "LET*" then 113 LetStar (MAP (\y. (getSym (CAR y), sexp2term (CAR (CDR y)))) 114 (sexp2list x2)) (sexp2term x3) else 115 if CAR x1 = Sym "LAMBDA" then 116 let y2 = CAR (CDR x1) in 117 let y3 = CAR (CDR (CDR x1)) in 118 LamApp (MAP getSym (sexp2list y2)) (sexp2term y3) 119 (MAP sexp2term (sexp2list (CDR x))) else 120 if x1 = Sym "DEFINE" then 121 App Define (MAP sexp2term (sexp2list (CDR x))) else 122 if x1 = Sym "ERROR" then 123 App Error (MAP sexp2term (sexp2list (CDR x))) else 124 if x1 = Sym "FUNCALL" then 125 App Funcall (MAP sexp2term (sexp2list (CDR x))) else 126 if x1 = Sym "PRINT" then 127 App Print (MAP sexp2term (sexp2list (CDR x))) 128 else (* user-defined fun *) 129 App (Fun (getSym x1)) 130 (MAP sexp2term (sexp2list (CDR x)))` 131 (WF_REL_TAC `measure LSIZE` 132 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC IMP_isDot 133 \\ FULL_SIMP_TAC std_ss [isDot_thm,LSIZE_def,CDR_def,CAR_def] 134 \\ IMP_RES_TAC MEM_sexp2list_LSIZE 135 \\ POP_ASSUM MP_TAC \\ FULL_SIMP_TAC std_ss [CDR_def] 136 \\ REPEAT STRIP_TAC 137 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS) 138 \\ REPEAT (MATCH_MP_TAC LSIZE_CDR_LESS) \\ REPEAT DECIDE_TAC 139 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [CAR_def,LSIZE_def] \\ DECIDE_TAC); 140 141 142(* a structural operational semantics *) 143 144val EVAL_DATA_OP_def = Define ` 145 (EVAL_DATA_OP opCONS = ((\xs. LISP_CONS (EL 0 xs) (EL 1 xs)), 2)) /\ 146 (EVAL_DATA_OP opEQUAL = ((\xs. LISP_EQUAL (EL 0 xs) (EL 1 xs)), 2)) /\ 147 (EVAL_DATA_OP opLESS = ((\xs. LISP_LESS (EL 0 xs) (EL 1 xs)), 2)) /\ 148 (EVAL_DATA_OP opSYMBOL_LESS = ((\xs. LISP_SYMBOL_LESS (EL 0 xs) (EL 1 xs)), 2)) /\ 149 (EVAL_DATA_OP opADD = ((\xs. LISP_ADD (EL 0 xs) (EL 1 xs)), 2)) /\ 150 (EVAL_DATA_OP opSUB = ((\xs. LISP_SUB (EL 0 xs) (EL 1 xs)), 2)) /\ 151 (EVAL_DATA_OP opCONSP = ((\xs. LISP_CONSP (EL 0 xs)), 1)) /\ 152 (EVAL_DATA_OP opNATP = ((\xs. LISP_NUMBERP (EL 0 xs)), 1)) /\ 153 (EVAL_DATA_OP opSYMBOLP = ((\xs. LISP_SYMBOLP (EL 0 xs)), 1)) /\ 154 (EVAL_DATA_OP opCAR = ((\xs. CAR (EL 0 xs)), 1)) /\ 155 (EVAL_DATA_OP opCDR = ((\xs. CDR (EL 0 xs)), (1:num)))`; 156 157val VarBindAux_def = Define ` 158 (VarBindAux [] args = FEMPTY) /\ 159 (VarBindAux (p::ps) [] = FEMPTY) /\ 160 (VarBindAux (p::ps) (a::as) = (VarBindAux ps as) |+ (p,a))`; 161 162val VarBind_def = Define ` 163 VarBind params args = VarBindAux (REVERSE params) (REVERSE args)`; 164 165val add_def_def = Define ` 166 add_def fns x = FUNION fns (FEMPTY |+ x)`; 167 168val (R_ev_rules,R_ev_ind,R_ev_cases) = Hol_reln ` 169 (!s a fns io ok. 170 R_ev (Const s, a,fns,io,ok) (s,fns,io,ok)) 171 /\ 172 (!x (a: string |-> SExp) fns io ok. 173 x IN FDOM a ==> 174 R_ev (Var x,a,fns,io,ok) (a ' x,fns,io,ok)) 175 /\ 176 (!a fns io ok s fns1 io1 ok1. 177 R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 178 R_ev (Or [],a,fns,io,ok) (s,fns1,io1,ok1)) 179 /\ 180 (!a fns io s1 fns1 io1 t ts ok. 181 R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 ==> 182 R_ev (Or (t::ts),a,fns,io,ok) (s1,fns1,io1,ok1)) 183 /\ 184 (!a fns io s1 fns1 io1 s2 fns2 io2 t ts ok ok2. 185 R_ev (t,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~(isTrue s1) /\ 186 R_ev (Or ts,a,fns1,io1,ok1) (s2,fns2,io2,ok2) ==> 187 R_ev (Or (t::ts),a,fns,io,ok) (s2,fns2,io2,ok2)) 188 /\ 189 (!e1 e2 e3 s1 s a ok1 ok2. 190 R_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ ~isTrue s1 /\ 191 R_ev (e3,a,fns1,io1,ok1) (s,fns2,io2,ok2) 192 ==> 193 R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 194 /\ 195 (!e1 e2 e3 s1 s a ok1 ok2. 196 R_ev (e1,a,fns,io,ok) (s1,fns1,io1,ok1) /\ isTrue s1 /\ 197 R_ev (e2,a,fns1,io1,ok1) (s,fns2,io2,ok2) 198 ==> 199 R_ev (If e1 e2 e3,a,fns,io,ok) (s,fns2,io2,ok2)) 200 /\ 201 (!e xs ys fns a ok1 ok2. 202 R_evl (ys,a,fns,io,ok) (sl,fns1,io1,ok1) /\ (LENGTH xs = LENGTH ys) /\ 203 R_ev (e,FUNION (VarBind xs sl) a,fns1,io1,ok1) (x,fns2,io2,ok2) 204 ==> 205 R_ev (LamApp xs e ys,a,fns,io,ok) (x,fns2,io2,ok2)) 206 /\ 207 (!el args a fc fns x ok1 ok2. 208 R_evl (el,a,fns,io,ok) (args,fns1,io1,ok1) /\ 209 R_ap (fc,args,a,fns1,io1,ok1) (x,fns2,io2,ok2) 210 ==> 211 R_ev (App fc el,a,fns,io,ok) (x,fns2,io2,ok2)) 212 /\ 213 (!fc args a fns f. 214 (EVAL_DATA_OP fc = (f,LENGTH args)) 215 ==> 216 R_ap (PrimitiveFun fc,args,a,fns,io,ok) (f args,fns,io,ok)) 217 /\ 218 (!args a fc fns params exp x ok2. 219 fc IN FDOM fns /\ 220 (fns ' fc = (params,exp)) /\ (LENGTH params = LENGTH args) /\ 221 R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2) 222 ==> 223 R_ap (Fun fc,args,a,fns,io:string,ok) (x,fns2,io2,ok2)) 224 /\ 225 (!args a fns io. 226 R_ap (Print,args,a,fns,io,ok) (Sym "NIL",fns, 227 io ++ sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n",ok)) 228 /\ 229 (!a fns fc formals body. 230 R_ap (Define,[fc; formals; body],a,fns,io,ok) 231 (Sym "NIL",add_def fns (getSym fc,MAP getSym (sexp2list formals),sexp2term body), 232 io,ok /\ ~(getSym fc IN FDOM fns))) 233 /\ 234 (!args a fns io anything. 235 R_ap (Error,args,a,fns,io,ok) (anything,fns, 236 io ++ sexp2string (list2sexp (Sym "ERROR"::args)) ++ "\n",F)) 237 /\ 238 (!args params a fname fns x ok2. 239 fname IN FDOM fns /\ 240 (fns ' fname = (params,exp)) /\ (LENGTH params = LENGTH args) /\ 241 R_ev (exp,VarBind params args,fns,io,ok) (x,fns2,io2,ok2) 242 ==> 243 R_ap (Funcall,Sym fname::args,a,fns,io,ok) (x,fns2,io2,ok2)) 244 /\ (* give short-cut semantics for failure states *) 245 (!f args a fns io res. 246 f IN FDOM fns /\ 247 (fns ' f = (params,exp)) /\ (LENGTH params = LENGTH args) ==> 248 R_ap (Fun f,args,a,fns,io,F) (res,fns,io,F)) 249 /\ (* give short-cut semantics for failure states *) 250 (!args a fns io res. 251 R_ap (Funcall,args,a,fns,io,F) (res,fns,io,F)) 252 /\ 253 (!a. 254 R_evl ([],a,fns,io,ok) ([],fns,io,ok)) 255 /\ 256 (!e el s sl a ok1 ok2. 257 R_ev (e,a,fns,io,ok) (s,fns1,io1,ok1) /\ 258 R_evl (el,a,fns1,io1,ok1) (sl,fns2,io2,ok2) 259 ==> 260 R_evl (e::el,a,fns,io,ok) (s::sl,fns2,io2,ok2)) 261 262 /\ (* semantics of macros below *) 263 264 (!e a fns io s fns1 io1 ok1. 265 R_ev (App (PrimitiveFun opCAR) [e],a,fns,io,ok) (s,fns1,io1,ok1) ==> 266 R_ev (First e,a,fns,io,ok) (s,fns1,io1,ok1)) 267 /\ 268 (!e a fns io s fns1 io1 ok1. 269 R_ev (First (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 270 R_ev (Second e,a,fns,io,ok) (s,fns1,io1,ok1)) 271 /\ 272 (!e a fns io s fns1 io1 ok1. 273 R_ev (Second (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 274 R_ev (Third e,a,fns,io,ok) (s,fns1,io1,ok1)) 275 /\ 276 (!e a fns io s fns1 io1 ok1. 277 R_ev (Third (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 278 R_ev (Fourth e,a,fns,io,ok) (s,fns1,io1,ok1)) 279 /\ 280 (!e a fns io s fns1 io1 ok1. 281 R_ev (Fourth (App (PrimitiveFun opCDR) [e]),a,fns,io,ok) (s,fns1,io1,ok1) ==> 282 R_ev (Fifth e,a,fns,io,ok) (s,fns1,io1,ok1)) 283 /\ 284 (!zs x a fns io s fns1 io1 ok1. 285 R_ev (LamApp (MAP FST zs) x (MAP SND zs),a,fns,io,ok) (s,fns1,io1,ok1) ==> 286 R_ev (Let zs x,a,fns,io,ok) (s,fns1,io1,ok1)) 287 /\ 288 (!x a fns io s fns1 io1 ok1. 289 R_ev (x,a,fns,io,ok) (s,fns1,io1,ok1) ==> 290 R_ev (LetStar [] x,a,fns,io,ok) (s,fns1,io1,ok1)) 291 /\ 292 (!z zs x a fns io s fns1 io1 ok1. 293 R_ev (Let [z] (LetStar zs x),a,fns,io,ok) (s,fns1,io1,ok1) ==> 294 R_ev (LetStar (z::zs) x,a,fns,io,ok) (s,fns1,io1,ok1)) 295 /\ 296 (!a fns io s fns1 io1 ok1. 297 R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 298 R_ev (Cond [],a,fns,io,ok) (s,fns1,io1,ok1)) 299 /\ 300 (!x1 x2 qs a fns io s fns1 io1 ok1. 301 R_ev (If x1 x2 (Cond qs),a,fns,io,ok) (s,fns1,io1,ok1) ==> 302 R_ev (Cond ((x1,x2)::qs),a,fns,io,ok) (s,fns1,io1,ok1)) 303 /\ 304 (!a fns io s fns1 io1 ok1. 305 R_ev (Const (Sym "T"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 306 R_ev (And [],a,fns,io,ok) (s,fns1,io1,ok1)) 307 /\ 308 (!a fns io s fns1 io1 ok1. 309 R_ev (Const (Sym "NIL"),a,fns,io,ok) (s,fns1,io1,ok1) ==> 310 R_ev (List [],a,fns,io,ok) (s,fns1,io1,ok1)) 311 /\ 312 (!a fns io s fns1 io1 ok1. 313 R_ev (t,a,fns,io,ok) (s,fns1,io1,ok1) ==> 314 R_ev (And [t],a,fns,io,ok) (s,fns1,io1,ok1)) 315 /\ 316 (!a fns io s fns1 io1 ok1. 317 R_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,fns,io,ok) (s,fns1,io1,ok1) ==> 318 R_ev (And (t1::t2::ts),a,fns,io,ok) (s,fns1,io1,ok1)) 319 /\ 320 (!a fns io s fns1 io1 ok1. 321 R_ev (App (PrimitiveFun opCONS) [t;List ts],a,fns,io,ok) (s,fns1,io1,ok1) ==> 322 R_ev (List (t::ts),a,fns,io,ok) (s,fns1,io1,ok1)) 323 /\ 324 (!fname ps body a fns io s fns1 io1 ok1. 325 R_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,fns,io,ok) (s,fns1,io1,ok1) ==> 326 R_ev (Defun fname ps body,a,fns,io,ok) (s,fns1,io1,ok1))`; 327 328val R_evl_LENGTH = save_thm("R_evl_LENGTH", 329 R_ev_ind 330 |> Q.SPECL [`\x y. T`,`\x y. (LENGTH (FST x) = LENGTH (FST y))`,`\x y. T`] 331 |> SIMP_RULE std_ss [LENGTH]); 332 333 334(* semantics of the read-eval-print loop *) 335 336val (R_exec_rules,R_exec_ind,R_exec_cases) = Hol_reln ` 337 (!input fns io rest. 338 (is_eof input = (T,rest)) ==> 339 R_exec (input,fns,io) (io,T)) 340 /\ 341 (!input fns io input2 exp rest s fns2 io2 ok2 io3 ok3. 342 (is_eof input = (F,input2)) /\ 343 (sexp_parse_stream input2 = (exp,rest)) /\ 344 R_ev (sexp2term exp,FEMPTY,fns,io,T) (s,fns2,io2,ok2) /\ 345 R_exec (rest,fns2,io2 ++ sexp2string s ++ "\n") (io3,ok3) ==> 346 R_exec (input,fns,io) (io3,ok2 /\ ok3))`; 347 348 349(* theorems about the semantics *) 350 351val R_ev_induct = IndDefLib.derive_strong_induction(R_ev_rules,R_ev_ind); 352 353val PULL_FORALL_IMP = METIS_PROVE [] ``(p ==> !x. q x) = !x. p ==> q x``; 354 355val R_ev_OK = prove( 356 ``(!x y. R_ap x y ==> SND (SND (SND y)) ==> (SND (SND (SND (SND (SND x)))))) /\ 357 (!x y. R_evl x y ==> SND (SND (SND y)) ==> (SND (SND (SND (SND (x)))))) /\ 358 (!x y. R_ev x y ==> SND (SND (SND y)) ==> (SND (SND (SND (SND (x))))))``, 359 HO_MATCH_MP_TAC R_ev_ind \\ SIMP_TAC std_ss [pairTheory.FORALL_PROD,LET_DEF]); 360 361val R_ev_T_11_lemma = prove( 362 ``(!x y. R_ap x y ==> !z. SND (SND (SND y)) /\ R_ap x z ==> (y = z)) /\ 363 (!x y. R_evl x y ==> !z. SND (SND (SND y)) /\ R_evl x z ==> (y = z)) /\ 364 (!x y. R_ev x y ==> !z. SND (SND (SND y)) /\ R_ev x z ==> (y = z))``, 365 HO_MATCH_MP_TAC R_ev_induct \\ SIMP_TAC std_ss [] 366 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 367 \\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [R_ev_cases] \\ SIMP_TAC (srw_ss()) [] 368 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ RES_TAC 369 \\ IMP_RES_TAC R_ev_OK \\ FULL_SIMP_TAC std_ss [listTheory.CONS_11] 370 \\ RES_TAC \\ FULL_SIMP_TAC std_ss []) 371 |> SIMP_RULE std_ss [pairTheory.FORALL_PROD,PULL_FORALL_IMP]; 372 373val R_ev_T_11 = store_thm("R_ev_T_11", 374 ``!x y. R_ev x (res,k,io,T) /\ R_ev x y ==> (y = (res,k,io,T))``, 375 FULL_SIMP_TAC std_ss [pairTheory.FORALL_PROD] \\ REPEAT STRIP_TAC 376 \\ IMP_RES_TAC R_ev_T_11_lemma \\ FULL_SIMP_TAC std_ss []); 377 378val R_ap_T_11 = store_thm("R_ap_T_11", 379 ``!x y. R_ap x (res,k,io,T) /\ R_ap x y ==> (y = (res,k,io,T))``, 380 FULL_SIMP_TAC std_ss [pairTheory.FORALL_PROD] \\ REPEAT STRIP_TAC 381 \\ IMP_RES_TAC R_ev_T_11_lemma \\ FULL_SIMP_TAC std_ss []); 382 383val R_ap_F_11 = store_thm("R_ap_F_11", 384 ``R_ap x (res,k,io,F) /\ R_ap x (res2,k2,io2,b) ==> ~b``, 385 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 386 \\ IMP_RES_TAC R_ap_T_11 \\ FULL_SIMP_TAC std_ss []); 387 388Theorem R_ev_T_cases: 389 (R_ev (x,env,k,io,ok) (r,k',io',T) ��� 390 R_ev (x,env,k,io,T) (r,k',io',T) /\ ok) /\ 391 (R_evl (xs,env,k,io,ok) (rs,k',io',T) ��� 392 R_evl (xs,env,k,io,T) (rs,k',io',T) /\ ok) /\ 393 (R_ap (f,args,env,k,io,ok) (r,k',io',T) ��� 394 R_ap (f,args,env,k,io,T) (r,k',io',T) /\ ok) 395Proof REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 396 \\ IMP_RES_TAC R_ev_OK \\ FULL_SIMP_TAC std_ss [] 397QED 398 399 400val _ = export_theory(); 401