1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_proof"; 2 3open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 4open lisp_typeTheory lisp_semanticsTheory lisp_evalTheory; 5 6val _ = numLib.prefer_num(); 7 8(* translating the semantics' s-expressions into implementation s-expressions *) 9 10val atom2sexp_def = Define ` 11 (atom2sexp Nil = Sym "nil") /\ 12 (atom2sexp (Number n) = Val n) /\ 13 (atom2sexp (String s) = Sym s)`; 14 15val sexpression2sexp_def = Define ` 16 (sexpression2sexp (A a) = atom2sexp a) /\ 17 (sexpression2sexp (Cons x y) = Dot (sexpression2sexp x) (sexpression2sexp y))`; 18 19val list2sexp_def = Define ` 20 (list2sexp [] = Sym "nil") /\ 21 (list2sexp (x::xs) = Dot x (list2sexp xs))`; 22 23val x2sexp_def = tDefine "x2sexp" ` 24 (x2sexp (F,xx,FunCon s) = Sym s) /\ 25 (x2sexp (F,xx,FunVar s) = Sym s) /\ 26 (x2sexp (F,xx,Lambda vs x) = 27 list2sexp [Sym "lambda"; list2sexp (MAP Sym vs); x2sexp (T,x,FunVar "nil")]) /\ 28 (x2sexp (F,xx,Label l f) = list2sexp [Sym "label"; Sym l; x2sexp (F,Var "nil",f)]) /\ 29 (x2sexp (T,Con y,yy) = list2sexp [Sym "quote"; sexpression2sexp y]) /\ 30 (x2sexp (T,Var v,yy) = Sym v) /\ 31 (x2sexp (T,App f xs,yy) = list2sexp (x2sexp (F,Var "nil",f) :: MAP (\x. x2sexp (T,x,FunVar "nil")) xs)) /\ 32 (x2sexp (T,Ite cs,yy) = list2sexp (Sym "cond" :: MAP (\ (t1,t2). 33 list2sexp [x2sexp (T,t1,FunVar "nil"); x2sexp (T,t2,FunVar "nil")]) cs))` 34 (WF_REL_TAC `measure (\(x,y,z). if x then term_size y else func_size z)` 35 THEN REWRITE_TAC [CONJ_ASSOC] 36 THEN REVERSE STRIP_TAC THEN1 (REPEAT STRIP_TAC THEN DECIDE_TAC) 37 THEN REVERSE STRIP_TAC THEN1 (REPEAT STRIP_TAC THEN DECIDE_TAC) 38 THEN REVERSE STRIP_TAC THEN1 (REPEAT STRIP_TAC THEN DECIDE_TAC) 39 THEN REWRITE_TAC [GSYM CONJ_ASSOC] 40 THEN STRIP_TAC THEN1 41 (STRIP_TAC THEN Induct 42 THEN REWRITE_TAC [MEM,term_size_def] THEN REPEAT STRIP_TAC 43 THEN ASM_REWRITE_TAC [] THEN RES_TAC THEN DECIDE_TAC) 44 THEN STRIP_TAC THEN1 45 (Induct THEN (Cases ORELSE ALL_TAC) 46 THEN SIMP_TAC std_ss [MEM,term_size_def] THEN REPEAT STRIP_TAC 47 THEN ASM_REWRITE_TAC [] THEN RES_TAC THEN DECIDE_TAC) 48 THEN 49 (Induct THEN (Cases ORELSE ALL_TAC) 50 THEN SIMP_TAC std_ss [MEM,term_size_def] THEN REPEAT STRIP_TAC 51 THEN ASM_REWRITE_TAC [] THEN RES_TAC THEN DECIDE_TAC)) 52 53val x2sexp = x2sexp_def |> CONJUNCTS |> map SPEC_ALL |> LIST_CONJ 54 55val term2sexp_def = save_thm("func2sexp_def",save_thm("term2sexp_def",let 56 val term2sexp_deff = Define `term2sexp x = x2sexp (T,x,FunVar "nil")`; 57 val func2sexp_deff = Define `func2sexp y = x2sexp (F,Var "nil",y)`; 58 val th = Q.INST [`xx`|->`Var "nil"`,`yy`|->`FunVar "nil"`] x2sexp 59 val th = REWRITE_RULE [GSYM term2sexp_deff,GSYM func2sexp_deff] th 60 in th end)); 61 62val zip_yz_lemma = prove( 63 ``!xs ys zs x (stack:SExp) alist (l:num). 64 (LENGTH xs = LENGTH ys) ==> 65 ?x' alist'. zip_yz (list2sexp zs,x,list2sexp xs,list2sexp ys,stack,alist,l) = 66 (list2sexp (REVERSE (MAP (\ (x,y). Dot x y) (ZIP (xs,ys))) ++ zs),x',list2sexp [],list2sexp [],stack,alist',l)``, 67 Induct 68 THEN Cases_on `ys` THEN SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 69 THEN REWRITE_TAC [ZIP,MAP,APPEND,list2sexp_def,REVERSE_DEF] 70 THEN ONCE_REWRITE_TAC [zip_yz_def] 71 THEN REWRITE_TAC [isDot_def] THEN1 METIS_TAC [] 72 THEN SIMP_TAC std_ss [ZIP,MAP,list2sexp_def,APPEND,CAR_def,CDR_def,LET_DEF] 73 THEN REWRITE_TAC [GSYM list2sexp_def] 74 THEN REPEAT STRIP_TAC 75 THEN RES_TAC 76 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`Dot h' h::zs`,`list2sexp zs`, 77 `stack`,`l`,`list2sexp zs`]) 78 THEN ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND]) 79 80val LISP_LENGTH_def = Define ` 81 (LISP_LENGTH (Dot x y) = 1 + LISP_LENGTH y) /\ 82 (LISP_LENGTH (Val n) = 0) /\ 83 (LISP_LENGTH (Sym s) = 0)`; 84 85val lisp_length_EQ = (REWRITE_RULE [DECIDE ``n + 0 = n``] o Q.SPEC `0` o prove) ( 86 ``!n x. ?x2. !y z stack alist l. 87 lisp_length (Val n,x,y,z,stack,alist,l:num) = 88 (Val (LISP_LENGTH x + n),x2,y,z,stack,alist,l)``, 89 REVERSE (Induct_on `x`) 90 THEN ONCE_REWRITE_TAC [lisp_length_def,LISP_LENGTH_def] 91 THEN REWRITE_TAC [isDot_def,DECIDE ``(0 + n) = n``] 92 THEN1 (METIS_TAC []) THEN1 (METIS_TAC []) 93 THEN SIMP_TAC std_ss [CDR_def,LISP_ADD_def,LET_DEF] 94 THEN REWRITE_TAC [DECIDE ``1 + m + n = m + (n + 1)``] 95 THEN METIS_TAC []); 96 97val lisp_ops_thm = prove( 98 ``!exp x y zstack alist l. 99 (lisp_numberp (exp,x,y,z,stack,alist,l) = 100 (LISP_NUMBERP exp,x,y,z,stack,alist,l)) /\ 101 (lisp_symbolp (exp,x,y,z,stack,alist,l) = 102 (LISP_SYMBOLP exp,x,y,z,stack,alist,l)) /\ 103 (lisp_consp (exp,x,y,z,stack,alist,l) = 104 (LISP_CONSP exp,x,y,z,stack,alist,l)) /\ 105 (lisp_atomp (exp,x,y,z,stack,alist,l) = 106 (LISP_ATOMP exp,x,y,z,stack,alist,l)) /\ 107 (lisp_less (Val m,Val n,y,z,stack,alist,l) = 108 (LISP_LESS (Val m) (Val n),Val n,y,z,stack,alist,l))``, 109 Cases 110 THEN SIMP_TAC std_ss [LISP_SYMBOLP_def,LISP_NUMBERP_def,LISP_ATOMP_def, 111 LISP_CONSP_def,LISP_TEST_def,isSym_def,isDot_def,isVal_def,LET_DEF, 112 lisp_numberp_def,lisp_symbolp_def,lisp_atomp_def,lisp_consp_def, 113 LISP_LESS_def,getVal_def,lisp_less_def] THEN METIS_TAC []); 114 115val rev_exp_thm = prove( 116 ``!ys xs x y stack alist l. 117 rev_exp(list2sexp xs,x,y,list2sexp ys,stack,alist,l) = 118 (list2sexp (REVERSE ys ++ xs),y,y,list2sexp [],stack,alist,l)``, 119 Induct 120 THEN REWRITE_TAC [list2sexp_def] 121 THEN ONCE_REWRITE_TAC [rev_exp_def] 122 THEN SIMP_TAC std_ss [isDot_def,LET_DEF,REVERSE_DEF,APPEND] 123 THEN SIMP_TAC std_ss [CAR_def,CDR_def,GSYM APPEND_ASSOC,APPEND] 124 THEN ASM_REWRITE_TAC [GSYM list2sexp_def]); 125 126val reverse_exp_thm = prove( 127 ``!xs x y stack alist l. 128 reverse_exp(list2sexp xs,x,y,z,stack,alist,l) = 129 (list2sexp (REVERSE xs),y,y,TASK_FUNC,stack,alist,l)``, 130 SIMP_TAC std_ss [reverse_exp_def,LET_DEF,GSYM list2sexp_def, 131 rev_exp_thm,APPEND_NIL]); 132 133val LIST_LOOKUP_def = Define ` 134 (LIST_LOOKUP (x:string) [] = (FEMPTY ' x:(sexpression + func))) /\ 135 (LIST_LOOKUP x (y::ys) = if x = FST y then SND y else LIST_LOOKUP x ys)`; 136 137val iFunBind_def = 138 Define 139 `iFunBind (a:(string # (sexpression + func)) list) f fn = (f, INR fn) :: a`; 140 141val iVarBind_def = 142 Define 143 `(iVarBind a [] sl = (a : (string # (sexpression + func)) list)) /\ 144 (iVarBind a (x::xl) [] = iVarBind ((x,INL (A Nil)) :: a) xl []) /\ 145 (iVarBind a (x::xl) (s::sl) = iVarBind ((x, INL s) :: a) xl sl)`; 146 147val (iR_ev_rules,iR_ev_ind,iR_ev_cases) = 148 Hol_reln 149 `(!s a. 150 iR_ev (Con s, a) s) 151 /\ 152 (!x a. 153 MEM x (MAP FST a) /\ ISL (LIST_LOOKUP x a) ==> 154 iR_ev (Var x, a) (OUTL(LIST_LOOKUP x a))) 155 /\ 156 (!fc args a. 157 FunConSemOK fc args ==> 158 iR_ap (FunCon fc,args,a) (FunConSem fc args)) 159 /\ 160 (!fn el args s a. 161 ~(MEM (func2sexp fn) [Sym "quote"; Sym "cond"]) /\ 162 iR_evl (el,a) args /\ iR_ap (fn,args,a) s /\ (LENGTH args = LENGTH el) 163 ==> iR_ev (App fn el,a) s) 164 /\ 165 (!a. 166 iR_ev (Ite [], a) False) 167 /\ 168 (!e1 e2 el s a. 169 iR_ev (e1,a) False /\ iR_ev (Ite el,a) s 170 ==> iR_ev (Ite ((e1,e2)::el),a) s) 171 /\ 172 (!e1 e2 el s1 s a. 173 iR_ev (e1,a) s1 /\ isTrue s1 /\ iR_ev (e2,a) s 174 ==> 175 iR_ev (Ite ((e1,e2)::el),a) s) 176 /\ 177 (!x fn args s a. 178 ~(MEM (func2sexp fn) [Sym "quote"; Sym "cond"]) /\ 179 iR_ap (fn,args,iFunBind a x fn) s ==> iR_ap(Label x fn,args,a) s) 180 /\ 181 (!fv args s a. 182 fv NOTIN {"quote";"cond";"car";"cdr";"cons";"+";"-";"*";"div";"mod";"<"; 183 "equal";"atomp";"consp";"symbolp";"numberp"} /\ 184 MEM fv (MAP FST a) /\ ISR (LIST_LOOKUP fv a) /\ 185 iR_ap (OUTR(LIST_LOOKUP fv a),args,a) s ==> iR_ap (FunVar fv,args,a) s) 186 /\ 187 (!xl e args s a. 188 (LENGTH args = LENGTH xl) /\ 189 (!a2. (FILTER (\x. ~(MEM (FST x) xl)) a = FILTER (\x. ~(MEM (FST x) xl)) a2) ==> 190 iR_ev (e,iVarBind a2 xl args) s) 191 ==> iR_ap (Lambda xl e,args,a) s) 192 /\ 193 (!a. 194 iR_evl ([],a) []) 195 /\ 196 (!e el s sl a. 197 iR_ev (e,a) s /\ iR_evl (el,a) sl 198 ==> iR_evl (e::el,a) (s::sl))`; 199 200val IF_LEMMA = prove( 201 ``!b x y. (if b then x else y) = (b /\ x) \/ (~b /\ y)``, 202 Cases THEN SIMP_TAC std_ss []); 203 204val iR_ap_LEMMA = prove( 205 ``iR_ap (fn,args,a) s ==> ~(MEM (func2sexp fn) [Sym "quote"; Sym "cond"])``, 206 ONCE_REWRITE_TAC [iR_ev_cases] 207 THEN SRW_TAC [] [term2sexp_def] 208 THEN FULL_SIMP_TAC std_ss [FunConSemOK_def,IF_LEMMA] 209 THEN EVAL_TAC THEN ASM_SIMP_TAC std_ss []); 210 211val pair2sexp_def = Define ` 212 (pair2sexp (s, INL x) = Dot (Sym s) (sexpression2sexp x)) /\ 213 (pair2sexp (s, INR y) = Dot (Sym s) (func2sexp y))`; 214 215val alist2sexp_def = Define ` 216 (alist2sexp al = list2sexp (MAP pair2sexp al))`; 217 218val lisp_eval_ok_def = Define ` 219 lisp_eval_ok (exp_in,alist) exp_out = 220 !x:SExp y:SExp stack:SExp l:num. ?x':SExp y':SExp. 221 lisp_eval (term2sexp exp_in,x,y,TASK_EVAL,stack,alist2sexp alist,l) = 222 lisp_eval (sexpression2sexp exp_out,x',y',TASK_CONT,stack,alist2sexp alist,l)`; 223 224val lisp_func_ok_def = Define ` 225 lisp_func_ok (fn,args,alist) result = 226 !y:SExp stack:SExp l:num. ?x':SExp y':SExp. 227 lisp_eval (list2sexp (MAP sexpression2sexp args),func2sexp fn,y,TASK_FUNC,stack,alist2sexp alist,l) = 228 lisp_eval (sexpression2sexp result,x',y',TASK_CONT,stack,alist2sexp alist,l)`; 229 230val lookup_aux_lemma = prove( 231 ``!x a t:SExp z:SExp q:SExp. 232 MEM x (MAP FST a) ==> 233 ?q' y'. 234 (lookup_aux (Sym x,q,alist2sexp a,z,stack:SExp,t,l:num) = 235 (if ISL (LIST_LOOKUP x a) 236 then sexpression2sexp (OUTL (LIST_LOOKUP x a)) 237 else func2sexp (OUTR (LIST_LOOKUP x a)), 238 q',y',z,stack,t,l))``, 239 STRIP_TAC THEN Induct 240 THEN SIMP_TAC std_ss [MAP,MEM] 241 THEN NTAC 4 STRIP_TAC 242 THEN Cases_on `x = FST h` 243 THEN ASM_SIMP_TAC std_ss [LIST_LOOKUP_def,alist2sexp_def,MAP] 244 THEN Cases_on `h` THEN Cases_on `r` 245 THEN ONCE_REWRITE_TAC [lookup_aux_def] 246 THEN SIMP_TAC std_ss [LET_DEF,pair2sexp_def,list2sexp_def,CAR_def,CDR_def] 247 THEN FULL_SIMP_TAC std_ss [SExp_11] 248 THEN POP_ASSUM MP_TAC 249 THEN POP_ASSUM (ASSUME_TAC o Q.SPECL [`t`,`z`,`Sym q'`]) 250 THEN REPEAT STRIP_TAC 251 THEN RES_TAC 252 THEN ASM_REWRITE_TAC [GSYM alist2sexp_def] 253 THEN METIS_TAC []); 254 255val lisp_eval_hide_def = Define `lisp_eval_hide = lisp_eval`; 256 257val sexpression2sexp_11 = prove( 258 ``!u v. (sexpression2sexp u = sexpression2sexp v) = 259 (delete_Nil u = delete_Nil v)``, 260 Induct 261 THEN Cases_on `v` 262 THEN REPEAT (Cases_on `a`) 263 THEN REPEAT (Cases_on `a'`) 264 THEN REWRITE_TAC [sexpression2sexp_def,atom2sexp_def, 265 delete_Nil_def,delete_Nil_aux_def] 266 THEN SRW_TAC [] []); 267 268val LISP_EQUAL_THM = prove( 269 ``!u v. (LISP_EQUAL (sexpression2sexp u) (sexpression2sexp v) = 270 sexpression2sexp (Equal (u,v))) /\ 271 (LISP_CONSP (sexpression2sexp u) = sexpression2sexp (Consp u)) /\ 272 (LISP_ATOMP (sexpression2sexp u) = sexpression2sexp (Atomp u)) /\ 273 (LISP_SYMBOLP (sexpression2sexp u) = sexpression2sexp (Symbolp u)) /\ 274 (LISP_NUMBERP (sexpression2sexp u) = sexpression2sexp (Numberp u))``, 275 REWRITE_TAC [LISP_EQUAL_def,Equal_def,sexpression2sexp_11,True_def, 276 False_def,LISP_TEST_def,LISP_ATOMP_def,LISP_SYMBOLP_def,LISP_CONSP_def, 277 LISP_NUMBERP_def,isDot_def,isSym_def,isVal_def] 278 THEN REPEAT STRIP_TAC 279 THEN1 SRW_TAC [] [delete_Nil_def,delete_Nil_aux_def,True_def, 280 sexpression2sexp_def,atom2sexp_def,False_def] 281 THEN Cases_on `u` THEN (Cases_on `a` ORELSE ALL_TAC) 282 THEN REWRITE_TAC [isDot_def,isSym_def,isVal_def,sexpression2sexp_def, 283 atom2sexp_def,Consp_def,False_def,True_def,Atomp_def, 284 Symbolp_def,Numberp_def]); 285 286val EVAL_ARGS_LEMMA = prove( 287 ``!t h args fn a s x y xs. 288 EVERY I (MAP (\(x,y). lisp_eval_ok (x,a) y) (ZIP (h::t,args))) /\ 289 (LENGTH args = LENGTH (h::t)) /\ ~(fn = Sym "cond") ==> 290 ?x' y'. 291 lisp_eval 292 (term2sexp h,x,y,TASK_EVAL, 293 Dot (Dot (list2sexp (MAP (\x. term2sexp x) t)) (list2sexp xs)) 294 (Dot fn stack),alist2sexp a,l) = 295 lisp_eval_hide 296 (list2sexp (REVERSE xs ++ MAP sexpression2sexp args),fn,fn,TASK_FUNC,stack, 297 alist2sexp a,l)``, 298 Induct 299 THEN Cases_on `args` 300 THEN SIMP_TAC std_ss [LENGTH,ZIP,MAP,EVERY_DEF] 301 THEN REWRITE_TAC [DECIDE ``~(0 = SUC n)``] 302 THEN REPEAT STRIP_TAC 303 THENL [ 304 FULL_SIMP_TAC std_ss [lisp_eval_ok_def] 305 THEN Q.PAT_X_ASSUM `!x y stack l. ?x'. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`x`,`y`,` 306 Dot (Dot (list2sexp []) (list2sexp xs)) (Dot fn stack)`,`l`]) 307 THEN ASM_SIMP_TAC std_ss [] 308 THEN ONCE_REWRITE_TAC [lisp_eval_def] 309 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 310 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 311 THEN SIMP_TAC std_ss [SExp_distinct,lisp_cont_def] 312 THEN ASM_SIMP_TAC std_ss [LET_DEF,isDot_def,CDR_def,CAR_def,list2sexp_def] 313 THEN ASM_SIMP_TAC std_ss [LET_DEF,isDot_def,CDR_def,CAR_def,GSYM list2sexp_def] 314 THEN SIMP_TAC std_ss [reverse_exp_thm,HD,lisp_eval_hide_def] 315 THEN FULL_SIMP_TAC std_ss [LENGTH_NIL,MAP,REVERSE_DEF], 316 FULL_SIMP_TAC std_ss [lisp_eval_ok_def] 317 THEN Q.PAT_X_ASSUM `!x y stack l. ?x'. bbb` (STRIP_ASSUME_TAC o Q.SPECL [`x`,`y`,` 318 Dot (Dot (list2sexp (term2sexp h'::MAP (\x. term2sexp x) t)) (list2sexp xs)) (Dot fn stack)`,`l`]) 319 THEN ASM_SIMP_TAC std_ss [] 320 THEN ONCE_REWRITE_TAC [lisp_eval_def] 321 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 322 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 323 THEN SIMP_TAC std_ss [SExp_distinct,lisp_cont_def] 324 THEN ASM_SIMP_TAC std_ss [LET_DEF,isDot_def,CDR_def,CAR_def,list2sexp_def] 325 THEN ASM_SIMP_TAC std_ss [LET_DEF,isDot_def,CDR_def,CAR_def,GSYM list2sexp_def] 326 THEN POP_ASSUM (K ALL_TAC) 327 THEN `(LENGTH t' = LENGTH (h'::t))` by ASM_SIMP_TAC std_ss [LENGTH] 328 THEN RES_TAC THEN ONCE_REWRITE_TAC [list2sexp_def] 329 THEN ASM_REWRITE_TAC [REVERSE_DEF,GSYM APPEND_ASSOC,APPEND]]); 330 331val LISP_LENGTH_THM = prove( 332 ``!xs. LISP_LENGTH (list2sexp xs) = LENGTH xs``, 333 Induct THEN ASM_SIMP_TAC std_ss [LISP_LENGTH_def,list2sexp_def,LENGTH] 334 THEN DECIDE_TAC); 335 336val repeat_cdr_1 = prove( 337 ``repeat_cdr(exp,Val 1,y,z,stack,alist,l) = 338 (exp,Val 0,y,z,stack,CDR alist,l)``, 339 NTAC 2 (ONCE_REWRITE_TAC [repeat_cdr_def]) 340 THEN SIMP_TAC std_ss [LET_DEF,LISP_SUB_def,SExp_11]); 341 342val iVarBind_EXISTS = prove( 343 ``!a xl args. ?xs. (iVarBind a xl args = xs ++ a) /\ (LENGTH xs = LENGTH xl)``, 344 Induct_on `xl` THEN Cases_on `args` THEN REWRITE_TAC [iVarBind_def] 345 THEN1 (STRIP_TAC THEN Q.EXISTS_TAC `[]` THEN SIMP_TAC std_ss [APPEND,LENGTH]) 346 THEN1 (STRIP_TAC THEN Q.EXISTS_TAC `[]` THEN SIMP_TAC std_ss [APPEND,LENGTH]) 347 THEN REPEAT STRIP_TAC THEN1 348 (POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`(h,INL (A Nil))::a`,`[]`]) 349 THEN Q.EXISTS_TAC `SNOC (h,INL (A Nil)) xs` 350 THEN ASM_SIMP_TAC std_ss [LENGTH_SNOC,LENGTH] 351 THEN ASM_SIMP_TAC std_ss [SNOC_APPEND,GSYM APPEND_ASSOC,APPEND]) 352 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`(h',INL h)::a`,`t`]) 353 THEN Q.EXISTS_TAC `SNOC (h',INL h) xs` 354 THEN ASM_SIMP_TAC std_ss [LENGTH_SNOC,LENGTH] 355 THEN ASM_SIMP_TAC std_ss [SNOC_APPEND,GSYM APPEND_ASSOC,APPEND]); 356 357val sexpression_IF = prove( 358 ``!b. sexpression2sexp (if b then True else False) = LISP_TEST b``, 359 Cases THEN EVAL_TAC); 360 361val lisp_add_lemma = prove( 362 ``!args x m. 363 (!x. MEM x args ==> ?n. x = A (Number n)) ==> 364 ?q1 q2. 365 lisp_add (Val m,x,list2sexp (MAP sexpression2sexp args), 366 TASK_CONT,stack,alist2sexp a,l) = 367 (sexpression2sexp (FOLDL Add (A (Number m)) args),q1,q2,TASK_CONT, 368 stack,alist2sexp a,l)``, 369 Induct 370 THEN SIMP_TAC std_ss [MAP,list2sexp_def,FOLDL] 371 THEN ONCE_REWRITE_TAC [lisp_add_def] 372 THEN SIMP_TAC std_ss [LET_DEF,isDot_def,sexpression2sexp_def,atom2sexp_def] 373 THEN SIMP_TAC std_ss [CAR_def,CDR_def,MEM] 374 THEN REPEAT STRIP_TAC 375 THEN `?n. h = A (Number n)` by METIS_TAC [] 376 THEN ASM_SIMP_TAC std_ss [LISP_ADD_def,FOLDL] 377 THEN SIMP_TAC std_ss [LET_DEF,isDot_def,sexpression2sexp_def,atom2sexp_def] 378 THEN ASM_SIMP_TAC std_ss [LISP_ADD_def,FOLDL,Add_def] 379 THEN `!x. MEM x args ==> ?n. x = A (Number n)` by METIS_TAC [] 380 THEN RES_TAC THEN METIS_TAC []); 381 382val lisp_mult_lemma = prove( 383 ``!args x y m. 384 (!x. MEM x args ==> ?n. x = A (Number n)) ==> 385 ?q1 q2 q3. 386 lisp_mult (Val m,x,y,list2sexp (MAP sexpression2sexp args), 387 stack,alist2sexp a,l) = 388 (sexpression2sexp (FOLDL Mult (A (Number m)) args),q1,q2,q3, 389 stack,alist2sexp a,l)``, 390 Induct 391 THEN SIMP_TAC std_ss [MAP,list2sexp_def,FOLDL] 392 THEN ONCE_REWRITE_TAC [lisp_mult_def] 393 THEN SIMP_TAC std_ss [LET_DEF,isDot_def,sexpression2sexp_def,atom2sexp_def] 394 THEN SIMP_TAC std_ss [CAR_def,CDR_def,MEM] 395 THEN REPEAT STRIP_TAC 396 THEN `?n. h = A (Number n)` by METIS_TAC [] 397 THEN ASM_SIMP_TAC std_ss [LISP_MULT_def,FOLDL] 398 THEN SIMP_TAC std_ss [LET_DEF,isDot_def,sexpression2sexp_def,atom2sexp_def] 399 THEN ASM_SIMP_TAC std_ss [LISP_MULT_def,FOLDL,Mult_def] 400 THEN `!x. MEM x args ==> ?n. x = A (Number n)` by METIS_TAC [] 401 THEN RES_TAC THEN METIS_TAC []); 402 403val LISP_REDUCE_AUX_def = Define ` 404 (LISP_REDUCE_AUX 0 xs alist = ((alist:(string # (sexpression + func)) list),Val 0)) /\ 405 (LISP_REDUCE_AUX n xs [] = ([],Val n)) /\ 406 (LISP_REDUCE_AUX (SUC n) xs ((y,z)::ys) = 407 if MEM (Sym y) xs then LISP_REDUCE_AUX n xs ys 408 else ((y,z)::ys,Val (SUC n)))`; 409 410val LISP_REDUCE_A_def = Define ` 411 LISP_REDUCE_A (stack,xs,alist) = 412 if isDot stack /\ isVal (CAR stack) 413 then FST (LISP_REDUCE_AUX (getVal (CAR stack)) xs alist) else alist`; 414 415val LISP_REDUCE_S_def = Define ` 416 LISP_REDUCE_S (stack,xs,alist) = 417 if isDot stack /\ isVal (CAR stack) 418 then let s = (SND (LISP_REDUCE_AUX (getVal (CAR stack)) xs alist)) in 419 if s = Val 0 then CDR stack else Dot s (CDR stack) 420 else stack`; 421 422val lisp_find_in_list_thm = prove( 423 ``!xs x. 424 ?exp2 x2 y2. 425 (lisp_find_in_list (CAR (pair2sexp (q,r)),x,list2sexp xs,z,stack,alist,l) = 426 (exp2,x2,y2,z,stack,alist,l)) /\ 427 ((exp2 = Sym "nil") = ~MEM (Sym q) xs)``, 428 Induct THEN ONCE_REWRITE_TAC [lisp_find_in_list_def] 429 THEN ASM_SIMP_TAC std_ss [MEM,list2sexp_def,isDot_def,CAR_def,CDR_def,LET_DEF] 430 THEN Cases_on `r` THEN FULL_SIMP_TAC std_ss [pair2sexp_def,CAR_def] 431 THEN REPEAT STRIP_TAC THEN Cases_on `Sym q = h` 432 THEN ASM_SIMP_TAC std_ss [EVAL ``Sym "t" = Sym "nil"``]); 433 434val lisp_reduce_alist_aux_EQ = prove( 435 ``!xs alist exp x y. 436 ?exp2 x2 y2. 437 lisp_reduce_alist_aux (exp,x,y,Val n,Dot (list2sexp xs) stack,alist2sexp alist,l) = 438 let (alist,z) = LISP_REDUCE_AUX n xs alist in 439 (exp2,x2,y2,z,Dot (list2sexp xs) stack,alist2sexp alist,l)``, 440 Induct_on `n` THEN Cases_on `alist` 441 THEN SIMP_TAC std_ss [alist2sexp_def,list2sexp_def,MAP,LISP_REDUCE_AUX_def,LET_DEF] 442 THEN ONCE_REWRITE_TAC [lisp_reduce_alist_aux_def] 443 THEN SIMP_TAC std_ss [SExp_11,isDot_def,DECIDE ``~(SUC n = 0)``,CAR_def,CDR_def,LET_DEF] 444 THEN ASSUME_TAC (GEN_ALL lisp_find_in_list_thm) THEN REPEAT STRIP_TAC 445 THEN Cases_on `h` THEN helperLib.SEP_I_TAC "lisp_find_in_list" 446 THEN ASM_SIMP_TAC std_ss [LISP_REDUCE_AUX_def,LISP_SUB_def] THEN REPEAT STRIP_TAC 447 THEN Cases_on `MEM (Sym q) xs` THEN ASM_SIMP_TAC std_ss [GSYM alist2sexp_def,LET_DEF] 448 THEN FULL_SIMP_TAC std_ss [alist2sexp_def,MAP,list2sexp_def,CDR_def] 449 THEN helperLib.SEP_I_TAC "lisp_reduce_alist_aux" 450 THEN ASM_SIMP_TAC std_ss [LET_DEF] THEN METIS_TAC []); 451 452val lisp_reduce_alist_EQ = prove( 453 ``!stack exp xs x y z l alist. 454 ?x2 z2. 455 lisp_reduce_alist (exp,x,Dot (list2sexp xs) y,z,stack,alist2sexp alist,l) = 456 (exp,x2,Dot (list2sexp xs) y,z2, LISP_REDUCE_S (stack,xs,alist), 457 alist2sexp (LISP_REDUCE_A (stack,xs,alist)),l)``, 458 STRIP_TAC 459 THEN `?n s x1 x2. (stack = Sym s) \/ (stack = Dot x1 x2) \/ (stack = Val n)` by 460 (Cases_on `stack` THEN ASM_SIMP_TAC std_ss [SExp_11,SExp_distinct] THEN METIS_TAC []) 461 THEN ASM_SIMP_TAC std_ss [lisp_reduce_alist_def, 462 LISP_REDUCE_A_def,LISP_REDUCE_S_def,isDot_def,LET_DEF,CAR_def,CDR_def] 463 THEN `?n1 s1 x3 x4. (x1 = Sym s1) \/ (x1 = Dot x3 x4) \/ (x1 = Val n1)` by 464 (Cases_on `x1` THEN ASM_SIMP_TAC std_ss [SExp_11,SExp_distinct] THEN METIS_TAC []) 465 THEN FULL_SIMP_TAC std_ss [isDot_def,isSym_def,isVal_def] 466 THEN REPEAT STRIP_TAC 467 THEN STRIP_ASSUME_TAC (helperLib.MATCH_INST (SPEC_ALL lisp_reduce_alist_aux_EQ) 468 ``lisp_reduce_alist_aux 469 (Dot (list2sexp xs) (Dot (Dot exp x2) (Dot (list2sexp xs) y)), 470 Dot (Dot exp x2) (Dot (list2sexp xs) y),list2sexp xs,Val n1, 471 Dot (list2sexp xs) (Dot (Dot exp x2) (Dot (list2sexp xs) y)), 472 alist2sexp alist,l)``) 473 THEN ASM_SIMP_TAC std_ss [getVal_def,CDR_def,LET_DEF] 474 THEN Cases_on `LISP_REDUCE_AUX n1 xs alist` THEN ASM_SIMP_TAC std_ss [] 475 THEN REPEAT STRIP_TAC THEN Cases_on `r = Val 0` 476 THEN ASM_SIMP_TAC std_ss [CAR_def,CDR_def]); 477 478val FILTER_LISP_REDUCE_A = prove( 479 ``!a stack xl. 480 FILTER (\x. ~MEM (FST x) xl) (LISP_REDUCE_A (stack,MAP Sym xl,a)) = 481 FILTER (\x. ~MEM (FST x) xl) a``, 482 SIMP_TAC std_ss [LISP_REDUCE_A_def] 483 THEN Cases_on `stack` THEN ASM_SIMP_TAC std_ss [isDot_def,CAR_def] 484 THEN Cases_on `S'` THEN ASM_SIMP_TAC std_ss [isVal_def,CAR_def,getVal_def] 485 THEN Q.SPEC_TAC (`n`,`n`) THEN Induct_on `a` 486 THEN Cases_on `n` THEN ASM_SIMP_TAC std_ss [FILTER,LISP_REDUCE_AUX_def] 487 THEN Cases THEN ASM_SIMP_TAC std_ss [FILTER,LISP_REDUCE_AUX_def,MEM_MAP,SExp_11] 488 THEN REPEAT STRIP_TAC THEN Cases_on `MEM q xl` THEN ASM_SIMP_TAC std_ss [FILTER]); 489 490val repeat_cdr_thm = prove( 491 ``!n exp y z stack a l. 492 (repeat_cdr (exp,Val n,y,z,stack,a,l) = 493 (exp,Val 0,y,z,stack,FUNPOW CDR n a,l))``, 494 Induct THEN ONCE_REWRITE_TAC [repeat_cdr_def] 495 THEN REWRITE_TAC [iVarBind_def,APPEND] 496 THEN SIMP_TAC std_ss [SExp_11,DECIDE ``~(SUC n = 0)``,LET_DEF,arithmeticTheory.FUNPOW] 497 THEN ASM_SIMP_TAC std_ss [LISP_SUB_def]); 498 499val FUNPOW_CDR_iVarBind = prove( 500 ``!a xs ys. FUNPOW CDR (LENGTH xs) (alist2sexp (iVarBind a xs ys)) = alist2sexp a``, 501 REPEAT STRIP_TAC THEN STRIP_ASSUME_TAC (Q.SPECL [`a`,`xs`,`ys`] iVarBind_EXISTS) 502 THEN POP_ASSUM (ASSUME_TAC o GSYM) THEN ASM_SIMP_TAC std_ss [] 503 THEN Q.SPEC_TAC (`xs'`,`ts`) THEN REPEAT (POP_ASSUM (K ALL_TAC)) 504 THEN Induct THEN SIMP_TAC std_ss [arithmeticTheory.FUNPOW,LENGTH,APPEND] 505 THEN Cases_on `h` THEN Cases_on `r` 506 THEN FULL_SIMP_TAC std_ss [MAP,pair2sexp_def,list2sexp_def,CDR_def,alist2sexp_def]); 507 508val LISP_REDUCE_AUX_IMP = prove( 509 ``!n a x alist m. 510 (LISP_REDUCE_AUX n x a = (alist,m)) ==> 511 getVal m <= n /\ isVal m /\ 512 (alist2sexp alist = FUNPOW CDR (n - getVal m) (alist2sexp a))``, 513 Induct THEN Cases_on `a` 514 THEN SIMP_TAC std_ss [LISP_REDUCE_AUX_def,getVal_def,arithmeticTheory.FUNPOW,isVal_def] 515 THEN Cases_on `h` 516 THEN SIMP_TAC std_ss [LISP_REDUCE_AUX_def,getVal_def,arithmeticTheory.FUNPOW] 517 THEN REVERSE (Cases_on `MEM (Sym q) x`) 518 THEN ASM_SIMP_TAC std_ss [getVal_def,arithmeticTheory.FUNPOW,isVal_def] 519 THEN REPEAT STRIP_TAC THEN RES_TAC THEN1 DECIDE_TAC 520 THEN `SUC n - getVal m = SUC (n - getVal m)` by DECIDE_TAC 521 THEN ASM_SIMP_TAC std_ss [arithmeticTheory.FUNPOW] 522 THEN ASM_SIMP_TAC std_ss [alist2sexp_def,MAP,list2sexp_def,CDR_def]); 523 524val iR_ev_LEMMA = let 525 val th = iR_ev_ind 526 val th = Q.SPECL [`lisp_eval_ok`,`lisp_func_ok`, 527 `\(xl,a) yl. EVERY I (MAP (\(x,y). lisp_eval_ok (x,a) y) (ZIP (xl,yl)))`] th 528 val th = SIMP_RULE std_ss [ZIP,MAP,EVERY_DEF] th 529 val goal = (fst o dest_imp o concl) th 530 val INIT_TAC = SIMP_TAC std_ss [lisp_func_ok_def,lisp_eval_ok_def,term2sexp_def,list2sexp_def] 531 THEN REPEAT STRIP_TAC 532 THEN CONV_TAC ((QUANT_CONV o QUANT_CONV) (RAND_CONV 533 (REWRITE_CONV [GSYM lisp_eval_hide_def]))) 534 THEN ONCE_REWRITE_TAC [lisp_eval_def] 535 val th = (hd o CONJUNCTS o MP th o prove) (goal, 536 STRIP_TAC THEN1 537 (INIT_TAC 538 THEN REWRITE_TAC [isSym_def,isDot_def] 539 THEN SIMP_TAC std_ss [CAR_def,CDR_def,LET_DEF] 540 THEN SIMP_TAC std_ss [lisp_app_def,LET_DEF,CAR_def] 541 THEN REWRITE_TAC [lisp_eval_hide_def] THEN METIS_TAC []) 542 THEN STRIP_TAC THEN1 543 (INIT_TAC 544 THEN REWRITE_TAC [isSym_def,lisp_lookup_def] 545 THEN SIMP_TAC std_ss [LET_DEF] 546 THEN STRIP_ASSUME_TAC (UNDISCH (Q.SPECL [`x`,`a`,`alist2sexp a`,`TASK_CONT`,`x'`] lookup_aux_lemma)) 547 THEN ASM_REWRITE_TAC [] 548 THEN SIMP_TAC std_ss [] 549 THEN REWRITE_TAC [lisp_eval_hide_def] THEN METIS_TAC []) 550 THEN STRIP_TAC THEN1 551 (INIT_TAC 552 THEN REWRITE_TAC [EVAL ``TASK_FUNC = TASK_EVAL``] 553 THEN FULL_SIMP_TAC std_ss [IF_LEMMA,FunConSemOK_def] 554 THEN REWRITE_TAC [list2sexp_def,sexpression2sexp_def,MAP,FunConSem_def] 555 THEN REWRITE_TAC [EVAL ``EL 0 (x::xs)``,EVAL ``EL 1 (x::y::zs)``,Cdr_def,Car_def] 556 THEN ONCE_REWRITE_TAC [lisp_func_def] 557 THEN SIMP_TAC std_ss [isDot_def,CDR_def,CAR_def,LET_DEF,SExp_11,lisp_ops_thm] 558 THEN CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 559 THEN SIMP_TAC std_ss [LISP_EQUAL_THM,Add_def,Sub_def,Mult_def,Div_def,Mod_def, 560 sexpression2sexp_def,atom2sexp_def,LISP_ADD_def,LISP_SUB_def,LISP_MULT_def,LISP_DIV_def,LISP_MOD_def, 561 lisp_ops_thm,Less_def,LISP_LESS_def,getVal_def,sexpression_IF] 562 THEN IMP_RES_TAC ((Q.SPECL [`args`,`Sym "+"`,`0`] lisp_add_lemma)) 563 THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) 564 THEN IMP_RES_TAC ((Q.SPECL [`args`,`Sym "*"`,`y`,`1`] lisp_mult_lemma)) 565 THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC_ALL) 566 THEN ASM_SIMP_TAC std_ss [] 567 THEN ASM_REWRITE_TAC [lisp_eval_hide_def] THEN METIS_TAC []) 568 THEN STRIP_TAC THEN1 569 (INIT_TAC 570 THEN SIMP_TAC std_ss [LET_DEF,isSym_def,isDot_def,CDR_def,CAR_def] 571 THEN ONCE_REWRITE_TAC [lisp_app_def] 572(* THEN IMP_RES_TAC iR_ap_LEMMA *) 573 THEN FULL_SIMP_TAC std_ss [MEM] 574 THEN Cases_on `el = []` THEN1 575 (FULL_SIMP_TAC std_ss [list2sexp_def,MAP,isDot_def,LET_DEF] 576 THEN FULL_SIMP_TAC std_ss [LENGTH,LENGTH_NIL,list2sexp_def,MAP] 577 THEN Q.PAT_X_ASSUM `!x.bbb` (STRIP_ASSUME_TAC o Q.SPECL [`y`,`stack`,`l`]) 578 THEN FULL_SIMP_TAC std_ss [LENGTH,LENGTH_NIL,list2sexp_def,MAP] 579 THEN (REWRITE_TAC [lisp_eval_hide_def] THEN METIS_TAC [])) 580 THEN Cases_on `el` THEN FULL_SIMP_TAC std_ss [] 581 THEN SIMP_TAC std_ss [MAP,list2sexp_def,isDot_def,CAR_def,CDR_def,LET_DEF] 582 THEN FULL_SIMP_TAC std_ss [GSYM lisp_eval_ok_def, GSYM lisp_func_ok_def] 583 THEN IMP_RES_TAC (REWRITE_RULE [REVERSE_DEF,APPEND,list2sexp_def] (Q.INST [`xs`|->`[]`] (SPEC_ALL EVAL_ARGS_LEMMA))) 584 THEN ASM_SIMP_TAC std_ss [] 585 THEN FULL_SIMP_TAC std_ss [lisp_func_ok_def] 586 THEN METIS_TAC [lisp_eval_hide_def]) 587 THEN STRIP_TAC THEN1 588 (INIT_TAC 589 THEN SIMP_TAC std_ss [isDot_def,isSym_def,CAR_def,CDR_def,LET_DEF,MAP,list2sexp_def] 590 THEN ONCE_REWRITE_TAC [lisp_app_def] 591 THEN SIMP_TAC std_ss [SExp_11,EVAL ``"cond" = "quote"``,isDot_def] 592 THEN SIMP_TAC std_ss [False_def,sexpression2sexp_def,atom2sexp_def,lisp_eval_hide_def] 593 THEN METIS_TAC []) 594 THEN STRIP_TAC THEN1 595 (INIT_TAC 596 THEN SIMP_TAC std_ss [isDot_def,isSym_def,CAR_def,CDR_def,LET_DEF,MAP,list2sexp_def] 597 THEN ONCE_REWRITE_TAC [lisp_app_def] 598 THEN SIMP_TAC std_ss [SExp_11,EVAL ``"cond" = "quote"``,isDot_def] 599 THEN SIMP_TAC std_ss [False_def,sexpression2sexp_def,atom2sexp_def, 600 lisp_eval_hide_def,LET_DEF,CAR_def] 601 THEN POP_ASSUM MP_TAC 602 (* THEN POP_ASSUM (K ALL_TAC) *) 603 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`Dot (Sym "cond") stack`,`y`,`Dot 604 (Dot (Dot (term2sexp e1) (Dot (term2sexp e2) (Sym "nil"))) 605 (list2sexp (MAP 606 (\(t1,t2). Dot (term2sexp t1) (Dot (term2sexp t2) (Sym "nil"))) 607 el))) (Dot (Sym "cond") stack)`,`l`]) 608 THEN ASM_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) 609 THEN STRIP_TAC 610 THEN SIMP_TAC std_ss [sexpression2sexp_def,False_def,atom2sexp_def] 611 THEN CONV_TAC ((QUANT_CONV o QUANT_CONV o RATOR_CONV) (ONCE_REWRITE_CONV [lisp_eval_def])) 612 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 613 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 614 THEN SIMP_TAC std_ss [LET_DEF,SExp_distinct] 615 THEN SIMP_TAC std_ss [lisp_cont_def,LET_DEF,CDR_def,CAR_def,isDot_def] 616 THEN METIS_TAC []) 617 THEN STRIP_TAC THEN1 618 (INIT_TAC 619 THEN SIMP_TAC std_ss [isDot_def,isSym_def,CAR_def,CDR_def,LET_DEF,MAP,list2sexp_def] 620 THEN ONCE_REWRITE_TAC [lisp_app_def] 621 THEN SIMP_TAC std_ss [SExp_11,EVAL ``"cond" = "quote"``,isDot_def] 622 THEN SIMP_TAC std_ss [False_def,sexpression2sexp_def,atom2sexp_def, 623 lisp_eval_hide_def,LET_DEF,CAR_def] 624 THEN POP_ASSUM MP_TAC 625 (* THEN POP_ASSUM (K ALL_TAC) *) 626 THEN POP_ASSUM MP_TAC 627 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`Dot (Sym "cond") stack`,`y`,`Dot 628 (Dot (Dot (term2sexp e1) (Dot (term2sexp e2) (Sym "nil"))) 629 (list2sexp (MAP 630 (\(t1,t2). Dot (term2sexp t1) (Dot (term2sexp t2) (Sym "nil"))) 631 el))) (Dot (Sym "cond") stack)`,`l`]) 632 THEN ASM_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) 633 THEN SIMP_TAC std_ss [isTrue_def,False_def] 634 THEN STRIP_TAC THEN STRIP_TAC 635 THEN SIMP_TAC std_ss [sexpression2sexp_def,False_def,atom2sexp_def] 636 THEN CONV_TAC ((QUANT_CONV o QUANT_CONV o RATOR_CONV) (ONCE_REWRITE_CONV [lisp_eval_def])) 637 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 638 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 639 THEN SIMP_TAC std_ss [LET_DEF,SExp_distinct] 640 THEN SIMP_TAC std_ss [lisp_cont_def,LET_DEF,CDR_def,CAR_def,isDot_def] 641 THEN `sexpression2sexp s1 <> Sym "nil"` by 642 (Cases_on `s1` THEN (Cases_on `a'` ORELSE ALL_TAC) 643 THEN SRW_TAC [] [sexpression2sexp_def,atom2sexp_def]) 644 THEN ASM_SIMP_TAC std_ss [] THEN METIS_TAC []) 645 THEN STRIP_TAC THEN1 646 (INIT_TAC 647 THEN REWRITE_TAC [EVAL ``TASK_FUNC = TASK_EVAL``] 648 THEN ONCE_REWRITE_TAC [lisp_func_def] 649 THEN SIMP_TAC std_ss [LET_DEF,isDot_def,CAR_def,CDR_def] 650 THEN REWRITE_TAC [EVAL ``Sym "label" = Sym "lambda"``] 651 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL 652 [`Dot (Sym x) (Dot (func2sexp fn) (Sym "nil"))`,`Dot (Val 1) stack`,`l`]) 653 THEN POP_ASSUM (ASSUME_TAC o CONV_RULE (RAND_CONV 654 (ONCE_REWRITE_CONV [GSYM lisp_eval_hide_def]) THENC 655 ONCE_REWRITE_CONV [lisp_eval_def] THENC 656 REWRITE_CONV [EVAL ``TASK_FUNC = TASK_EVAL``] THENC 657 SIMP_CONV std_ss [LET_DEF,iFunBind_def,alist2sexp_def,MAP, 658 pair2sexp_def,list2sexp_def] THENC 659 REWRITE_CONV [GSYM alist2sexp_def,lisp_eval_hide_def])) 660 THEN ASM_SIMP_TAC std_ss [] 661 THEN ONCE_REWRITE_TAC [lisp_eval_def] 662 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 663 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 664 THEN SIMP_TAC std_ss [LET_DEF,SExp_distinct] 665 THEN SIMP_TAC std_ss [lisp_cont_def,LET_DEF,CDR_def,CAR_def,isDot_def,repeat_cdr_1] 666 THEN REWRITE_TAC [lisp_eval_hide_def] THEN METIS_TAC []) 667 THEN STRIP_TAC THEN1 668 (INIT_TAC 669 THEN REWRITE_TAC [EVAL ``TASK_FUNC = TASK_EVAL``] 670 THEN ONCE_REWRITE_TAC [lisp_func_def] 671 THEN SIMP_TAC std_ss [CAR_def,CDR_def,isDot_def,isSym_def,list2sexp_def,SExp_11] 672 THEN FULL_SIMP_TAC std_ss [IN_INSERT,LET_DEF,lisp_lookup_def] 673 THEN IMP_RES_TAC lookup_aux_lemma 674 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`list2sexp (MAP sexpression2sexp args)`,`alist2sexp a`,`stack`,`Sym fv`,`l`]) 675 THEN ASM_REWRITE_TAC [] 676 THEN POP_ASSUM (K ALL_TAC) 677 THEN Cases_on `LIST_LOOKUP fv a` 678 THEN FULL_SIMP_TAC std_ss [ISR,ISL] 679 THEN POP_ASSUM (K ALL_TAC) 680 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`y'`,`stack`,`l`]) 681 THEN POP_ASSUM (ASSUME_TAC o CONV_RULE (RAND_CONV 682 (ONCE_REWRITE_CONV [GSYM lisp_eval_hide_def]) THENC 683 ONCE_REWRITE_CONV [lisp_eval_def] THENC 684 REWRITE_CONV [EVAL ``TASK_FUNC = TASK_EVAL``] THENC 685 SIMP_CONV std_ss [LET_DEF,iFunBind_def,alist2sexp_def,MAP, 686 pair2sexp_def,list2sexp_def] THENC 687 REWRITE_CONV [GSYM alist2sexp_def,lisp_eval_hide_def])) 688 THEN ASM_SIMP_TAC std_ss [] 689 THEN REWRITE_TAC [lisp_eval_hide_def] THEN METIS_TAC []) 690 THEN 691 (INIT_TAC 692 THEN REWRITE_TAC [EVAL ``TASK_FUNC = TASK_EVAL``] 693 THEN ONCE_REWRITE_TAC [lisp_func_def] 694 THEN SIMP_TAC std_ss [CAR_def,CDR_def,isDot_def,isSym_def,list2sexp_def,SExp_11] 695 THEN FULL_SIMP_TAC std_ss [IN_INSERT,LET_DEF,CAR_def,CDR_def] 696 THEN ASSUME_TAC (GEN_ALL lisp_reduce_alist_EQ) 697 THEN helperLib.SEP_I_TAC "lisp_reduce_alist" 698 THEN ASM_SIMP_TAC std_ss [] 699 THEN STRIP_ASSUME_TAC (Q.SPEC `list2sexp (MAP sexpression2sexp args)` lisp_length_EQ) 700 THEN ASM_SIMP_TAC std_ss [] 701 THEN SIMP_TAC std_ss [CAR_def,CDR_def,isDot_def,isSym_def,list2sexp_def,SExp_11] 702 THEN FULL_SIMP_TAC std_ss [IN_INSERT,LET_DEF,CAR_def,CDR_def] 703 THEN REWRITE_TAC [alist2sexp_def,LISP_LENGTH_THM,LENGTH_MAP] 704 THEN Q.PAT_X_ASSUM `LENGTH args = LENGTH xl` (ASSUME_TAC o GSYM) 705 THEN SIMP_TAC std_ss [CAR_def,CDR_def,isDot_def,isSym_def,list2sexp_def,SExp_11] 706 THEN ASSUME_TAC (GEN_ALL zip_yz_lemma) THEN helperLib.SEP_I_TAC "zip_yz" 707 THEN POP_ASSUM MP_TAC THEN ASM_SIMP_TAC std_ss [LENGTH_MAP] 708 THEN REPEAT STRIP_TAC THEN ASM_SIMP_TAC std_ss [CAR_def,CDR_def] 709 THEN POP_ASSUM (K ALL_TAC) 710 THEN `!zs. list2sexp (REVERSE 711 (MAP (\(x,y). Dot x y) 712 (ZIP (MAP Sym xl,MAP sexpression2sexp args))) ++ 713 MAP pair2sexp zs) = 714 alist2sexp (iVarBind zs xl args)` by 715 (Q.PAT_X_ASSUM `LENGTH xl = LENGTH args` MP_TAC 716 THEN Q.SPEC_TAC (`xl`,`xs`) 717 THEN Q.SPEC_TAC (`args`,`ys`) 718 THEN REPEAT (POP_ASSUM (K ALL_TAC)) 719 THEN Induct 720 THEN Cases_on `xs` THEN SIMP_TAC std_ss [LENGTH,DECIDE ``~(SUC n = 0)``] 721 THEN SIMP_TAC std_ss [ZIP,MAP,REVERSE_DEF,APPEND,iVarBind_def,alist2sexp_def,GSYM APPEND_ASSOC,GSYM pair2sexp_def] 722 THEN REWRITE_TAC [GSYM MAP] 723 THEN REPEAT STRIP_TAC THEN RES_TAC 724 THEN ASM_SIMP_TAC std_ss [alist2sexp_def]) 725 THEN ASM_SIMP_TAC std_ss [] THEN POP_ASSUM (K ALL_TAC) 726 THEN POP_ASSUM MP_TAC 727 THEN POP_ASSUM (K ALL_TAC) 728 THEN STRIP_TAC 729 THEN Q.PAT_X_ASSUM `!a2.bbb` (ASSUME_TAC o 730 Q.SPEC `LISP_REDUCE_A (stack,MAP Sym xl,a)`) 731 THEN FULL_SIMP_TAC std_ss [FILTER_LISP_REDUCE_A] 732 THEN Q.PAT_X_ASSUM `!x.bbb` (STRIP_ASSUME_TAC o Q.SPECL 733 [`x'`,`list2sexp []`,`Dot (Val (LENGTH (args:sexpression list))) 734 (LISP_REDUCE_S (stack,MAP Sym xl,a))`,`l`]) 735 THEN ASM_REWRITE_TAC [] THEN POP_ASSUM (K ALL_TAC) 736 THEN ONCE_REWRITE_TAC [lisp_eval_def] 737 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 738 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 739 THEN SIMP_TAC std_ss [SExp_distinct,lisp_cont_def,LET_DEF,isDot_def,CDR_def,CAR_def] 740 THEN SIMP_TAC std_ss [repeat_cdr_thm] 741 THEN POP_ASSUM (ASSUME_TAC o GSYM) THEN ASM_SIMP_TAC std_ss [] 742 THEN ASM_SIMP_TAC std_ss [FUNPOW_CDR_iVarBind,GSYM alist2sexp_def] 743 THEN SIMP_TAC std_ss [LISP_REDUCE_S_def,LISP_REDUCE_A_def] 744 THEN REVERSE (Cases_on `isDot stack /\ isVal (CAR stack)`) 745 THEN1 (FULL_SIMP_TAC std_ss [lisp_eval_hide_def] THEN METIS_TAC []) 746 THEN FULL_SIMP_TAC std_ss [] 747 THEN `?n s2. stack = Dot (Val n) s2` by METIS_TAC [isVal_thm,isDot_thm,CAR_def] 748 THEN FULL_SIMP_TAC std_ss [CAR_def,CDR_def,getVal_def] 749 THEN ONCE_REWRITE_TAC [ONCE_REWRITE_RULE [GSYM lisp_eval_hide_def] lisp_eval_def] 750 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 751 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``,isDot_def] 752 THEN SIMP_TAC std_ss [lisp_cont_def,LET_DEF,CAR_def,CDR_def,isDot_def,repeat_cdr_thm] 753 THEN `?alist m. LISP_REDUCE_AUX n (MAP Sym xl) a = (alist,m)` by METIS_TAC [pairTheory.PAIR] 754 THEN ASM_SIMP_TAC std_ss [] 755 THEN IMP_RES_TAC LISP_REDUCE_AUX_IMP 756 THEN Cases_on `m = Val 0` THEN ASM_SIMP_TAC std_ss [getVal_def] 757 THEN1 METIS_TAC [lisp_eval_hide_def] 758 THEN ONCE_REWRITE_TAC [lisp_eval_def] 759 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 760 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``,isDot_def] 761 THEN SIMP_TAC std_ss [lisp_cont_def,LET_DEF,CAR_def,CDR_def,isDot_def,repeat_cdr_thm] 762 THEN `?i. m = Val i` by METIS_TAC [isVal_thm] 763 THEN FULL_SIMP_TAC std_ss [SExp_11,isDot_def,repeat_cdr_thm,getVal_def] 764 THEN `i + (n - i) = n` by DECIDE_TAC 765 THEN FULL_SIMP_TAC std_ss [GSYM arithmeticTheory.FUNPOW_ADD,lisp_eval_hide_def] 766 THEN METIS_TAC [])) 767 in th end; 768 769val fmap2list_def = Define ` 770 fmap2list f = MAP (\x. (x,f ' x)) (SET_TO_LIST (FDOM f))`; 771 772val list2fmap_def = Define ` 773 (list2fmap [] = FEMPTY) /\ 774 (list2fmap ((a,x)::xs) = (list2fmap xs) |+ (a,x))`; 775 776val FDOM_list2sexp = prove( 777 ``!xs x. x IN (FDOM (list2fmap xs)) = MEM x (MAP FST xs)``, 778 Induct THEN (Cases_on `h` ORELSE ALL_TAC) 779 THEN REWRITE_TAC [list2fmap_def,FDOM_FEMPTY,NOT_IN_EMPTY,MAP,MEM] 780 THEN ASM_SIMP_TAC std_ss [FDOM_FUPDATE,IN_INSERT]); 781 782val FDOM_fmap2list_list2fmap = prove( 783 ``!f. FDOM (list2fmap (fmap2list f)) = FDOM f``, 784 REWRITE_TAC [FDOM_list2sexp,EXTENSION] 785 THEN SIMP_TAC std_ss [fmap2list_def] 786 THEN SIMP_TAC std_ss [MEM_MAP,fmap2list_def,MEM_SET_TO_LIST,FDOM_FINITE] 787 THEN METIS_TAC [pairTheory.FST]); 788 789val list2fmap_fmap2list = prove( 790 ``!f:('a |-> 'b). list2fmap (fmap2list f) = f``, 791 REWRITE_TAC [fmap_EXT] 792 THEN REWRITE_TAC [FDOM_fmap2list_list2fmap,EXTENSION] 793 THEN REWRITE_TAC [fmap2list_def] 794 THEN STRIP_TAC 795 THEN `FINITE (FDOM f)` by REWRITE_TAC [FDOM_FINITE] 796 THEN POP_ASSUM MP_TAC 797 THEN Q.SPEC_TAC (`FDOM f`,`d`) 798 THEN Induct_on `CARD d` THEN STRIP_TAC 799 THEN1 METIS_TAC [CARD_EQ_0,NOT_IN_EMPTY] 800 THEN Cases_on `d = {}` THEN ASM_SIMP_TAC std_ss [CARD_EMPTY,numTheory.NOT_SUC] 801 THEN IMP_RES_TAC CHOICE_INSERT_REST 802 THEN REPEAT STRIP_TAC 803 THEN IMP_RES_TAC SET_TO_LIST_THM 804 THEN ASM_SIMP_TAC std_ss [MAP,list2fmap_def,FAPPLY_FUPDATE_THM] 805 THEN Cases_on `x = CHOICE d` THEN ASM_SIMP_TAC std_ss [] 806 THEN `FINITE (REST d)` by METIS_TAC [FINITE_INSERT] 807 THEN `v = CARD (REST d)` by ( 808 `SUC v = SUC (CARD (REST d))` by METIS_TAC [CARD_INSERT,CHOICE_NOT_IN_REST] 809 THEN FULL_SIMP_TAC std_ss []) 810 THEN RES_TAC THEN METIS_TAC [IN_INSERT]); 811 812val list2fmap_APPLY = prove( 813 ``!xs x. list2fmap xs ' x = LIST_LOOKUP x xs``, 814 Induct THEN (Cases_on `h` ORELSE ALL_TAC) 815 THEN REWRITE_TAC [list2fmap_def,LIST_LOOKUP_def] 816 THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM]); 817 818val LIST_LOOKUP_INTRO = prove( 819 ``!x a. a ' x = LIST_LOOKUP x (fmap2list a)``, 820 METIS_TAC [list2fmap_fmap2list,list2fmap_APPLY]); 821 822val iR_PERM_def = Define ` 823 iR_PERM x y = (list2fmap x = list2fmap y)`; 824 825val iR_PERM_EQ = prove( 826 ``!xs a. iR_PERM xs (fmap2list a) = (a = list2fmap xs)``, 827 METIS_TAC [iR_PERM_def,list2fmap_fmap2list]); 828 829val LIST_LOOKUP_fmap2list_list2fmap = prove( 830 ``!xs x. LIST_LOOKUP x (fmap2list (list2fmap xs)) = 831 LIST_LOOKUP x xs``, 832 REWRITE_TAC [GSYM LIST_LOOKUP_INTRO] 833 THEN Induct THEN (Cases_on `h` ORELSE ALL_TAC) 834 THEN REWRITE_TAC [list2fmap_def,LIST_LOOKUP_def] 835 THEN ASM_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM]); 836 837val FILTER_T = prove( 838 ``!xs. FILTER (\x. T) xs = xs``, 839 Induct THEN SRW_TAC [] []); 840 841val list2fmap_iVarBind = prove( 842 ``!xs ys zs. list2fmap (iVarBind xs ys zs) = VarBind (list2fmap xs) ys zs``, 843 Induct_on `ys` THEN SIMP_TAC std_ss [iVarBind_def,VarBind_def] 844 THEN Cases_on `zs` THEN ASM_SIMP_TAC std_ss [iVarBind_def,VarBind_def,list2fmap_def]); 845 846val VarBind_EQ = prove( 847 ``!xs ys f1 f2. 848 (DRESTRICT f1 (COMPL (LIST_TO_SET xs)) = 849 DRESTRICT f2 (COMPL (LIST_TO_SET xs))) ==> 850 (VarBind f1 xs ys = VarBind f2 xs ys)``, 851 Induct THEN SIMP_TAC std_ss [VarBind_def,MEM,LIST_TO_SET_THM] 852 THEN1 SRW_TAC [] [DRESTRICT_UNIV] THEN Cases_on `ys` 853 THEN SIMP_TAC std_ss [VarBind_def,MEM,LIST_TO_SET_THM] 854 THEN REPEAT STRIP_TAC THEN Q.PAT_X_ASSUM `!ys. bbb` MATCH_MP_TAC 855 THEN FULL_SIMP_TAC std_ss [GSYM fmap_EQ_THM,DRESTRICT_DEF,IN_INTER,IN_COMPL,IN_INSERT,EXTENSION,FDOM_FUPDATE,FAPPLY_FUPDATE_THM] 856 THEN METIS_TAC []); 857 858val DRESTRICT_list2fmap = prove( 859 ``!xs ys. DRESTRICT (list2fmap xs) (COMPL (set ys)) = 860 list2fmap (FILTER (\x. ~MEM (FST x) ys) xs)``, 861 Induct THEN SIMP_TAC std_ss [list2fmap_def,FILTER,DRESTRICT_FEMPTY] 862 THEN Cases THEN SIMP_TAC std_ss [list2fmap_def,DRESTRICT_FUPDATE] 863 THEN ASM_SIMP_TAC std_ss [IN_COMPL] 864 THEN Cases_on `MEM q ys` THEN ASM_SIMP_TAC std_ss [list2fmap_def]); 865 866val R_ev_LEMMA = let 867 val th = Q.SPECL [`\(e,a) s. !xs. iR_PERM xs (fmap2list a) ==> iR_ev (e,xs) s`, 868 `\(fn,args,a) s. !xs. iR_PERM xs (fmap2list a) ==> iR_ap (fn,args,xs) s`, 869 `\(xl,a) yl. !xs. iR_PERM xs (fmap2list a) ==> iR_evl (xl,xs) yl`] R_ev_ind 870 val th = SIMP_RULE std_ss [ZIP,MAP,EVERY_DEF] th 871 val goal = (fst o dest_imp o concl) th 872 val th = (hd o CONJUNCTS o MP th o prove) (goal, 873 REPEAT STRIP_TAC THEN REWRITE_TAC [iR_ev_rules] 874 THEN IMP_RES_TAC iR_ev_rules THEN ASM_SIMP_TAC std_ss [] 875 THEN FULL_SIMP_TAC std_ss [MEM,IN_INSERT,NOT_IN_EMPTY] 876 THEN REPEAT (Q.PAT_X_ASSUM `T` (K ALL_TAC)) 877 THEN RES_TAC 878 THEN1 879 (FULL_SIMP_TAC std_ss [LIST_LOOKUP_INTRO,iR_PERM_EQ] 880 THEN FULL_SIMP_TAC bool_ss [LIST_LOOKUP_fmap2list_list2fmap] 881 THEN MATCH_MP_TAC (el 2 (CONJUNCTS iR_ev_rules)) 882 THEN ASM_SIMP_TAC std_ss [GSYM FDOM_list2sexp]) 883 THEN1 (METIS_TAC [iR_ev_rules,iR_ap_LEMMA]) 884 THEN1 885 (MATCH_MP_TAC (el 6 (CONJUNCTS iR_ev_rules)) THEN ASM_SIMP_TAC std_ss []) 886 THEN1 887 (MATCH_MP_TAC (el 8 (CONJUNCTS iR_ev_rules)) THEN ASM_SIMP_TAC std_ss [] 888 THEN MATCH_MP_TAC (METIS_PROVE [] ``((c ==> b) /\ c) ==> (b /\ c)``) 889 THEN STRIP_TAC THEN1 METIS_TAC [iR_ap_LEMMA] 890 THEN Q.PAT_X_ASSUM `!xs.bbb` MATCH_MP_TAC 891 THEN FULL_SIMP_TAC std_ss [iR_PERM_def,list2fmap_fmap2list] 892 THEN ASM_SIMP_TAC std_ss [FunBind_def,iFunBind_def,list2fmap_def]) 893 THEN1 894 (MATCH_MP_TAC (el 9 (CONJUNCTS iR_ev_rules)) 895 THEN FULL_SIMP_TAC std_ss [IN_INSERT,NOT_IN_EMPTY] 896 THEN FULL_SIMP_TAC std_ss [LIST_LOOKUP_INTRO,iR_PERM_EQ] 897 THEN FULL_SIMP_TAC bool_ss [LIST_LOOKUP_fmap2list_list2fmap] 898 THEN FULL_SIMP_TAC std_ss [FDOM_list2sexp]) 899 THEN1 900 (MATCH_MP_TAC (el 10 (CONJUNCTS iR_ev_rules)) THEN ASM_SIMP_TAC std_ss [] 901 THEN REPEAT STRIP_TAC THEN Q.PAT_X_ASSUM `!xs. bbb ==> bbbb` MATCH_MP_TAC 902 THEN FULL_SIMP_TAC std_ss [iR_PERM_EQ,list2fmap_iVarBind] 903 THEN MATCH_MP_TAC VarBind_EQ THEN POP_ASSUM MP_TAC 904 THEN ASM_SIMP_TAC std_ss [DRESTRICT_list2fmap]) 905 THEN METIS_TAC [iR_ev_rules]) 906 in th end; 907 908val R_lisp_eval_ok = prove( 909 ``!e a s. R_ev (e,a) s ==> lisp_eval_ok (e,fmap2list a) s``, 910 REPEAT STRIP_TAC 911 THEN IMP_RES_TAC R_ev_LEMMA 912 THEN FULL_SIMP_TAC std_ss [] 913 THEN `iR_PERM (fmap2list a) (fmap2list a)` by 914 REWRITE_TAC [iR_PERM_def] 915 THEN RES_TAC THEN METIS_TAC [iR_ev_LEMMA]); 916 917val LISP_EVAL_def = Define ` 918 LISP_EVAL (exp,alist,limit) = 919 FST (lisp_eval (exp,Sym "nil",Sym "nil",Sym "nil",Sym "nil",alist,limit))`; 920 921val LISP_EVAL_CORRECT = store_thm("LISP_EVAL_CORRECT", 922 ``!exp alist result l. 923 R_ev (exp,alist) result ==> 924 (LISP_EVAL (term2sexp exp, alist2sexp (fmap2list alist),l) = 925 sexpression2sexp result)``, 926 REPEAT STRIP_TAC 927 THEN IMP_RES_TAC R_lisp_eval_ok 928 THEN FULL_SIMP_TAC std_ss [lisp_eval_ok_def,LISP_EVAL_def] 929 THEN REWRITE_TAC [GSYM TASK_EVAL_def] 930 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`TASK_EVAL`,`TASK_EVAL`,`TASK_EVAL`,`l`]) 931 THEN ASM_SIMP_TAC std_ss [] 932 THEN ONCE_REWRITE_TAC [lisp_eval_def] 933 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 934 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 935 THEN REWRITE_TAC [TASK_EVAL_def,isDot_def]); 936 937val LISP_EVAL_LIMIT_CORRECT = store_thm("LISP_EVAL_LIMIT_CORRECT", 938 ``!exp alist result l. 939 R_ev (exp,alist) result ==> 940 ((SND o SND o SND o SND o SND o SND) 941 (lisp_eval (term2sexp exp, Sym "nil", Sym "nil", Sym "nil", 942 Sym "nil", alist2sexp (fmap2list alist),l)) = l)``, 943 REPEAT STRIP_TAC 944 THEN IMP_RES_TAC R_lisp_eval_ok 945 THEN FULL_SIMP_TAC std_ss [lisp_eval_ok_def,LISP_EVAL_def] 946 THEN REWRITE_TAC [GSYM TASK_EVAL_def] 947 THEN POP_ASSUM (STRIP_ASSUME_TAC o Q.SPECL [`TASK_EVAL`,`TASK_EVAL`,`TASK_EVAL`,`l`]) 948 THEN ASM_SIMP_TAC std_ss [] 949 THEN ONCE_REWRITE_TAC [lisp_eval_def] 950 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_FUNC``] 951 THEN REWRITE_TAC [EVAL ``TASK_CONT = TASK_EVAL``] 952 THEN REWRITE_TAC [TASK_EVAL_def,isDot_def]); 953 954val _ = export_theory(); 955