1open HolKernel boolLib bossLib Parse; val _ = new_theory "milawa_exec"; 2 3open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 4open optionTheory arithmeticTheory relationTheory combinTheory; 5 6open lisp_sexpTheory lisp_semanticsTheory; 7open milawa_logicTheory milawa_defsTheory; 8 9infix \\ 10val op \\ = op THEN; 11 12 13(* We define an intermediate language MR_ev -- a language which is 14 very much like the runtime's specification R_ev. The difference is 15 that MR_ev is deterministic, functions that are simply just Error 16 are given a semantics from the logic's context ctxt. 17 18 We prove three important properties in this file: 19 - any evlaution in MR is also valid in the runtime 20 MR_ev ==> R_ev 21 - macro expansion does not change the evalaution result 22 MR_ev (term2term x,...) ==> MR_ev (x,...) 23 - any evaluation inside the logic can also be done in MR 24 M_ev ==> MR_ev 25 26*) 27 28val (MR_ev_rules,MR_ev_ind,MR_ev_cases) = Hol_reln ` 29 (!s a fns ok. 30 MR_ev (Const s,a,ctxt:context_type,fns,ok) (s,ok)) 31 /\ 32 (!x (a: string |-> SExp) fns ok. 33 x IN FDOM a ==> 34 MR_ev (Var x,a,ctxt,fns,ok) (FAPPLY a x,ok)) 35 /\ 36 (!a fns ok s ok1. 37 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==> 38 MR_ev (Or [],a,ctxt,fns,ok) (s,ok1)) 39 /\ 40 (!a fns s1 t ts ok. 41 MR_ev (t,a,ctxt,fns,ok) (s1,ok1) /\ isTrue s1 ==> 42 MR_ev (Or (t::ts),a,ctxt,fns,ok) (s1,ok1)) 43 /\ 44 (!a fns s1 s2 t ts ok ok2. 45 MR_ev (t,a,ctxt,fns,ok) (s1,ok1) /\ ~(isTrue s1) /\ 46 MR_ev (Or ts,a,ctxt,fns,ok1) (s2,ok2) ==> 47 MR_ev (Or (t::ts),a,ctxt,fns,ok) (s2,ok2)) 48 /\ 49 (!e1 e2 e3 s1 s a ok1 ok2. 50 MR_ev (e1,a,ctxt,fns,ok) (s1,ok1) /\ ~isTrue s1 /\ 51 MR_ev (e3,a,ctxt,fns,ok1) (s,ok2) 52 ==> 53 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2)) 54 /\ 55 (!e1 e2 e3 s1 s a ok1 ok2. 56 MR_ev (e1,a,ctxt,fns,ok) (s1,ok1) /\ isTrue s1 /\ 57 MR_ev (e2,a,ctxt,fns,ok1) (s,ok2) 58 ==> 59 MR_ev (If e1 e2 e3,a,ctxt,fns,ok) (s,ok2)) 60 /\ 61 (!e xs ys fns a ok1 ok2. 62 MR_evl (ys,a,ctxt,fns,ok) (sl,ok1) /\ (LENGTH xs = LENGTH ys) /\ 63 MR_ev (e,FUNION (VarBind xs sl) a,ctxt,fns,ok1) (x,ok2) 64 ==> 65 MR_ev (LamApp xs e ys,a,ctxt,fns,ok) (x,ok2)) 66 /\ 67 (!el args a fc fns x ok1 ok2. 68 MR_evl (el,a,ctxt,fns,ok) (args,ok1) /\ 69 MR_ap (fc,args,a,ctxt,fns,ok1) (x,ok2) 70 ==> 71 MR_ev (App fc el,a,ctxt,fns,ok) (x,ok2)) 72 /\ 73 (!fc args a fns f. 74 (EVAL_DATA_OP fc = (f,LENGTH args)) 75 ==> 76 MR_ap (PrimitiveFun fc,args,a,ctxt,fns,ok) (f args,ok)) 77 /\ 78 (!args a fc fns params exp x ok2. 79 ~MEM fc ["NOT";"RANK";"ORDP";"ORD<"] /\ 80 fc IN FDOM fns /\ ~(?xs. exp = App Error xs) /\ 81 (fns ' fc = (params,exp)) /\ (LENGTH params = LENGTH args) /\ 82 MR_ev (exp,VarBind params args,ctxt,fns,ok) (x,ok2) 83 ==> 84 MR_ap (Fun fc,args,a,ctxt,fns,ok) (x,ok2)) 85 /\ 86 (!args a fc fns params x. 87 ~MEM fc ["NOT";"RANK";"ORDP";"ORD<"] /\ 88 (LENGTH params = LENGTH args) /\ 89 fc IN FDOM fns /\ (fns ' fc = (params,App Error [Const x])) /\ 90 fc IN FDOM ctxt /\ (ctxt ' fc = (params,body,sem)) 91 ==> 92 MR_ap (Fun fc,args,a,ctxt,fns,ok) (sem args,F)) 93 /\ 94 (!x a ctxt fns ok. 95 MR_ap (Fun "NOT",[x],a,ctxt,fns,ok) (not x,ok)) 96 /\ 97 (!x a ctxt fns ok. 98 MR_ap (Fun "RANK",[x],a,ctxt,fns,ok) (rank x,ok)) 99 /\ 100 (!x a ctxt fns ok. 101 MR_ap (Fun "ORDP",[x],a,ctxt,fns,ok) (ordp x,ok)) 102 /\ 103 (!x y a ctxt fns ok. 104 MR_ap (Fun "ORD<",[x;y],a,ctxt,fns,ok) (ord_ x y,ok)) 105 /\ 106 (!args params a fname fns x ok2. 107 fname IN FDOM fns /\ 108 (fns ' fname = (params,exp)) /\ (LENGTH params = LENGTH args) /\ 109 MR_ev (exp,VarBind params args,ctxt,fns,ok) (x,ok2) 110 ==> 111 MR_ap (Funcall,Sym fname::args,a,ctxt,fns,ok) (x,ok2)) 112 /\ 113 (!a. 114 MR_evl ([],a,ctxt,fns,ok) ([],ok)) 115 /\ 116 (!e el s sl a ok1 ok2. 117 MR_ev (e,a,ctxt,fns,ok) (s,ok1) /\ 118 MR_evl (el,a,ctxt,fns,ok1) (sl,ok2) 119 ==> 120 MR_evl (e::el,a,ctxt,fns,ok) (s::sl,ok2)) 121 122 /\ (* semantics of macros below *) 123 124 (!e a fns s ok1. 125 MR_ev (App (PrimitiveFun opCAR) [e],a,ctxt,fns,ok) (s,ok1) ==> 126 MR_ev (First e,a,ctxt,fns,ok) (s,ok1)) 127 /\ 128 (!e a fns s ok1. 129 MR_ev (First (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==> 130 MR_ev (Second e,a,ctxt,fns,ok) (s,ok1)) 131 /\ 132 (!e a fns s ok1. 133 MR_ev (Second (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==> 134 MR_ev (Third e,a,ctxt,fns,ok) (s,ok1)) 135 /\ 136 (!e a fns s ok1. 137 MR_ev (Third (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==> 138 MR_ev (Fourth e,a,ctxt,fns,ok) (s,ok1)) 139 /\ 140 (!e a fns s ok1. 141 MR_ev (Fourth (App (PrimitiveFun opCDR) [e]),a,ctxt,fns,ok) (s,ok1) ==> 142 MR_ev (Fifth e,a,ctxt,fns,ok) (s,ok1)) 143 /\ 144 (!zs x a fns s ok1. 145 MR_ev (LamApp (MAP FST zs) x (MAP SND zs),a,ctxt,fns,ok) (s,ok1) ==> 146 MR_ev (Let zs x,a,ctxt,fns,ok) (s,ok1)) 147 /\ 148 (!x a fns s ok1. 149 MR_ev (x,a,ctxt,fns,ok) (s,ok1) ==> 150 MR_ev (LetStar [] x,a,ctxt,fns,ok) (s,ok1)) 151 /\ 152 (!z zs x a fns s ok1. 153 MR_ev (Let [z] (LetStar zs x),a,ctxt,fns,ok) (s,ok1) ==> 154 MR_ev (LetStar (z::zs) x,a,ctxt,fns,ok) (s,ok1)) 155 /\ 156 (!a fns s ok1. 157 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==> 158 MR_ev (Cond [],a,ctxt,fns,ok) (s,ok1)) 159 /\ 160 (!x1 x2 qs a fns s ok1. 161 MR_ev (If x1 x2 (Cond qs),a,ctxt,fns,ok) (s,ok1) ==> 162 MR_ev (Cond ((x1,x2)::qs),a,ctxt,fns,ok) (s,ok1)) 163 /\ 164 (!a fns s ok1. 165 MR_ev (Const (Sym "T"),a,ctxt,fns,ok) (s,ok1) ==> 166 MR_ev (And [],a,ctxt,fns,ok) (s,ok1)) 167 /\ 168 (!a fns s ok1. 169 MR_ev (Const (Sym "NIL"),a,ctxt,fns,ok) (s,ok1) ==> 170 MR_ev (List [],a,ctxt,fns,ok) (s,ok1)) 171 /\ 172 (!a fns s ok1. 173 MR_ev (t,a,ctxt,fns,ok) (s,ok1) ==> 174 MR_ev (And [t],a,ctxt,fns,ok) (s,ok1)) 175 /\ 176 (!a fns s ok1. 177 MR_ev (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,ctxt,fns,ok) (s,ok1) ==> 178 MR_ev (And (t1::t2::ts),a,ctxt,fns,ok) (s,ok1)) 179 /\ 180 (!a fns s ok1. 181 MR_ev (App (PrimitiveFun opCONS) [t;List ts],a,ctxt,fns,ok) (s,ok1) ==> 182 MR_ev (List (t::ts),a,ctxt,fns,ok) (s,ok1)) 183 /\ 184 (!fname ps body a fns s ok1. 185 MR_ev (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,ctxt,fns,ok) (s,ok1) ==> 186 MR_ev (Defun fname ps body,a,ctxt,fns,ok) (s,ok1))`; 187 188(* deterministic *) 189 190val PULL_IMP = save_thm("PULL_IMP",METIS_PROVE [] 191 ``!P Q. ((P ==> !x. Q x) = !x. P ==> Q x) /\ 192 (((?x. Q x) ==> P) = !x. Q x ==> P)``) 193 194val PULL_CONJ = METIS_PROVE [] 195 ``!P Q. ((P /\ !x. Q x) = !x. P /\ Q x) /\ 196 (((!x. Q x) /\ P) = !x. Q x /\ P) /\ 197 ((P /\ ?x. Q x) = ?x. P /\ Q x) /\ 198 (((?x. Q x) /\ P) = ?x. Q x /\ P)`` 199 200local 201 202val lemma = MR_ev_ind 203 |> Q.SPEC `\x y. 204 !f args a ctxt fns ok res ok1 res2 ok2 ok3. 205 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 206 MR_ap (f,args,a,ctxt,fns,ok2) (res2,ok3) ==> (res = res2)` 207 |> Q.SPEC `\x y. 208 !xs a ctxt fns ok res ok1 res2 ok2 ok3. 209 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 210 MR_evl (xs,a,ctxt,fns,ok2) (res2,ok3) ==> (res = res2)` 211 |> Q.SPEC `\x y. 212 !x1 a ctxt fns ok res ok1 res2 ok2 ok3. 213 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 214 MR_ev (x1,a,ctxt,fns,ok2) (res2,ok3) ==> (res = res2)` 215 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP])) 216 217in 218 219val MR_ev_11 = store_thm("MR_ev_11", 220 lemma |> concl |> dest_comb |> snd, 221 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC 222 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 223 \\ FULL_SIMP_TAC std_ss [] 224 \\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [MR_ev_cases] 225 \\ ASM_SIMP_TAC (srw_ss()) [] 226 \\ REPEAT STRIP_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 227 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ FULL_SIMP_TAC std_ss [MEM]); 228 229end 230 231local 232 233val lemma = MR_ev_ind 234 |> Q.SPEC `\x y. 235 !f args a ctxt fns ok res ok1 res2 ok2 ok3. 236 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 237 MR_ap (f,args,a,ctxt,fns,ok) (res2,ok2) ==> (res = res2) /\ (ok1 = ok2)` 238 |> Q.SPEC `\x y. 239 !xs a ctxt fns ok res ok1 res2 ok2 ok3. 240 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 241 MR_evl (xs,a,ctxt,fns,ok) (res2,ok2) ==> (res = res2) /\ (ok1 = ok2)` 242 |> Q.SPEC `\x y. 243 !x1 a ctxt fns ok res ok1 res2 ok2 ok3. 244 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 245 MR_ev (x1,a,ctxt,fns,ok) (res2,ok2) ==> (res = res2) /\ (ok1 = ok2)` 246 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP])) 247 248in 249 250val MR_ev_11_ALL = store_thm("MR_ev_11_ALL", 251 lemma |> concl |> dest_comb |> snd, 252 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC 253 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 254 \\ FULL_SIMP_TAC std_ss [] 255 \\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [MR_ev_cases] 256 \\ ASM_SIMP_TAC (srw_ss()) [] 257 \\ REPEAT STRIP_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 258 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ FULL_SIMP_TAC std_ss [MEM] 259 \\ NTAC 2 (POP_ASSUM MP_TAC) 260 \\ ONCE_REWRITE_TAC [MR_ev_cases] 261 \\ ASM_SIMP_TAC (srw_ss()) []); 262 263end 264 265local 266 267val lemma = MR_ev_ind 268 |> Q.SPEC `\x y. 269 !f args a ctxt fns ok res ok1. 270 (x = (f,args,a,ctxt \\ name,fns,ok)) /\ (y = (res,ok1)) ==> 271 MR_ap (f,args,a,ctxt,fns,ok) (res,ok1)` 272 |> Q.SPEC `\x y. 273 !xs a ctxt fns ok res ok1 res2 ok2 ok3. 274 (x = (xs,a,ctxt \\ name,fns,ok)) /\ (y = (res,ok1)) ==> 275 MR_evl (xs,a,ctxt,fns,ok) (res,ok1)` 276 |> Q.SPEC `\x y. 277 !x1 a ctxt fns ok res ok1 res2 ok2 ok3. 278 (x = (x1,a,ctxt \\ name,fns,ok)) /\ (y = (res,ok1)) ==> 279 MR_ev (x1,a,ctxt,fns,ok) (res,ok1)` 280 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP])) 281 282in 283 284val MR_ev_CTXT = store_thm("MR_ev_CTXT", 285 lemma |> concl |> dest_comb |> snd, 286 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC 287 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 288 \\ ONCE_REWRITE_TAC [MR_ev_cases] 289 \\ FULL_SIMP_TAC (srw_ss()) [] 290 \\ METIS_TAC [DOMSUB_FAPPLY_NEQ]); 291 292end 293 294val add_def_lemma = store_thm("add_def_lemma", 295 ``(FDOM (add_def k x) = FDOM k UNION {FST x}) /\ 296 (add_def k x ' n = if n IN FDOM k then k ' n else 297 if n = FST x then SND x else FEMPTY ' n)``, 298 Cases_on `x` 299 \\ ASM_SIMP_TAC std_ss [SUBMAP_DEF,add_def_def, 300 FUNION_DEF,FAPPLY_FUPDATE_THM, 301 FDOM_FUPDATE,IN_UNION,FDOM_FUPDATE, 302 FDOM_FEMPTY]); 303 304local 305 306val lemma = MR_ev_ind 307 |> Q.SPEC `\x y. 308 !f args a ctxt fns ok res ok1. 309 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==> 310 MR_ap (f,args,a,ctxt,add_def fns d,ok) (res,ok1)` 311 |> Q.SPEC `\x y. 312 !xs a ctxt fns ok res ok1 res2 ok2 ok3. 313 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==> 314 MR_evl (xs,a,ctxt,add_def fns d,ok) (res,ok1)` 315 |> Q.SPEC `\x y. 316 !x1 a ctxt fns ok res ok1 res2 ok2 ok3. 317 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==> 318 MR_ev (x1,a,ctxt,add_def fns d,ok) (res,ok1)` 319 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP])) 320 321in 322 323val MR_ev_add_def = store_thm("MR_ev_add_def", 324 lemma |> concl |> dest_comb |> snd, 325 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC 326 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 327 \\ ONCE_REWRITE_TAC [MR_ev_cases] 328 \\ FULL_SIMP_TAC (srw_ss()) [add_def_lemma] 329 \\ METIS_TAC []); 330 331end 332 333local 334 335val lemma = MR_ev_ind 336 |> Q.SPEC `\x y. 337 !f args a ctxt fns ok res ok1 z. 338 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 339 MR_ap (f,args,a,ctxt,fns,ok) z ==> (z = (res,ok1))` 340 |> Q.SPEC `\x y. 341 !xs a ctxt fns ok res ok1 z. 342 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 343 MR_evl (xs,a,ctxt,fns,ok) z ==> (z = (res,ok1))` 344 |> Q.SPEC `\x y. 345 !x1 a ctxt fns ok res ok1 z. 346 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ 347 MR_ev (x1,a,ctxt,fns,ok) z ==> (z = (res,ok1))` 348 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP])) 349 350in 351 352val MR_ev_11_FULL = store_thm("MR_ev_11_FULL", 353 lemma |> concl |> dest_comb |> snd, 354 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC 355 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 356 \\ FULL_SIMP_TAC std_ss [] 357 \\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [MR_ev_cases] 358 \\ ASM_SIMP_TAC (srw_ss()) [] 359 \\ REPEAT STRIP_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 360 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ FULL_SIMP_TAC std_ss [MEM]); 361 362end 363 364local 365 366val lemma = MR_ev_ind 367 |> Q.SPEC `\x y. 368 !f args a ctxt fns ok res ok1 z. 369 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ ok1 ==> ok` 370 |> Q.SPEC `\x y. 371 !xs a ctxt fns ok res ok1 z. 372 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ ok1 ==> ok` 373 |> Q.SPEC `\x y. 374 !x1 a ctxt fns ok res ok1 z. 375 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ ok1 ==> ok` 376 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP])) 377 378in 379 380val MR_ev_OK = store_thm("MR_ev_OK", 381 lemma |> concl |> dest_comb |> snd, 382 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []); 383 384end 385 386val MR_ev_induct = IndDefLib.derive_strong_induction(MR_ev_rules,MR_ev_ind); 387 388val MR_ap_ARB = prove( 389 ``MR_ap (fc,args,b,ctxt,fns,ok1) (x,ok2) = 390 MR_ap (fc,args,ARB,ctxt,fns,ok1) (x,ok2)``, 391 ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC std_ss []); 392 393val FDOM_VarBind = prove( 394 ``!xs ys x. (LENGTH xs = LENGTH ys) ==> 395 (x IN FDOM (VarBind xs ys) = MEM x xs)``, 396 SIMP_TAC std_ss [VarBind_def] 397 \\ ONCE_REWRITE_TAC [GSYM MEM_REVERSE,GSYM LENGTH_REVERSE] 398 \\ NTAC 3 STRIP_TAC 399 \\ Q.SPEC_TAC (`REVERSE xs`,`xs`) \\ Q.SPEC_TAC (`REVERSE ys`,`ys`) 400 \\ Induct_on `xs` \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 401 \\ ASM_SIMP_TAC (srw_ss()) [VarBindAux_def]); 402 403val MR_ap_cases = CONJUNCTS MR_ev_cases |> el 1 404val MR_evl_cases = CONJUNCTS MR_ev_cases |> el 2 405 406val MR_evl_LENGTH = prove( 407 ``!xs ys ok ok1. MR_evl (xs,a,ctxt,fns,ok) (ys,ok1) ==> (LENGTH xs = LENGTH ys)``, 408 Induct \\ Cases_on `ys` \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases,LENGTH] 409 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 410 411 412(* MR_ev ==> R_ev *) 413 414local 415 416val lemma = R_ev_ind 417 |> Q.SPEC `\x y. 418 !f args a ctxt fns ok res ok1 io q1 q2. 419 (x = (f,args,a,fns,io,ok)) /\ (y = (res,q1,q2,ok1)) /\ ok1 ==> ok` 420 |> Q.SPEC `\x y. 421 !xs a ctxt fns ok res ok1 io q1 q2. 422 (x = (xs,a,fns,io,ok)) /\ (y = (res,q1,q2,ok1)) /\ ok1 ==> ok` 423 |> Q.SPEC `\x y. 424 !x1 a ctxt fns ok res ok1 io q1 q2. 425 (x = (x1,a,fns,io,ok)) /\ (y = (res,q1,q2,ok1)) /\ ok1 ==> ok` 426 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP,AND_IMP_INTRO])) 427 428in 429 430val R_ev_ok_LEMMA = prove( 431 lemma |> concl |> dest_comb |> snd, 432 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss []) 433 |> SIMP_RULE std_ss [] 434 435end 436 437 438local 439 440val lemma = MR_ev_ind 441 |> Q.SPEC `\x y. 442 !f args a ctxt fns ok res ok1 io. 443 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ core_assum fns ==> 444 ?io1. (ok1 ==> (io1 = "")) /\ 445 R_ap (f,args,a,fns,io,ok) (res,fns,io ++ io1,ok1)` 446 |> Q.SPEC `\x y. 447 !xs a ctxt fns ok res ok1 io. 448 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ core_assum fns ==> 449 ?io1. (ok1 ==> (io1 = "")) /\ 450 R_evl (xs,a,fns,io,ok) (res,fns,io ++ io1,ok1)` 451 |> Q.SPEC `\x y. 452 !x1 a ctxt fns ok res ok1 io. 453 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) /\ core_assum fns ==> 454 ?io1. (ok1 ==> (io1 = "")) /\ 455 R_ev (x1,a,fns,io,ok) (res,fns,io ++ io1,ok1)` 456 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP,AND_IMP_INTRO])) 457 458in 459 460val MR_IMP_R = store_thm("MR_IMP_R", 461 lemma |> concl |> dest_comb |> snd, 462 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC 463 \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 464 \\ ASM_SIMP_TAC (srw_ss()) [Once R_ev_cases] 465 \\ FULL_SIMP_TAC std_ss [R_ev_not,R_ev_rank,R_ev_ordp,R_ev_ord_] 466 THEN1 METIS_TAC [APPEND_ASSOC,APPEND] 467 \\ TRY (Q.PAT_X_ASSUM `!io.bbb` MP_TAC 468 \\ Q.PAT_X_ASSUM `!io.bbb` (STRIP_ASSUME_TAC o SPEC_ALL) 469 \\ REPEAT STRIP_TAC 470 \\ Q.PAT_X_ASSUM `!io.bbb` (STRIP_ASSUME_TAC o Q.SPEC `STRCAT io io1`) 471 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 472 \\ Q.EXISTS_TAC `io1 ++ io1'` 473 \\ FULL_SIMP_TAC std_ss [APPEND_eq_NIL] 474 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 475 \\ IMP_RES_TAC R_ev_ok_LEMMA \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 476 \\ TRY (METIS_TAC []) 477 THEN1 478 (ONCE_REWRITE_TAC [R_ev_cases] \\ SIMP_TAC (srw_ss()) [] 479 \\ ONCE_REWRITE_TAC [R_ev_cases] \\ SIMP_TAC (srw_ss()) [] 480 \\ ONCE_REWRITE_TAC [R_ev_cases] \\ SIMP_TAC (srw_ss()) [] \\ METIS_TAC []) 481 \\ Q.EXISTS_TAC `""` \\ FULL_SIMP_TAC std_ss [APPEND_NIL] 482 THEN1 (IMP_RES_TAC R_ev_not \\ POP_ASSUM MP_TAC 483 \\ SIMP_TAC (srw_ss()) [Once R_ev_cases]) 484 THEN1 (IMP_RES_TAC R_ev_rank \\ POP_ASSUM MP_TAC 485 \\ SIMP_TAC (srw_ss()) [Once R_ev_cases]) 486 THEN1 (IMP_RES_TAC R_ev_ordp \\ POP_ASSUM MP_TAC 487 \\ SIMP_TAC (srw_ss()) [Once R_ev_cases]) 488 THEN1 (IMP_RES_TAC R_ev_ord_ \\ POP_ASSUM MP_TAC 489 \\ SIMP_TAC (srw_ss()) [Once R_ev_cases])); 490 491end 492 493(* definition of term2term *) 494 495val ISORT_INSERT_def = Define ` 496 (ISORT_INSERT ord x [] = [x]) /\ 497 (ISORT_INSERT ord x (y::ys) = 498 if ord y x then y::ISORT_INSERT ord x ys else x::y::ys)`; 499 500val ISORT_def = Define ` 501 (ISORT ord [] = []) /\ 502 (ISORT ord (x::xs) = ISORT_INSERT ord x (ISORT ord xs))`; 503 504val REMOVE_DUPLICATES_def = Define ` 505 (REMOVE_DUPLICATES [] = []) /\ 506 (REMOVE_DUPLICATES (x::xs) = 507 if MEM x xs then REMOVE_DUPLICATES xs else x::REMOVE_DUPLICATES xs)`; 508 509val logic_sym2prim_def = Define ` 510 logic_sym2prim s = 511 if s = "CONS" then SOME logic_CONS else 512 if s = "EQUAL" then SOME logic_EQUAL else 513 if s = "<" then SOME logic_LESS else 514 if s = "SYMBOL-<" then SOME logic_SYMBOL_LESS else 515 if s = "+" then SOME logic_ADD else 516 if s = "-" then SOME logic_SUB else 517 if s = "CONSP" then SOME logic_CONSP else 518 if s = "NATP" then SOME logic_NATP else 519 if s = "SYMBOLP" then SOME logic_SYMBOLP else 520 if s = "CAR" then SOME logic_CAR else 521 if s = "CDR" then SOME logic_CDR else 522 if s = "NOT" then SOME logic_NOT else 523 if s = "RANK" then SOME logic_RANK else 524 if s = "IF" then SOME logic_IF else 525 if s = "ORDP" then SOME logic_ORDP else 526 if s = "ORD<" then SOME logic_ORD_LESS else NONE`; 527 528val prim2p_def = Define ` 529 (prim2p opCONS = logic_CONS) /\ 530 (prim2p opEQUAL = logic_EQUAL) /\ 531 (prim2p opLESS = logic_LESS) /\ 532 (prim2p opSYMBOL_LESS = logic_SYMBOL_LESS) /\ 533 (prim2p opADD = logic_ADD) /\ 534 (prim2p opSUB = logic_SUB) /\ 535 (prim2p opCONSP = logic_CONSP) /\ 536 (prim2p opNATP = logic_NATP) /\ 537 (prim2p opSYMBOLP = logic_SYMBOLP) /\ 538 (prim2p opCAR = logic_CAR) /\ 539 (prim2p opCDR = logic_CDR)`; 540 541val func2f_def = Define ` 542 (func2f (PrimitiveFun opCONS) = mPrimitiveFun logic_CONS) /\ 543 (func2f (PrimitiveFun opEQUAL) = mPrimitiveFun logic_EQUAL) /\ 544 (func2f (PrimitiveFun opLESS) = mPrimitiveFun logic_LESS) /\ 545 (func2f (PrimitiveFun opSYMBOL_LESS) = mPrimitiveFun logic_SYMBOL_LESS) /\ 546 (func2f (PrimitiveFun opADD) = mPrimitiveFun logic_ADD) /\ 547 (func2f (PrimitiveFun opSUB) = mPrimitiveFun logic_SUB) /\ 548 (func2f (PrimitiveFun opCONSP) = mPrimitiveFun logic_CONSP) /\ 549 (func2f (PrimitiveFun opNATP) = mPrimitiveFun logic_NATP) /\ 550 (func2f (PrimitiveFun opSYMBOLP) = mPrimitiveFun logic_SYMBOLP) /\ 551 (func2f (PrimitiveFun opCAR) = mPrimitiveFun logic_CAR) /\ 552 (func2f (PrimitiveFun opCDR) = mPrimitiveFun logic_CDR) /\ 553 (func2f (Fun name) = if name = "NOT" then mPrimitiveFun logic_NOT else 554 if name = "RANK" then mPrimitiveFun logic_RANK else 555 if name = "ORDP" then mPrimitiveFun logic_ORDP else 556 if name = "ORD<" then mPrimitiveFun logic_ORD_LESS else 557 if name = "IF" then mPrimitiveFun logic_IF else 558 mFun name) /\ 559 (func2f Define = mFun "DEFINE") /\ 560 (func2f Print = mFun "PRINT") /\ 561 (func2f Error = mFun "ERROR") /\ 562 (func2f Funcall = mFun "FUNCALL")` 563 564val SUM_def = Define ` 565 (SUM [] = 0:num) /\ 566 (SUM (x::xs) = x + SUM xs)`; 567 568val MEM_term5_size = prove( 569 ``!xs a. MEM a xs ==> term_size a < term5_size xs``, 570 Induct \\ FULL_SIMP_TAC std_ss [MEM,term_size_def] \\ REPEAT STRIP_TAC 571 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 572 573val MEM_term3_size = prove( 574 ``!xs a. MEM a xs ==> term_size (FST a) < term3_size xs /\ 575 term_size (SND a) < term3_size xs``, 576 Induct \\ FULL_SIMP_TAC std_ss [MEM,term_size_def] \\ REPEAT STRIP_TAC 577 \\ Cases_on `h` \\ RES_TAC \\ FULL_SIMP_TAC std_ss [term_size_def] \\ DECIDE_TAC); 578 579val MEM_term1_size = prove( 580 ``!xs a. MEM a xs ==> term_size (SND a) <= term1_size xs``, 581 Induct \\ FULL_SIMP_TAC std_ss [MEM,term_size_def] \\ REPEAT STRIP_TAC 582 \\ Cases_on `h` \\ RES_TAC \\ FULL_SIMP_TAC std_ss [term_size_def] \\ DECIDE_TAC); 583 584val term_cost_def = tDefine "term_cost" ` 585 (term_cost (Const c) = 1) /\ 586 (term_cost (Var v) = 1) /\ 587 (term_cost (If x1 x2 x3) = 1 + term_cost x1 + term_cost x2 + term_cost x3) /\ 588 (term_cost (App f xs) = 10 + SUM (MAP term_cost xs)) /\ 589 (term_cost (LamApp vs x xs) = 1 + LENGTH xs + SUM (MAP term_cost xs) + term_cost x) /\ 590 (term_cost (First x) = 20 + term_cost x) /\ 591 (term_cost (Second x) = 30 + term_cost x) /\ 592 (term_cost (Third x) = 40 + term_cost x) /\ 593 (term_cost (Fourth x) = 50 + term_cost x) /\ 594 (term_cost (Fifth x) = 60 + term_cost x) /\ 595 (term_cost (Or xs) = 5 * SUM (MAP term_cost xs) + 5 * LENGTH xs + 5) /\ 596 (term_cost (And xs) = 5 * SUM (MAP term_cost xs) + 5 * LENGTH xs + 5) /\ 597 (term_cost (List xs) = 5 * SUM (MAP term_cost xs) + 5 * LENGTH xs + 5) /\ 598 (term_cost (Cond ys) = 5 * SUM (MAP term_cost (MAP FST ys)) + 599 5 * SUM (MAP term_cost (MAP SND ys)) + 5 * LENGTH ys + 5) /\ 600 (term_cost (Defun name vs body) = 100:num) /\ 601 (term_cost (Let zs x) = SUM (MAP term_cost (MAP SND zs)) + 602 LENGTH zs + term_cost x + 5) /\ 603 (term_cost (LetStar zs x) = 5 * SUM (MAP term_cost (MAP SND zs)) + 604 10 * LENGTH zs + term_cost x + 5)` 605 (WF_REL_TAC `measure term_size` \\ REPEAT STRIP_TAC 606 \\ FULL_SIMP_TAC std_ss [PULL_IMP,MEM_MAP] \\ IMP_RES_TAC MEM_term1_size 607 \\ IMP_RES_TAC MEM_term3_size \\ IMP_RES_TAC MEM_term5_size \\ DECIDE_TAC) 608 609val MEM_term_cost = prove( 610 ``!xs a. MEM a xs ==> term_cost a <= SUM (MAP (\a. term_cost a) xs)``, 611 Induct \\ SIMP_TAC std_ss [MEM,SUM_def,MAP] \\ REPEAT STRIP_TAC 612 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ DECIDE_TAC); 613 614val FST_MEM_term_cost = prove( 615 ``!xs a. MEM (a,b) xs ==> 616 term_cost a <= SUM (MAP (\a. term_cost a) (MAP FST xs))``, 617 Induct \\ SIMP_TAC std_ss [MEM,SUM_def,MAP] \\ REPEAT STRIP_TAC 618 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ DECIDE_TAC); 619 620val SND_MEM_term_cost = prove( 621 ``!xs a. MEM (b,a) xs ==> 622 term_cost a <= SUM (MAP (\a. term_cost a) (MAP SND xs))``, 623 Induct \\ SIMP_TAC std_ss [MEM,SUM_def,MAP] \\ REPEAT STRIP_TAC 624 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ DECIDE_TAC); 625 626val car = ``mApp (mPrimitiveFun logic_CAR)`` 627val cdr = ``mApp (mPrimitiveFun logic_CDR)`` 628val iif = ``mApp (mPrimitiveFun logic_IF)`` 629val cos = ``mApp (mPrimitiveFun logic_CONS)`` 630 631val term_vars_def = tDefine "term_vars" ` 632 (term_vars (Const c) = []) /\ 633 (term_vars (Var v) = [v]) /\ 634 (term_vars (If x1 x2 x3) = term_vars x1 ++ term_vars x2 ++ term_vars x3) /\ 635 (term_vars (App f xs) = FLAT (MAP term_vars xs)) /\ 636 (term_vars (LamApp vs x xs) = FILTER (\v. ~(MEM v vs)) (term_vars x) ++ FLAT (MAP term_vars xs)) /\ 637 (term_vars (First x) = term_vars x) /\ 638 (term_vars (Second x) = term_vars x) /\ 639 (term_vars (Third x) = term_vars x) /\ 640 (term_vars (Fourth x) = term_vars x) /\ 641 (term_vars (Fifth x) = term_vars x) /\ 642 (term_vars (Or xs) = FLAT (MAP term_vars xs)) /\ 643 (term_vars (And xs) = FLAT (MAP term_vars xs)) /\ 644 (term_vars (List xs) = FLAT (MAP term_vars xs)) /\ 645 (term_vars (Let ts x) = FILTER (\v. ~(MEM v (MAP FST ts))) (term_vars x) ++ 646 FLAT (MAP (\ (x,y). term_vars y) ts)) /\ 647 (term_vars (Cond ys) = FLAT (MAP (\ (x,y). term_vars x ++ term_vars y) ys)) /\ 648 (term_vars (LetStar [] x) = term_vars x) /\ 649 (term_vars (LetStar (t::ts) x) = FILTER (\v. ~(v = FST t)) (term_vars (LetStar ts x)) ++ term_vars (SND t)) /\ 650 (term_vars (Defun name vs body) = [])` 651 (WF_REL_TAC `measure term_cost` 652 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_term_cost 653 \\ IMP_RES_TAC SND_MEM_term_cost \\ IMP_RES_TAC FST_MEM_term_cost 654 \\ FULL_SIMP_TAC std_ss [term_cost_def,LENGTH_MAP,LENGTH,MAP,SUM_def] 655 \\ FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_CLAUSES] \\ REPEAT DECIDE_TAC); 656 657local 658 659val lemma = MR_ev_induct 660 |> Q.SPEC `\x y. 661 !f args a ctxt fns ok res ok1 z. 662 (x = (f,args,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==> 663 MR_ap (f,args,a,ctxt,fns,ok) (res,ok1)` 664 |> Q.SPEC `\x y. 665 !xs a b ctxt fns ok res ok1 z n v. 666 (x = (xs,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==> 667 (!y. MEM y (FLAT (MAP term_vars xs)) ==> 668 (y IN FDOM a = y IN FDOM b) /\ (a ' y = b ' y)) ==> 669 MR_evl (xs,b,ctxt,fns,ok) (res,ok1)` 670 |> Q.SPEC `\x y. 671 !x1 a b ctxt fns ok res ok1 z n v. 672 (x = (x1,a,ctxt,fns,ok)) /\ (y = (res,ok1)) ==> 673 (!y. MEM y (term_vars x1) ==> 674 (y IN FDOM a = y IN FDOM b) /\ (a ' y = b ' y)) ==> 675 MR_ev (x1,b,ctxt,fns,ok) (res,ok1)` 676 |> CONV_RULE (RAND_CONV (SIMP_CONV std_ss [PULL_IMP])) 677 678in 679 680val MR_ev_VARS = prove( 681 lemma |> concl |> dest_comb |> snd, 682 MATCH_MP_TAC lemma \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 683 \\ ASM_SIMP_TAC (srw_ss()) [Once MR_ev_cases,term_vars_def] 684 \\ FULL_SIMP_TAC (srw_ss()) [term_vars_def,MR_ap_ARB] 685 THEN1 (METIS_TAC []) THEN1 (METIS_TAC []) THEN1 (METIS_TAC []) 686 THEN1 687 (REPEAT STRIP_TAC 688 \\ `MR_evl (ys,b,ctxt,fns,ok) (sl,ok1)` by METIS_TAC [] 689 \\ Q.LIST_EXISTS_TAC [`sl`,`ok1`] \\ FULL_SIMP_TAC std_ss [] 690 \\ Q.PAT_X_ASSUM `!b:string |-> SExp. bbb` MATCH_MP_TAC 691 \\ FULL_SIMP_TAC std_ss [FUNION_DEF,IN_UNION] 692 \\ FULL_SIMP_TAC std_ss [MEM_FILTER,MEM_FLAT,MEM_MAP,PULL_CONJ] 693 \\ STRIP_TAC \\ STRIP_TAC 694 \\ Cases_on `y IN FDOM (VarBind xs sl)` \\ FULL_SIMP_TAC std_ss [] 695 \\ IMP_RES_TAC MR_evl_LENGTH \\ METIS_TAC [FDOM_VarBind]) 696 THEN1 (METIS_TAC []) THEN1 (METIS_TAC []) 697 THEN1 698 (POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [MAP_MAP_o,o_DEF] 699 \\ `(\x. term_vars (SND x)) = (\(x':string,y). term_vars y)` by (FULL_SIMP_TAC std_ss [FUN_EQ_THM] \\ Cases \\ FULL_SIMP_TAC std_ss []) 700 \\ FULL_SIMP_TAC std_ss [MEM_FILTER] \\ METIS_TAC []) 701 \\ Cases_on `z` \\ FULL_SIMP_TAC std_ss [] 702 \\ METIS_TAC []) |> CONJUNCT2 |> SIMP_RULE std_ss [AND_IMP_INTRO]; 703 704end 705 706val logic_prim2sym_def = Define ` 707 (logic_prim2sym logic_CONS = "CONS") /\ 708 (logic_prim2sym logic_EQUAL = "EQUAL") /\ 709 (logic_prim2sym logic_LESS = "<") /\ 710 (logic_prim2sym logic_SYMBOL_LESS = "SYMBOL-<") /\ 711 (logic_prim2sym logic_ADD = "+") /\ 712 (logic_prim2sym logic_SUB = "-") /\ 713 (logic_prim2sym logic_CONSP = "CONSP") /\ 714 (logic_prim2sym logic_NATP = "NATP") /\ 715 (logic_prim2sym logic_SYMBOLP = "SYMBOLP") /\ 716 (logic_prim2sym logic_CAR = "CAR") /\ 717 (logic_prim2sym logic_CDR = "CDR") /\ 718 (logic_prim2sym logic_NOT = "NOT") /\ 719 (logic_prim2sym logic_RANK = "RANK") /\ 720 (logic_prim2sym logic_IF = "IF") /\ 721 (logic_prim2sym logic_ORDP = "ORDP") /\ 722 (logic_prim2sym logic_ORD_LESS = "ORD<")`; 723 724val bad_names_tm = 725 ``["NIL"; "QUOTE"; "CONS"; "EQUAL"; "<"; "SYMBOL-<"; "+"; "-"; "CONSP"; 726 "NATP"; "SYMBOLP"; "CAR"; "CDR"; "NOT"; "RANK"; "IF"; "ORDP"; "ORD<"]`` 727 728val INDEX_OF_def = Define ` 729 (INDEX_OF n x [] = NONE) /\ 730 (INDEX_OF n x (y::xs) = if x = y then SOME n else INDEX_OF (n+1:num) x xs)`; 731 732val logic_func2sexp_def = Define ` 733 (logic_func2sexp (mPrimitiveFun p) = Sym (logic_prim2sym p)) /\ 734 (logic_func2sexp (mFun f) = 735 if MEM f ^bad_names_tm then Val (THE (INDEX_OF 0 f ^bad_names_tm)) else Sym f)` 736 737val t2sexp_def = tDefine "t2sexp" ` 738 (t2sexp (mConst s) = list2sexp [Sym "QUOTE"; s]) /\ 739 (t2sexp (mVar v) = Sym v) /\ 740 (t2sexp (mApp fc vs) = list2sexp (logic_func2sexp fc :: MAP t2sexp vs)) /\ 741 (t2sexp (mLamApp xs z ys) = list2sexp (list2sexp [Sym "LAMBDA"; list2sexp (MAP Sym xs); t2sexp z]::MAP t2sexp ys))` 742 (WF_REL_TAC `measure (logic_term_size)` \\ SRW_TAC [] [] \\ REPEAT DECIDE_TAC 743 THEN1 (Induct_on `vs` \\ SRW_TAC [] [MEM,logic_term_size_def] \\ RES_TAC \\ DECIDE_TAC) 744 THEN1 (Induct_on `ys` \\ SRW_TAC [] [MEM,logic_term_size_def] \\ RES_TAC \\ DECIDE_TAC)); 745 746val f2sexp_def = Define ` 747 (f2sexp (Or x y) = list2sexp [Sym "POR*"; f2sexp x; f2sexp y]) /\ 748 (f2sexp (Not x) = list2sexp [Sym "PNOT*"; f2sexp x]) /\ 749 (f2sexp (Equal t1 t2) = list2sexp [Sym "PEQUAL*"; t2sexp t1; t2sexp t2])`; 750 751val let2t_def = Define ` 752 let2t ts body = 753 let vars = MAP Sym (MAP FST ts) in 754 let terms = MAP SND ts in 755 let body_vars = (REMOVE_DUPLICATES (MAP Sym (free_vars body))) in 756 let id_vars = ISORT (\x y. getSym x <= getSym y) 757 (FILTER (\x. ~MEM x vars) body_vars) in 758 let formals = MAP getSym (id_vars ++ vars) in 759 let actuals = MAP (mVar o getSym) id_vars ++ terms in 760 mLamApp formals body actuals`; 761 762val or2t_def = Define ` 763 (or2t [] = mConst (Sym "NIL")) /\ 764 (or2t [x] = x) /\ 765 (or2t (x::y::xs) = 766 let else_term = or2t (y::xs) in 767 let cheap = (isTrue (logic_variablep (t2sexp x)) \/ 768 isTrue (logic_constantp (t2sexp x))) in 769 if cheap \/ MEM "SPECIAL-VAR-FOR-OR" (free_vars else_term) then 770 mApp (mPrimitiveFun logic_IF) [x;x;else_term] 771 else 772 let2t [("SPECIAL-VAR-FOR-OR",x)] 773 (mApp (mPrimitiveFun logic_IF) 774 [mVar "SPECIAL-VAR-FOR-OR"; mVar "SPECIAL-VAR-FOR-OR"; else_term]))` 775 776val term2t_def = tDefine "term2t" ` 777 (term2t (Const c) = mConst c) /\ 778 (term2t (Var v) = mVar v) /\ 779 (term2t (If x1 x2 x3) = ^iif [term2t x1; term2t x2; term2t x3]) /\ 780 (term2t (App f xs) = mApp (func2f f) (MAP term2t xs)) /\ 781 (term2t (LamApp vs x xs) = mLamApp vs (term2t x) (MAP term2t xs)) /\ 782 (term2t (First x) = ^car [term2t x]) /\ 783 (term2t (Second x) = ^car [^cdr [term2t x]]) /\ 784 (term2t (Third x) = ^car [^cdr [^cdr [term2t x]]]) /\ 785 (term2t (Fourth x) = ^car [^cdr [^cdr [^cdr [term2t x]]]]) /\ 786 (term2t (Fifth x) = ^car [^cdr [^cdr [^cdr [^cdr [term2t x]]]]]) /\ 787 (term2t (Or xs) = or2t (MAP term2t xs)) /\ 788 (term2t (And []) = mConst (Sym "T")) /\ 789 (term2t (And [x]) = term2t x) /\ 790 (term2t (And (x1::x2::xs)) = ^iif [term2t x1; term2t (And (x2::xs)); mConst (Sym "NIL")]) /\ 791 (term2t (List []) = mConst (Sym "NIL")) /\ 792 (term2t (List (x::xs)) = ^cos [term2t x; term2t (List xs)]) /\ 793 (term2t (Let ts x) = let2t (MAP (\ (x,y). (x,term2t y)) ts) (term2t x)) /\ 794 (term2t (Cond []) = mConst (Sym "NIL")) /\ 795 (term2t (Cond ((x,y)::rs)) = ^iif [term2t x; term2t y; term2t (Cond rs)]) /\ 796 (term2t (LetStar [] x) = term2t x) /\ 797 (term2t (LetStar ((v,x)::ts) y) = term2t (Let [(v,x)] (LetStar ts y))) /\ 798 (term2t (Defun name vs body) = 799 mApp (mFun "DEFINE") [mConst (Sym name); 800 mConst (list2sexp (MAP Sym vs)); 801 mConst body])` 802 (WF_REL_TAC `measure term_cost` 803 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_term_cost \\ IMP_RES_TAC SND_MEM_term_cost 804 \\ FULL_SIMP_TAC std_ss [term_cost_def,LENGTH_MAP,LENGTH,MAP,SUM_def] 805 \\ FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_CLAUSES] \\ REPEAT DECIDE_TAC); 806 807val MEM_logic_term_size = prove( 808 ``!xs x. MEM x xs ==> logic_term_size x < logic_term1_size xs``, 809 Induct \\ SIMP_TAC std_ss [MEM] \\ REPEAT STRIP_TAC \\ RES_TAC 810 \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC \\ DECIDE_TAC) 811 812val LENGTH_EQ_3 = prove( 813 ``(LENGTH xs = 3) = ?x1 x2 x3. xs = [x1;x2;x3]``, 814 Cases_on `xs` \\ SIMP_TAC (srw_ss()) [] 815 \\ Cases_on `t` \\ SIMP_TAC (srw_ss()) [] 816 \\ Cases_on `t'` \\ SIMP_TAC (srw_ss()) [] 817 \\ Cases_on `t` \\ SIMP_TAC (srw_ss()) [] 818 \\ DECIDE_TAC) 819 820val f2func_def = Define ` 821 (f2func (mPrimitiveFun logic_CONS) = PrimitiveFun opCONS) /\ 822 (f2func (mPrimitiveFun logic_EQUAL) = PrimitiveFun opEQUAL) /\ 823 (f2func (mPrimitiveFun logic_LESS) = PrimitiveFun opLESS) /\ 824 (f2func (mPrimitiveFun logic_SYMBOL_LESS) = PrimitiveFun opSYMBOL_LESS) /\ 825 (f2func (mPrimitiveFun logic_ADD) = PrimitiveFun opADD) /\ 826 (f2func (mPrimitiveFun logic_SUB) = PrimitiveFun opSUB) /\ 827 (f2func (mPrimitiveFun logic_CONSP) = PrimitiveFun opCONSP) /\ 828 (f2func (mPrimitiveFun logic_NATP) = PrimitiveFun opNATP) /\ 829 (f2func (mPrimitiveFun logic_SYMBOLP) = PrimitiveFun opSYMBOLP) /\ 830 (f2func (mPrimitiveFun logic_CAR) = PrimitiveFun opCAR) /\ 831 (f2func (mPrimitiveFun logic_CDR) = PrimitiveFun opCDR) /\ 832 (f2func (mPrimitiveFun logic_NOT) = Fun "NOT") /\ 833 (f2func (mPrimitiveFun logic_RANK) = Fun "RANK") /\ 834 (f2func (mPrimitiveFun logic_ORDP) = Fun "ORDP") /\ 835 (f2func (mPrimitiveFun logic_ORD_LESS) = Fun "ORD<") /\ 836 (f2func (mPrimitiveFun logic_IF) = Fun "IF") /\ 837 (f2func (mFun name) = if name = "DEFINE" then Define else 838 if name = "PRINT" then Print else 839 if name = "ERROR" then Error else 840 if name = "FUNCALL" then Funcall else 841 Fun name)` 842 843val t2term_def = tDefine "t2term" ` 844 (t2term (mConst c) = Const c) /\ 845 (t2term (mVar v) = Var v) /\ 846 (t2term (mApp f xs) = 847 if (f = mPrimitiveFun logic_IF) /\ (LENGTH xs = 3) then 848 If (t2term (EL 0 xs)) (t2term (EL 1 xs)) (t2term (EL 2 xs)) 849 else App (f2func f) (MAP t2term xs)) /\ 850 (t2term (mLamApp vs x xs) = LamApp vs (t2term x) (MAP t2term xs))` 851 (WF_REL_TAC `measure logic_term_size` \\ REPEAT STRIP_TAC 852 \\ FULL_SIMP_TAC std_ss [LENGTH_EQ_3] \\ FULL_SIMP_TAC (srw_ss()) [] 853 \\ IMP_RES_TAC MEM_logic_term_size 854 \\ EVAL_TAC \\ DECIDE_TAC); 855 856val term2term_def = Define `term2term x = t2term (term2t x)`; 857 858 859(* MR_ev (term2term x,...) ==> MR_ev (x,...) *) 860 861val func_name_ok_def = Define ` 862 func_name_ok f = 863 ~MEM f [Fun "IF"; Fun "DEFINE"; Fun "FUNCALL"; Fun "PRINT"; Fun "ERROR"]`; 864 865val f2func_func2f = prove( 866 ``!f. func_name_ok f ==> (f2func (func2f f) = f) /\ 867 ~(func2f f = mPrimitiveFun logic_IF)``, 868 Cases \\ TRY (Cases_on `l` \\ EVAL_TAC) 869 \\ EVAL_TAC \\ SRW_TAC [] [] \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss []); 870 871val funcs_ok_def = tDefine "funcs_ok" ` 872 (funcs_ok (Const c) = T) /\ 873 (funcs_ok (Var v) = T) /\ 874 (funcs_ok (If x1 x2 x3) = funcs_ok x1 /\ funcs_ok x2 /\ funcs_ok x3) /\ 875 (funcs_ok (App f xs) = func_name_ok f /\ EVERY funcs_ok xs) /\ 876 (funcs_ok (LamApp vs x xs) = funcs_ok x /\ EVERY funcs_ok xs) /\ 877 (funcs_ok (First x) = funcs_ok x) /\ 878 (funcs_ok (Second x) = funcs_ok x) /\ 879 (funcs_ok (Third x) = funcs_ok x) /\ 880 (funcs_ok (Fourth x) = funcs_ok x) /\ 881 (funcs_ok (Fifth x) = funcs_ok x) /\ 882 (funcs_ok (Or xs) = EVERY funcs_ok xs) /\ 883 (funcs_ok (And xs) = EVERY funcs_ok xs) /\ 884 (funcs_ok (List xs) = EVERY funcs_ok xs) /\ 885 (funcs_ok (Let ts x) = EVERY (\ (x,y). funcs_ok y) ts /\ funcs_ok x) /\ 886 (funcs_ok (Cond ys) = EVERY (\ (x,y). funcs_ok x /\ funcs_ok y) ys) /\ 887 (funcs_ok (LetStar zs x) = funcs_ok x /\ EVERY (\ (x,y). funcs_ok y) zs) /\ 888 (funcs_ok (Defun name vs body) = T)` 889 (WF_REL_TAC `measure term_cost` 890 \\ REPEAT STRIP_TAC \\ IMP_RES_TAC MEM_term_cost 891 \\ IMP_RES_TAC SND_MEM_term_cost \\ IMP_RES_TAC FST_MEM_term_cost 892 \\ FULL_SIMP_TAC std_ss [term_cost_def,LENGTH_MAP,LENGTH,MAP,SUM_def] 893 \\ FULL_SIMP_TAC std_ss [LEFT_ADD_DISTRIB,MULT_CLAUSES] \\ REPEAT DECIDE_TAC); 894 895val funcs_ok_sexp2term = store_thm("funcs_ok_sexp2term", 896 ``!x. funcs_ok (sexp2term x)``, 897 HO_MATCH_MP_TAC sexp2term_ind \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 898 \\ ONCE_REWRITE_TAC [sexp2term_def] \\ SIMP_TAC std_ss [LET_DEF] 899 \\ SRW_TAC [] [] \\ SIMP_TAC std_ss [funcs_ok_def] 900 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP] 901 \\ ASM_SIMP_TAC (srw_ss()) [func_name_ok_def,MEM] 902 \\ Cases_on `CAR x` \\ FULL_SIMP_TAC std_ss [getSym_def] 903 \\ FULL_SIMP_TAC (srw_ss()) []); 904 905val MR_ev_CAR = prove( 906 ``MR_ev (App (PrimitiveFun opCAR) [x],a,ctxt,fns,ok) (s,ok2) = 907 ?res. MR_ev (x,a,ctxt,fns,ok) (res,ok2) /\ (s = CAR res)``, 908 SIMP_TAC (srw_ss()) [Once MR_ev_cases] 909 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases, Once MR_ap_cases] 910 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases,EVAL_DATA_OP_def,PULL_CONJ]); 911 912val MR_ev_CDR = prove( 913 ``MR_ev (App (PrimitiveFun opCDR) [x],a,ctxt,fns,ok) (s,ok2) = 914 ?res. MR_ev (x,a,ctxt,fns,ok) (res,ok2) /\ (s = CDR res)``, 915 SIMP_TAC (srw_ss()) [Once MR_ev_cases] 916 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases, Once MR_ap_cases] 917 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases,EVAL_DATA_OP_def,PULL_CONJ]); 918 919val MR_ev_First = 920 (SIMP_CONV (srw_ss()) [Once MR_ev_cases,MR_ev_CAR]) 921 ``MR_ev (First x,a,ctxt,fns,ok) (s,ok2)`` 922 923val MR_ev_Second = 924 (SIMP_CONV (srw_ss()) [Once MR_ev_cases,MR_ev_CDR,MR_ev_First,PULL_CONJ]) 925 ``MR_ev (Second x,a,ctxt,fns,ok) (s,ok2)`` 926 927val MR_ev_Third = 928 (SIMP_CONV (srw_ss()) [Once MR_ev_cases,MR_ev_CDR,MR_ev_Second,PULL_CONJ]) 929 ``MR_ev (Third x,a,ctxt,fns,ok) (s,ok2)`` 930 931val MR_ev_Fourth = 932 (SIMP_CONV (srw_ss()) [Once MR_ev_cases,MR_ev_CDR,MR_ev_Third,PULL_CONJ]) 933 ``MR_ev (Fourth x,a,ctxt,fns,ok) (s,ok2)`` 934 935val MR_ev_Fifth = 936 (SIMP_CONV (srw_ss()) [Once MR_ev_cases,MR_ev_CDR,MR_ev_Fourth,PULL_CONJ]) 937 ``MR_ev (Fifth x,a,ctxt,fns,ok) (s,ok2)`` 938 939val term2term_First = prove( 940 ``(!res ok2 ok a. 941 funcs_ok x /\ 942 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 943 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\ 944 funcs_ok (First x) /\ 945 MR_ev (term2term (First x),a,ctxt,fns,ok) (res,ok2) ==> 946 MR_ev (First x,a,ctxt,fns,ok) (res,ok2)``, 947 REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 948 LENGTH,funcs_ok_def,EVERY_MEM,f2func_def] \\ POP_ASSUM MP_TAC 949 \\ SIMP_TAC std_ss [MR_ev_First,MR_ev_CAR,MR_ev_First] \\ METIS_TAC []); 950 951val term2term_Second = prove( 952 ``(!res ok2 ok a. 953 funcs_ok x /\ 954 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 955 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\ 956 funcs_ok (Second x) /\ 957 MR_ev (term2term (Second x),a,ctxt,fns,ok) (res,ok2) ==> 958 MR_ev (Second x,a,ctxt,fns,ok) (res,ok2)``, 959 REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 960 LENGTH,funcs_ok_def,EVERY_MEM,f2func_def] \\ POP_ASSUM MP_TAC 961 \\ SIMP_TAC std_ss [MR_ev_CDR,MR_ev_CAR,MR_ev_Second] \\ METIS_TAC []); 962 963val term2term_Third = prove( 964 ``(!res ok2 ok a. 965 funcs_ok x /\ 966 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 967 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\ 968 funcs_ok (Third x) /\ 969 MR_ev (term2term (Third x),a,ctxt,fns,ok) (res,ok2) ==> 970 MR_ev (Third x,a,ctxt,fns,ok) (res,ok2)``, 971 REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 972 LENGTH,funcs_ok_def,EVERY_MEM,f2func_def] \\ POP_ASSUM MP_TAC 973 \\ SIMP_TAC std_ss [MR_ev_CDR,MR_ev_CAR,MR_ev_Third] \\ METIS_TAC []); 974 975val term2term_Fourth = prove( 976 ``(!res ok2 ok a. 977 funcs_ok x /\ 978 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 979 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\ 980 funcs_ok (Fourth x) /\ 981 MR_ev (term2term (Fourth x),a,ctxt,fns,ok) (res,ok2) ==> 982 MR_ev (Fourth x,a,ctxt,fns,ok) (res,ok2)``, 983 REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 984 LENGTH,funcs_ok_def,EVERY_MEM,f2func_def] \\ POP_ASSUM MP_TAC 985 \\ SIMP_TAC std_ss [MR_ev_CDR,MR_ev_CAR,MR_ev_Fourth] \\ METIS_TAC []); 986 987val term2term_Fifth = prove( 988 ``(!res ok2 ok a. 989 funcs_ok x /\ 990 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 991 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\ 992 funcs_ok (Fifth x) /\ 993 MR_ev (term2term (Fifth x),a,ctxt,fns,ok) (res,ok2) ==> 994 MR_ev (Fifth x,a,ctxt,fns,ok) (res,ok2)``, 995 REPEAT STRIP_TAC \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 996 LENGTH,funcs_ok_def,EVERY_MEM,f2func_def] \\ POP_ASSUM MP_TAC 997 \\ SIMP_TAC std_ss [MR_ev_CDR,MR_ev_CAR,MR_ev_Fifth] \\ METIS_TAC []); 998 999val MR_evl_MAP_Var = prove( 1000 ``!vs sl. 1001 MR_evl (MAP Var vs ++ ys,a,ctxt,fns,ok) (sl,ok1) ==> 1002 EVERY (\v. v IN FDOM a) vs /\ 1003 ?sl2. (sl = MAP (\v. a ' v) vs ++ sl2) /\ 1004 MR_evl (ys,a,ctxt,fns,ok) (sl2,ok1)``, 1005 Induct \\ SIMP_TAC std_ss [MAP,APPEND,EVERY_DEF] 1006 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1007 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1008 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [APPEND,CONS_11] 1009 \\ Q.PAT_X_ASSUM `sl = xxx` ASSUME_TAC 1010 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC); 1011 1012val VarBindAux_APPEND = prove( 1013 ``!xs xs2 ys ys2. 1014 (LENGTH xs = LENGTH ys) ==> 1015 (VarBindAux (xs ++ xs2) (ys ++ ys2) = 1016 FUNION (VarBindAux xs ys) (VarBindAux xs2 ys2))``, 1017 Induct \\ Cases_on `ys` 1018 \\ ASM_SIMP_TAC std_ss [APPEND,VarBindAux_def,FUNION_FEMPTY_1, 1019 LENGTH,ADD1,FUNION_FUPDATE_1]); 1020 1021val VarBindAux_ELIM = prove( 1022 ``!vs a. EVERY (\v. v IN FDOM a) vs ==> 1023 ((FUNION (VarBindAux vs (MAP (\v. a ' v) vs)) a) = a)``, 1024 Induct \\ ASM_SIMP_TAC std_ss [VarBindAux_def,FUNION_FEMPTY_1, 1025 MAP,EVERY_DEF,FUNION_FUPDATE_1,SIMP_RULE std_ss [] FUPDATE_ELIM]); 1026 1027val term2term_Let = prove( 1028 ``(!x' x. 1029 MEM (x',x) ts ==> 1030 !res ok2 ok a. 1031 funcs_ok x /\ 1032 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 1033 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\ 1034 (!res ok2 ok a. 1035 funcs_ok x /\ 1036 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 1037 MR_ev (x,a,ctxt,fns,ok) (res,ok2)) /\ 1038 funcs_ok (Let ts x) /\ 1039 MR_ev (term2term (Let ts x),a,ctxt,fns,ok) (res,ok2) ==> 1040 MR_ev (Let ts x,a,ctxt,fns,ok) (res,ok2)``, 1041 REPEAT STRIP_TAC 1042 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1043 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1044 \\ POP_ASSUM MP_TAC 1045 \\ SIMP_TAC std_ss [term2term_def,term2t_def,t2term_def,let2t_def,LET_DEF] 1046 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1047 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1048 \\ FULL_SIMP_TAC std_ss [MAP_MAP_o] 1049 \\ Q.ABBREV_TAC `xs1 = (MAP (Sym o FST o (\(x',y). (x',term2t y)))) ts` 1050 \\ Q.ABBREV_TAC `xs2 = (MAP Sym (free_vars (term2t x)))` 1051 \\ Q.ABBREV_TAC `xs3 = (ISORT (\x y. getSym x <= getSym y) (FILTER 1052 (\x. ~MEM x xs1) (REMOVE_DUPLICATES xs2)))` 1053 \\ `MAP ((\a. t2term a) o mVar o getSym) xs3 = MAP Var (MAP getSym xs3)` by (SIMP_TAC std_ss [MAP_MAP_o,o_DEF,t2term_def]) 1054 \\ FULL_SIMP_TAC std_ss [] 1055 \\ `MAP (getSym o Sym o FST o (\(x',y). (x',term2t y))) ts = MAP FST ts` by (SIMP_TAC std_ss [MAP_MAP_o,o_DEF,t2term_def,getSym_def] 1056 \\ CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV) 1057 \\ SIMP_TAC std_ss [] \\ CONV_TAC (DEPTH_CONV ETA_CONV) 1058 \\ SIMP_TAC std_ss []) 1059 \\ FULL_SIMP_TAC std_ss [] 1060 \\ `MAP ((\a. t2term a) o SND o (\(x',y). (x',term2t y))) ts = 1061 MAP term2term (MAP SND ts)` by 1062 (SIMP_TAC std_ss [MAP_MAP_o,o_DEF,t2term_def,getSym_def] 1063 \\ CONV_TAC (DEPTH_CONV PairRules.PBETA_CONV) 1064 \\ SIMP_TAC std_ss [term2term_def]) 1065 \\ FULL_SIMP_TAC std_ss [] 1066 \\ IMP_RES_TAC MR_evl_MAP_Var 1067 \\ FULL_SIMP_TAC std_ss [funcs_ok_def] 1068 \\ Q.LIST_EXISTS_TAC [`sl2`,`ok1`] 1069 \\ `FUNION (VarBind (MAP getSym xs3 ++ MAP FST ts) 1070 (MAP (\v. a ' v) (MAP getSym xs3) ++ sl2)) a = 1071 FUNION (VarBind (MAP FST ts) sl2) a` by 1072 (FULL_SIMP_TAC std_ss [VarBind_def,REVERSE_APPEND] 1073 \\ `LENGTH (REVERSE (MAP FST ts)) = LENGTH (REVERSE sl2)` by 1074 (IMP_RES_TAC MR_evl_LENGTH 1075 \\ FULL_SIMP_TAC std_ss [LENGTH_REVERSE,LENGTH_MAP]) 1076 \\ IMP_RES_TAC VarBindAux_APPEND 1077 \\ FULL_SIMP_TAC std_ss [GSYM FUNION_ASSOC] 1078 \\ METIS_TAC [VarBindAux_ELIM,rich_listTheory.ALL_EL_REVERSE,rich_listTheory.MAP_REVERSE]) 1079 \\ FULL_SIMP_TAC std_ss [GSYM term2term_def] \\ RES_TAC 1080 \\ Q.PAT_X_ASSUM `!x' x''. MEM (x',x'') ts ==> bbb` MP_TAC 1081 \\ Q.PAT_X_ASSUM `MR_evl (MAP term2term (MAP SND ts),a,xx) bb` MP_TAC 1082 \\ Q.PAT_X_ASSUM `EVERY (\(x',y). funcs_ok y) ts` MP_TAC 1083 \\ Q.SPEC_TAC (`ok`,`ok`) \\ Q.SPEC_TAC (`ok1`,`ok1`) 1084 \\ Q.SPEC_TAC (`sl2`,`sl2`) \\ Q.SPEC_TAC (`ts`,`ts`) 1085 \\ Induct \\ SIMP_TAC std_ss [MAP] \\ Cases 1086 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases] \\ REPEAT STRIP_TAC 1087 \\ ASM_SIMP_TAC (srw_ss()) [Once MR_evl_cases] 1088 \\ Q.LIST_EXISTS_TAC [`ok1''`] 1089 \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [PULL_IMP,AND_IMP_INTRO]) 1090 \\ Q.PAT_X_ASSUM `!sl:SExp list.bbb` ASSUME_TAC 1091 \\ FULL_SIMP_TAC std_ss [AND_IMP_INTRO] 1092 \\ POP_ASSUM MATCH_MP_TAC \\ METIS_TAC []); 1093 1094val IMP_IMP = METIS_PROVE [] ``b1 /\ (b2 ==> b3) ==> ((b1 ==> b2) ==> b3)``; 1095 1096val MEM_ISORT_INSERT = prove( 1097 ``!xs g x y. MEM x (ISORT_INSERT g y xs) = MEM x (y::xs)``, 1098 Induct \\ SRW_TAC [] [ISORT_INSERT_def,MEM] \\ METIS_TAC []); 1099 1100val MEM_ISORT = prove( 1101 ``!xs x g. MEM x (ISORT g xs) = MEM x xs``, 1102 Induct \\ ASM_SIMP_TAC std_ss [ISORT_def,MEM,MEM_ISORT_INSERT]); 1103 1104val FLAT_SNOC = prove( 1105 ``!xs x. FLAT (xs ++ [x]) = FLAT xs ++ x``, 1106 Induct \\ FULL_SIMP_TAC std_ss [FLAT,APPEND,APPEND_NIL,APPEND_ASSOC]); 1107 1108val MEM_free_vars_or2t = prove( 1109 ``!xs. 1110 MEM "SPECIAL-VAR-FOR-OR" (free_vars (or2t xs)) = 1111 MEM "SPECIAL-VAR-FOR-OR" (FLAT (MAP free_vars xs))``, 1112 Cases THEN1 EVAL_TAC \\ Q.SPEC_TAC (`h`,`h`) \\ Induct_on `t` 1113 \\ ASM_SIMP_TAC std_ss [or2t_def,MAP,FLAT,APPEND_NIL,LET_DEF,MEM_APPEND] 1114 \\ STRIP_TAC \\ STRIP_TAC 1115 \\ Cases_on `MEM "SPECIAL-VAR-FOR-OR" (free_vars h)` 1116 \\ FULL_SIMP_TAC std_ss [free_vars_def,MAP,FLAT,MEM_APPEND] 1117 \\ Cases_on `MEM "SPECIAL-VAR-FOR-OR" (FLAT (MAP free_vars t))` 1118 \\ FULL_SIMP_TAC std_ss [free_vars_def,MAP,FLAT,MEM_APPEND] 1119 \\ Cases_on `isTrue (logic_variablep (t2sexp h'))` 1120 \\ FULL_SIMP_TAC std_ss [free_vars_def,MAP,FLAT,MEM_APPEND,MEM] 1121 \\ Cases_on `isTrue (logic_constantp (t2sexp h'))` 1122 \\ FULL_SIMP_TAC std_ss [free_vars_def,MAP,FLAT,MEM_APPEND,MEM] 1123 \\ SIMP_TAC std_ss [let2t_def,MAP,LET_DEF,free_vars_def,FLAT,APPEND, 1124 APPEND_NIL,REMOVE_DUPLICATES_def,MEM,MEM_APPEND,MAP_APPEND] 1125 \\ FULL_SIMP_TAC std_ss [FLAT_SNOC,MEM_APPEND] 1126 \\ MATCH_MP_TAC (METIS_PROVE [] ``~b ==> (b \/ c = c)``) 1127 \\ FULL_SIMP_TAC std_ss [MEM_FLAT] 1128 \\ FULL_SIMP_TAC std_ss [MEM_MAP,MEM_ISORT,MEM_FILTER] 1129 \\ SIMP_TAC std_ss [METIS_PROVE [] ``~b \/ c = b ==> c``] 1130 \\ SIMP_TAC std_ss [METIS_PROVE [] ``c \/ ~b = b ==> c``] 1131 \\ SIMP_TAC (srw_ss()) [PULL_IMP] 1132 \\ Cases \\ SIMP_TAC std_ss [free_vars_def,MEM,getSym_def,CONS_11,NOT_CONS_NIL]); 1133 1134val term_ok_let2t = prove( 1135 ``term_ok ctxt (let2t xs y) ==> 1136 EVERY (\x. term_ok ctxt (SND x)) xs /\ term_ok ctxt y``, 1137 SIMP_TAC std_ss [let2t_def,LET_DEF,term_ok_def,EVERY_APPEND,EVERY_MEM,MEM_MAP] 1138 \\ SIMP_TAC std_ss [PULL_IMP]); 1139 1140val term_ok_or2t = prove( 1141 ``!xs. term_ok ctxt (or2t xs) ==> EVERY (term_ok ctxt) xs``, 1142 Cases THEN1 (SIMP_TAC std_ss [EVERY_DEF]) 1143 \\ Q.SPEC_TAC (`h`,`h`) \\ Q.SPEC_TAC (`t`,`t`) \\ Induct 1144 \\ SIMP_TAC std_ss [or2t_def,EVERY_DEF,LET_DEF] 1145 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [term_ok_def,EVERY_DEF] 1146 \\ RES_TAC \\ IMP_RES_TAC term_ok_let2t 1147 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,term_ok_def] \\ RES_TAC); 1148 1149val MEM_REMOVE_DUPLICATES = prove( 1150 ``!xs x. MEM x (REMOVE_DUPLICATES xs) = MEM x xs``, 1151 Induct \\ SRW_TAC [] [REMOVE_DUPLICATES_def,MEM] \\ METIS_TAC []); 1152 1153val FLAT_APPEND = prove( 1154 ``!xs ys. FLAT (xs ++ ys) = FLAT xs ++ FLAT ys``, 1155 Induct \\ ASM_SIMP_TAC std_ss [APPEND,FLAT,APPEND_ASSOC]); 1156 1157val MEM_free_vars_let2t = prove( 1158 ``MEM "SPECIAL-VAR-FOR-OR" (free_vars (let2t ts x)) = 1159 MEM "SPECIAL-VAR-FOR-OR" 1160 (FILTER (\v. ~MEM v (MAP FST ts)) (free_vars x) ++ 1161 FLAT (MAP (\ (x,y). free_vars y) ts))``, 1162 SIMP_TAC std_ss [let2t_def,LET_DEF,free_vars_def,MAP_APPEND,FLAT_APPEND] 1163 \\ SIMP_TAC std_ss [MEM_APPEND] 1164 \\ FULL_SIMP_TAC std_ss [MAP_MAP_o,o_DEF] 1165 \\ `(\x. free_vars (SND x)) = (\(x:string,y). free_vars y)` by (FULL_SIMP_TAC std_ss [FUN_EQ_THM,pairTheory.FORALL_PROD]) 1166 \\ FULL_SIMP_TAC std_ss [] 1167 \\ Cases_on `MEM "SPECIAL-VAR-FOR-OR" (FLAT (MAP (\(x,y). free_vars y) ts))` 1168 \\ FULL_SIMP_TAC std_ss [] 1169 \\ FULL_SIMP_TAC std_ss [MEM_FLAT] 1170 \\ FULL_SIMP_TAC std_ss [METIS_PROVE [] ``~b \/ c = b ==> c``] 1171 \\ FULL_SIMP_TAC std_ss [MEM_MAP,PULL_IMP,pairTheory.FORALL_PROD,PULL_CONJ] 1172 \\ FULL_SIMP_TAC std_ss [MEM_ISORT,MEM_FILTER,MEM_REMOVE_DUPLICATES] 1173 \\ FULL_SIMP_TAC std_ss [MEM_MAP] 1174 \\ FULL_SIMP_TAC std_ss [METIS_PROVE [] ``Q /\ (?x. P x) = ?x. Q /\ P x``] 1175 \\ FULL_SIMP_TAC std_ss [METIS_PROVE [] ``(?x. P x) /\ Q = ?x. Q /\ P x``] 1176 \\ FULL_SIMP_TAC (srw_ss()) [free_vars_def,getSym_def]); 1177 1178val free_vars_term_vars = prove( 1179 ``!x. term_ok ctxt (term2t x) ==> 1180 (MEM "SPECIAL-VAR-FOR-OR" (free_vars (term2t x)) = 1181 MEM "SPECIAL-VAR-FOR-OR" (term_vars x))``, 1182 HO_MATCH_MP_TAC (fetch "-" "term2t_ind") \\ REPEAT STRIP_TAC 1183 \\ FULL_SIMP_TAC std_ss [term2t_def,free_vars_def,term_vars_def, 1184 FLAT,MEM,MAP,APPEND_NIL,APPEND_ASSOC,MEM_APPEND,term_ok_def,EVERY_DEF] 1185 \\ IMP_RES_TAC term_ok_or2t 1186 \\ FULL_SIMP_TAC std_ss [MEM_FLAT,MEM_MAP,PULL_CONJ,MEM_free_vars_or2t, 1187 EVERY_MEM,PULL_CONJ,PULL_IMP,MEM_FILTER] 1188 THEN1 (METIS_TAC []) 1189 THEN1 (Cases_on `MEM "SPECIAL-VAR-FOR-OR" vs` \\ FULL_SIMP_TAC std_ss [] 1190 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ METIS_TAC []) 1191 THEN1 (METIS_TAC []) 1192 THEN1 (METIS_TAC []) 1193 THEN1 (FULL_SIMP_TAC std_ss [MEM_free_vars_let2t,MEM_FILTER,pairTheory.EXISTS_PROD, 1194 MEM_APPEND,MEM_FLAT,MEM_MAP,PULL_CONJ,pairTheory.FORALL_PROD] 1195 \\ IMP_RES_TAC term_ok_let2t 1196 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP,pairTheory.FORALL_PROD] 1197 \\ METIS_TAC [])); 1198 1199val term2term_Or = prove( 1200 ``!xs res ok ok2 a. 1201 (!x. 1202 MEM x xs ==> 1203 !res' ok2' ok' a'. 1204 MR_ev (term2term x,a',ctxt,fns,ok') (res',ok2') ==> 1205 MR_ev (x,a',ctxt,fns,ok') (res',ok2')) /\ 1206 EVERY (term_ok ctxt5) (MAP term2t xs) /\ EVERY funcs_ok xs /\ 1207 MR_ev (term2term (Or xs),a,ctxt,fns,ok) (res,ok2) ==> 1208 MR_ev (Or xs,a,ctxt,fns,ok) (res,ok2)``, 1209 Cases THEN1 1210 (SIMP_TAC std_ss [term2term_def,term2t_def,MAP,or2t_def,t2term_def,MEM] 1211 \\ REPEAT (ASM_SIMP_TAC (srw_ss()) [Once MR_ev_cases])) 1212 \\ SIMP_TAC std_ss [term2term_def,term2t_def] 1213 \\ Q.SPEC_TAC (`h`,`h`) \\ Q.SPEC_TAC (`t`,`t`) \\ Induct THEN1 1214 (SIMP_TAC std_ss [MAP,MEM,or2t_def,EVERY_DEF] \\ REPEAT STRIP_TAC 1215 \\ ASM_SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ RES_TAC 1216 \\ SIMP_TAC std_ss [isTrue_def] 1217 \\ Cases_on `res = Sym "NIL"` \\ FULL_SIMP_TAC std_ss [] 1218 \\ ONCE_REWRITE_TAC [CONJ_COMM] 1219 \\ ASM_SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1220 \\ ASM_SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ METIS_TAC []) 1221 \\ SIMP_TAC std_ss [or2t_def,MAP,LET_DEF] 1222 \\ REPEAT STRIP_TAC 1223 \\ FULL_SIMP_TAC std_ss [METIS_PROVE [] ``b\/c = ~b ==> c``] 1224 \\ Cases_on `~isTrue (logic_variablep (t2sexp (term2t h'))) /\ 1225 ~isTrue (logic_constantp (t2sexp (term2t h'))) ==> 1226 MEM "SPECIAL-VAR-FOR-OR" (free_vars (or2t (term2t h::MAP (\a. term2t a) t)))` 1227 \\ FULL_SIMP_TAC (srw_ss()) [t2term_def,LENGTH] THEN1 1228 (FULL_SIMP_TAC std_ss [LET_DEF] 1229 \\ POP_ASSUM (K ALL_TAC) \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1230 \\ POP_ASSUM MP_TAC \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1231 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] THEN1 1232 (DISJ2_TAC \\ Q.LIST_EXISTS_TAC [`ok1`,`s1`] 1233 \\ FULL_SIMP_TAC std_ss [PULL_IMP,AND_IMP_INTRO] 1234 \\ Q.PAT_X_ASSUM `!x1 x2 x3 x4 x5. bbb ==> MR_ev (Or xx,yyy) zz` MATCH_MP_TAC 1235 \\ FULL_SIMP_TAC std_ss [] \\ STRIP_TAC THEN1 (METIS_TAC []) 1236 \\ FULL_SIMP_TAC std_ss [GSYM lisp_extractTheory.R_ev_Or_SING_EQ]) 1237 \\ IMP_RES_TAC MR_ev_11 \\ FULL_SIMP_TAC std_ss [] \\ DISJ1_TAC 1238 \\ `MR_ev (h',a,ctxt,fns,ok) (res,ok1)` by METIS_TAC [] 1239 \\ `MR_ev (h',a,ctxt,fns,ok1) (res,ok2)` by METIS_TAC [] 1240 \\ Cases_on `ok2` \\ IMP_RES_TAC MR_ev_OK \\ FULL_SIMP_TAC std_ss [] 1241 \\ Cases_on `ok1` \\ IMP_RES_TAC MR_ev_OK \\ FULL_SIMP_TAC std_ss []) 1242 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1243 \\ MP_TAC (term2term_Let 1244 |> Q.INST [`ts`|->`[("SPECIAL-VAR-FOR-OR",h')]`, 1245 `x`|->`If (Var "SPECIAL-VAR-FOR-OR") (Var "SPECIAL-VAR-FOR-OR") (Or (h::t))`] 1246 |> SIMP_RULE (srw_ss()) [term2term_def,t2term_def,term2t_def,funcs_ok_def,LET_DEF]) 1247 \\ FULL_SIMP_TAC std_ss [] 1248 \\ MATCH_MP_TAC IMP_IMP 1249 \\ STRIP_TAC THEN1 1250 (FULL_SIMP_TAC std_ss [EVERY_MEM] 1251 \\ REPEAT STRIP_TAC \\ POP_ASSUM MP_TAC 1252 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC (srw_ss()) [] 1253 \\ SIMP_TAC std_ss [ONCE_REWRITE_CONV [MR_ev_cases] ``MR_ev (Var v,a,x) y`` 1254 |> SIMP_RULE (srw_ss()) []] \\ METIS_TAC [MR_ev_OK]) 1255 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1256 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1257 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1258 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases,PULL_CONJ] \\ STRIP_TAC 1259 \\ Q.PAT_X_ASSUM `MR_ev xx yy` MP_TAC \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1260 \\ SIMP_TAC std_ss [ONCE_REWRITE_CONV [MR_ev_cases] ``MR_ev (Var v,a,x) y`` 1261 |> SIMP_RULE (srw_ss()) [],FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_INSERT] 1262 \\ FULL_SIMP_TAC std_ss [VarBind_def,VarBindAux_def,REVERSE_DEF,APPEND] 1263 \\ FULL_SIMP_TAC std_ss [FUNION_FUPDATE_1,FUNION_FEMPTY_1, 1264 FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_INSERT] 1265 \\ REVERSE (REPEAT STRIP_TAC) THEN1 (FULL_SIMP_TAC std_ss []) 1266 \\ DISJ2_TAC \\ Q.LIST_EXISTS_TAC [`ok1`,`s`] 1267 \\ FULL_SIMP_TAC std_ss [] 1268 \\ MATCH_MP_TAC MR_ev_VARS 1269 \\ Q.EXISTS_TAC `a |+ ("SPECIAL-VAR-FOR-OR",s)` \\ FULL_SIMP_TAC std_ss [] 1270 \\ FULL_SIMP_TAC std_ss [FDOM_FUPDATE,FAPPLY_FUPDATE_THM,IN_INSERT] 1271 \\ STRIP_TAC \\ Cases_on `y = "SPECIAL-VAR-FOR-OR"` \\ FULL_SIMP_TAC std_ss [] 1272 \\ STRIP_TAC \\ sg `F` \\ FULL_SIMP_TAC std_ss [] 1273 \\ FULL_SIMP_TAC std_ss [term_vars_def,MEM_free_vars_or2t] 1274 \\ FULL_SIMP_TAC std_ss [MEM_FLAT,MEM_MAP] 1275 \\ `term2t h::MAP (\a. term2t a) t = MAP (\a. term2t a) (h::t)` by FULL_SIMP_TAC std_ss [MAP] 1276 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 1277 \\ FULL_SIMP_TAC std_ss [MEM_MAP,EVERY_MEM,PULL_IMP] 1278 \\ METIS_TAC [free_vars_term_vars,MEM]); 1279 1280val MR_ev_term2term = store_thm("MR_ev_term2term", 1281 ``!x res ok2 ok a. 1282 funcs_ok x /\ term_ok ctxt5 (term2t x) /\ 1283 MR_ev (term2term x,a,ctxt,fns,ok) (res,ok2) ==> 1284 MR_ev (x,a,ctxt,fns,ok) (res,ok2)``, 1285 HO_MATCH_MP_TAC (fetch "-" "term2t_ind") \\ REPEAT STRIP_TAC 1286 THEN1 (FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def,LENGTH]) 1287 THEN1 (FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def,LENGTH]) 1288 THEN1 (FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 1289 LENGTH,funcs_ok_def,LET_DEF,term_ok_def] 1290 \\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [MR_ev_cases] 1291 \\ FULL_SIMP_TAC (srw_ss()) [] \\ METIS_TAC []) 1292 THEN1 (FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 1293 LENGTH,funcs_ok_def,EVERY_MEM,term_ok_def] 1294 \\ IMP_RES_TAC f2func_func2f \\ FULL_SIMP_TAC std_ss [] 1295 \\ Q.PAT_X_ASSUM `MR_ev xx yy` MP_TAC 1296 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC (srw_ss()) [] 1297 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1298 \\ Q.LIST_EXISTS_TAC [`args`,`ok1`] \\ ASM_SIMP_TAC std_ss [] 1299 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 1300 \\ REPEAT (Q.PAT_X_ASSUM `!x.bbb` MP_TAC) 1301 \\ Q.PAT_X_ASSUM `MR_evl xx yy` MP_TAC 1302 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1303 \\ Q.SPEC_TAC (`args`,`args`) \\ Q.SPEC_TAC (`ok`,`ok`) 1304 \\ Induct_on `xs` \\ FULL_SIMP_TAC std_ss [MAP,MEM] 1305 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1306 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1307 \\ FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC \\ METIS_TAC []) 1308 THEN1 (FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def, 1309 LENGTH,funcs_ok_def,EVERY_MEM,term_ok_def] 1310 \\ POP_ASSUM MP_TAC \\ ONCE_REWRITE_TAC [MR_ev_cases] 1311 \\ FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 1312 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC 1313 \\ Q.LIST_EXISTS_TAC [`sl`,`ok1`] 1314 \\ ASM_SIMP_TAC std_ss [] 1315 \\ REPEAT (Q.PAT_X_ASSUM `!x.bbb` MP_TAC) 1316 \\ Q.PAT_X_ASSUM `MR_evl xx yy` MP_TAC 1317 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1318 \\ Q.SPEC_TAC (`sl`,`sl`) \\ Q.SPEC_TAC (`ok`,`ok`) 1319 \\ Induct_on `xs` \\ FULL_SIMP_TAC std_ss [MAP,MEM] 1320 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1321 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1322 \\ FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC \\ METIS_TAC []) 1323 THEN1 (FULL_SIMP_TAC std_ss [term_ok_def,term2t_def,EVERY_DEF] 1324 \\ METIS_TAC [term2term_First]) 1325 THEN1 (FULL_SIMP_TAC std_ss [term_ok_def,term2t_def,EVERY_DEF] 1326 \\ METIS_TAC [term2term_Second]) 1327 THEN1 (FULL_SIMP_TAC std_ss [term_ok_def,term2t_def,EVERY_DEF] 1328 \\ METIS_TAC [term2term_Third]) 1329 THEN1 (FULL_SIMP_TAC std_ss [term_ok_def,term2t_def,EVERY_DEF] 1330 \\ METIS_TAC [term2term_Fourth]) 1331 THEN1 (FULL_SIMP_TAC std_ss [term_ok_def,term2t_def,EVERY_DEF] 1332 \\ METIS_TAC [term2term_Fifth]) 1333 THEN1 (MATCH_MP_TAC term2term_Or 1334 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,funcs_ok_def,term_ok_def] 1335 \\ FULL_SIMP_TAC std_ss [term2t_def] 1336 \\ IMP_RES_TAC term_ok_or2t 1337 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP]) 1338 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1339 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases,term2term_def,term2t_def,t2term_def] 1340 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases,term2term_def,term2t_def,t2term_def]) 1341 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1342 \\ FULL_SIMP_TAC std_ss [term2term_def,term2t_def,t2term_def,funcs_ok_def,EVERY_DEF]) 1343 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1344 \\ SIMP_TAC std_ss [term2term_def,term2t_def,t2term_def,LENGTH] 1345 \\ SIMP_TAC (srw_ss()) [LET_DEF] 1346 \\ FULL_SIMP_TAC std_ss [funcs_ok_def,EVERY_DEF,term_ok_def,term2t_def] 1347 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC (srw_ss()) [t2term_def] 1348 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [term2term_def] 1349 \\ RES_TAC \\ METIS_TAC []) 1350 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1351 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases,term2term_def,term2t_def,t2term_def] 1352 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases,term2term_def,term2t_def,t2term_def]) 1353 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1354 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1355 \\ SIMP_TAC (srw_ss()) [Once MR_ap_cases,EVAL_DATA_OP_def] 1356 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases] 1357 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases] 1358 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases,PULL_CONJ] 1359 \\ SRW_TAC [] [] \\ POP_ASSUM MP_TAC 1360 \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def,f2func_def] 1361 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1362 \\ SIMP_TAC (srw_ss()) [Once MR_ap_cases,EVAL_DATA_OP_def] 1363 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases] 1364 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases] 1365 \\ SIMP_TAC (srw_ss()) [Once MR_evl_cases,PULL_CONJ] 1366 \\ REPEAT STRIP_TAC 1367 \\ FULL_SIMP_TAC std_ss [funcs_ok_def,EVERY_DEF,term_ok_def] 1368 \\ METIS_TAC []) 1369 THEN1 (MATCH_MP_TAC term2term_Let 1370 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,funcs_ok_def,term_ok_def] 1371 \\ FULL_SIMP_TAC std_ss [term2t_def] 1372 \\ IMP_RES_TAC term_ok_let2t 1373 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP] 1374 \\ FULL_SIMP_TAC std_ss [pairTheory.FORALL_PROD] \\ METIS_TAC []) 1375 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1376 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases,term2term_def,term2t_def,t2term_def] 1377 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases,term2term_def,term2t_def,t2term_def]) 1378 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1379 \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,t2term_def,term2t_def,f2func_def] 1380 \\ FULL_SIMP_TAC std_ss [LET_DEF] 1381 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1382 \\ FULL_SIMP_TAC std_ss [funcs_ok_def,EVERY_DEF,term_ok_def] 1383 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1384 \\ SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1385 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC \\ METIS_TAC []) 1386 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1387 \\ FULL_SIMP_TAC std_ss [term2term_def,term2t_def,t2term_def,funcs_ok_def,EVERY_DEF]) 1388 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] 1389 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ POP_ASSUM MP_TAC 1390 \\ FULL_SIMP_TAC std_ss [term2term_def,term2t_def,funcs_ok_def,EVERY_DEF]) 1391 THEN1 (SIMP_TAC (srw_ss()) [Once MR_ev_cases] \\ POP_ASSUM MP_TAC 1392 \\ FULL_SIMP_TAC (srw_ss()) [term2term_def,term2t_def,t2term_def, 1393 funcs_ok_def,EVERY_DEF,f2func_def])); 1394 1395(* M_ev ==> MR_ev *) 1396 1397val VarBindAux_lemma = prove( 1398 ``!params t. 1399 ~MEM p params /\ (LENGTH params = LENGTH t) ==> 1400 (VarBindAux (params ++ [p]) (t ++ [h]) = 1401 VarBindAux (params) t |+ (p,h))``, 1402 Induct \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [ADD1,LENGTH] THEN1 EVAL_TAC 1403 \\ ASM_SIMP_TAC std_ss [APPEND,MEM,VarBindAux_def] 1404 \\ METIS_TAC [FUPDATE_COMMUTES]); 1405 1406val VarBind_CONS = prove( 1407 ``!params t. 1408 ~MEM p params /\ (LENGTH params = LENGTH t) ==> 1409 (VarBind (p::params) (h::t) = VarBind params t |+ (p,h))``, 1410 SIMP_TAC std_ss [VarBind_def,REVERSE_DEF] \\ Induct 1411 \\ Cases_on `t` \\ FULL_SIMP_TAC std_ss [ADD1,LENGTH] THEN1 EVAL_TAC 1412 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC VarBindAux_lemma 1413 \\ FULL_SIMP_TAC std_ss [LENGTH_REVERSE,LENGTH,MEM_REVERSE]); 1414 1415val params_lemma = store_thm("params_lemma", 1416 ``!params args (v:string). 1417 MEM v params /\ (LENGTH args = LENGTH params) /\ ALL_DISTINCT params ==> 1418 v IN FDOM (VarBind params args) /\ 1419 (VarBind params args ' v = FunVarBind params args v)``, 1420 Induct \\ SIMP_TAC std_ss [MEM] 1421 \\ Cases_on `args` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 1422 \\ FULL_SIMP_TAC std_ss [FunVarBind_def,APPLY_UPDATE_THM] 1423 \\ ASM_SIMP_TAC std_ss [VarBind_CONS,ALL_DISTINCT] 1424 \\ FULL_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM, 1425 FDOM_FUPDATE,IN_INSERT] 1426 \\ METIS_TAC []); 1427 1428val LENGTH_EQ_1 = prove( 1429 ``(1 = LENGTH xs) = ?x1. xs = [x1]``, 1430 Cases_on `xs` \\ SIMP_TAC (srw_ss()) [] 1431 \\ Cases_on `t` \\ SIMP_TAC (srw_ss()) [] 1432 \\ Cases_on `t'` \\ SIMP_TAC (srw_ss()) [] 1433 \\ Cases_on `t` \\ SIMP_TAC (srw_ss()) [] 1434 \\ DECIDE_TAC) 1435 1436val LENGTH_EQ_2 = prove( 1437 ``(2 = LENGTH xs) = ?x1 x2. xs = [x1;x2]``, 1438 Cases_on `xs` \\ SIMP_TAC (srw_ss()) [] 1439 \\ Cases_on `t` \\ SIMP_TAC (srw_ss()) [] 1440 \\ Cases_on `t'` \\ SIMP_TAC (srw_ss()) [] 1441 \\ Cases_on `t` \\ SIMP_TAC (srw_ss()) [] 1442 \\ DECIDE_TAC) 1443 1444val rank_lemma = prove( 1445 ``!x1. rank x1 = Val (LSIZE x1)``, 1446 REVERSE Induct \\ ONCE_REWRITE_TAC [rank_def] 1447 \\ FULL_SIMP_TAC (srw_ss()) [LSIZE_def,LISP_CONSP_def,isDot_def, 1448 LISP_TEST_def,isTrue_def,LISP_ADD_def,getVal_def,CDR_def,CAR_def] 1449 \\ DECIDE_TAC); 1450 1451val LISP_TEST_THM = prove( 1452 ``!b. (isTrue (LISP_TEST b) = b) /\ 1453 ((LISP_TEST b = Sym "NIL") = ~b) /\ ((LISP_TEST b = Sym "T") = b)``, 1454 Cases \\ FULL_SIMP_TAC std_ss [] \\ EVAL_TAC); 1455 1456val isTrue_not = prove( 1457 ``!x. isTrue (not x) = ~isTrue x``, 1458 SIMP_TAC std_ss [isTrue_def,not_def] \\ SRW_TAC [] []); 1459 1460val ord__lemma = prove( 1461 ``!x1 x2. LISP_TEST (ORD_LT x1 x2) = ord_ x1 x2``, 1462 HO_MATCH_MP_TAC milawa_ordinalTheory.ORD_LT_ind \\ REPEAT STRIP_TAC 1463 \\ FULL_SIMP_TAC std_ss [] 1464 \\ ONCE_REWRITE_TAC [milawa_ordinalTheory.ORD_LT_def,ord__def] 1465 \\ SRW_TAC [] [LISP_TEST_def,LISP_LESS_def,isTrue_not,LISP_CONSP_def] 1466 \\ FULL_SIMP_TAC (srw_ss()) [lisp_extractTheory.isTrue_CLAUSES] 1467 \\ REPEAT (POP_ASSUM MP_TAC) \\ FULL_SIMP_TAC (srw_ss()) [isTrue_def] 1468 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1469 \\ FULL_SIMP_TAC std_ss [LISP_TEST_def] 1470 \\ Cases_on `isDot x2` \\ FULL_SIMP_TAC std_ss []); 1471 1472val ordp_lemma = prove( 1473 ``!x1. LISP_TEST (ORDP x1) = ordp x1``, 1474 ONCE_REWRITE_TAC [EQ_SYM_EQ] 1475 \\ HO_MATCH_MP_TAC milawa_ordinalTheory.ORDP_ind \\ REPEAT STRIP_TAC 1476 \\ FULL_SIMP_TAC std_ss [] 1477 \\ ONCE_REWRITE_TAC [milawa_ordinalTheory.ORDP_def,ordp_def] 1478 \\ SRW_TAC [] [LISP_TEST_def,LISP_LESS_def,isTrue_not,LISP_CONSP_def] 1479 \\ FULL_SIMP_TAC (srw_ss()) [lisp_extractTheory.isTrue_CLAUSES] 1480 \\ FULL_SIMP_TAC std_ss [LISP_NUMBERP_def,LISP_TEST_def] 1481 \\ REPEAT (POP_ASSUM MP_TAC) 1482 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss [isTrue_def,getVal_def] 1483 \\ FULL_SIMP_TAC std_ss [GSYM ord__lemma,LISP_TEST_def]); 1484 1485val fake_ftbl_entries_def = Define ` 1486 fake_ftbl_entries = 1487 ["IF"; "EQUAL"; "SYMBOLP"; "SYMBOL-<"; "NATP"; "<"; "+"; "-"; 1488 "CONSP"; "CONS"; "CAR"; "CDR"; "ERROR"; "PRINT"; "DEFINE"; 1489 "DEFUN"; "FUNCALL"; "LOOKUP-SAFE"; "DEFINE-SAFE"; 1490 "DEFINE-SAFE-LIST"; "MILAWA-INIT"; "MILAWA-MAIN"]`; 1491 1492val MilawaTrueFun_def = Define ` 1493 MilawaTrueFun ctxt f args result = 1494 MilawaTrue ctxt (Equal (mApp (mFun f) (MAP mConst args)) (mConst result))`; 1495 1496val runtime_inv_def = Define ` 1497 runtime_inv (ctxt:context_type) k = 1498 !name params body sem args ok. 1499 name IN FDOM ctxt /\ (ctxt ' name = (params,body,sem)) /\ 1500 (LENGTH args = LENGTH params) ==> 1501 ?ok2. MR_ap (Fun name,args,ARB,ctxt,k,ok) (sem args,ok2) /\ 1502 (ok2 ==> MilawaTrueFun ctxt name args (sem args))`; 1503 1504val MR_ap_CTXT = prove( 1505 ``MR_ap (Fun fc,args,a,ctxt \\ name,k,ok) (sem args,ok2) ==> 1506 MR_ap (Fun fc,args,a,ctxt,k,ok) (sem args,ok2)``, 1507 METIS_TAC [MR_ev_CTXT]); 1508 1509 1510(* M_IMP_MilawaTrue *) 1511 1512val MilawaTrue_MP = prove( 1513 ``context_ok ctxt /\ 1514 MilawaTrue ctxt a /\ MilawaTrue ctxt (Or (Not a) b) ==> 1515 MilawaTrue ctxt b``, 1516 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1517 \\ FULL_SIMP_TAC std_ss [formula_ok_def] \\ METIS_TAC [MilawaTrue_rules]); 1518 1519val MilawaTrue_MP2 = prove( 1520 ``context_ok ctxt /\ 1521 MilawaTrue ctxt (Not a) /\ MilawaTrue ctxt (Or a b) ==> 1522 MilawaTrue ctxt b``, 1523 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1524 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1525 \\ METIS_TAC [MilawaTrue_rules,formula_ok_def]); 1526 1527val MilawaTrue_REFL = prove( 1528 ``term_ok ctxt x ==> MilawaTrue ctxt (Equal x x)``, 1529 REPEAT STRIP_TAC 1530 \\ `MEM (HD MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1531 \\ FULL_SIMP_TAC std_ss [EVAL ``HD MILAWA_AXIOMS``] 1532 \\ `MilawaTrue ctxt (Equal (mVar "X") (mVar "X"))` by METIS_TAC [MilawaTrue_rules] 1533 \\ `Equal x x = formula_sub [("X",x)] (Equal (mVar "X") (mVar "X"))` by EVAL_TAC 1534 \\ FULL_SIMP_TAC std_ss [] 1535 \\ MATCH_MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1536 \\ FULL_SIMP_TAC std_ss [] \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []); 1537 1538val MilawaTrue_Sym = prove( 1539 ``context_ok ctxt /\ 1540 MilawaTrue ctxt (Equal x y) ==> MilawaTrue ctxt (Equal y x)``, 1541 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1542 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1543 \\ IMP_RES_TAC MilawaTrue_REFL 1544 \\ `MEM (EL 1 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1545 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 1 MILAWA_AXIOMS``] 1546 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1547 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1548 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1549 \\ `formula_ok ctxt (formula_sub [("X1",x);("X2",x);("Y1",y);("Y2",x)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1550 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1551 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1552 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1553 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def] 1554 \\ METIS_TAC [MilawaTrue_MP]); 1555 1556val MilawaTrue_TRANS = store_thm("MilawaTrue_TRANS", 1557 ``context_ok ctxt /\ 1558 MilawaTrue ctxt (Equal x y) /\ MilawaTrue ctxt (Equal y z) ==> 1559 MilawaTrue ctxt (Equal x z)``, 1560 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1561 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1562 \\ IMP_RES_TAC MilawaTrue_REFL 1563 \\ `MEM (EL 1 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1564 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 1 MILAWA_AXIOMS``] 1565 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1566 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1567 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1568 \\ `formula_ok ctxt (formula_sub [("X1",y);("X2",y);("Y1",x);("Y2",z)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1569 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1570 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1571 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1572 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def] 1573 \\ METIS_TAC [MilawaTrue_MP,MilawaTrue_Sym]) |> GEN_ALL; 1574 1575val MilawaTrue_IF1 = prove( 1576 ``context_ok ctxt /\ 1577 MilawaTrue ctxt (Equal e1 (mConst s1)) /\ ~isTrue s1 /\ 1578 MilawaTrue ctxt (Equal e3 (mConst s)) /\ term_ok ctxt e2 ==> 1579 MilawaTrue ctxt (Equal (mApp (mPrimitiveFun logic_IF) [e1;e2;e3]) (mConst s))``, 1580 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1581 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1582 \\ IMP_RES_TAC MilawaTrue_Sym \\ MATCH_MP_TAC MilawaTrue_TRANS 1583 \\ Q.EXISTS_TAC `e3` \\ FULL_SIMP_TAC std_ss [] 1584 \\ FULL_SIMP_TAC std_ss [isTrue_def] 1585 \\ `MEM (EL 5 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1586 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 5 MILAWA_AXIOMS``] 1587 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1588 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1589 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1590 \\ `formula_ok ctxt (formula_sub [("X",e1);("Y",e2);("Z",e3)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1591 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1592 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1593 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1594 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def] 1595 \\ METIS_TAC [MilawaTrue_MP]); 1596 1597val MilawaTrue_Or_Sym = prove( 1598 ``context_ok ctxt /\ 1599 MilawaTrue ctxt (Or x y) ==> MilawaTrue ctxt (Or y x)``, 1600 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1601 \\ FULL_SIMP_TAC std_ss [formula_ok_def] \\ METIS_TAC [MilawaTrue_rules]); 1602 1603val MilawaTrue_Or_Sym_RW = prove( 1604 ``context_ok ctxt ==> 1605 (MilawaTrue ctxt (Or x y) = MilawaTrue ctxt (Or y x))``, 1606 METIS_TAC [MilawaTrue_Or_Sym]); 1607 1608val MilawaTrue_Or_ASSOC = prove( 1609 ``context_ok ctxt /\ 1610 MilawaTrue ctxt (Or x (Or y z)) ==> MilawaTrue ctxt (Or (Or x y) z)``, 1611 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1612 \\ FULL_SIMP_TAC std_ss [formula_ok_def] \\ METIS_TAC [MilawaTrue_rules]); 1613 1614val MilawaTrue_Or_ASSOC_COMM = prove( 1615 ``context_ok ctxt /\ 1616 MilawaTrue ctxt (Or x (Or y z)) ==> MilawaTrue ctxt (Or z (Or x y))``, 1617 METIS_TAC [MilawaTrue_Or_ASSOC,MilawaTrue_Or_Sym]); 1618 1619val MilawaTrue_Not_Equal = prove( 1620 ``context_ok ctxt /\ 1621 MilawaTrue ctxt (Equal x y) /\ MilawaTrue ctxt (Not (Equal y z)) ==> 1622 MilawaTrue ctxt (Not (Equal x z))``, 1623 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1624 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1625 \\ IMP_RES_TAC MilawaTrue_REFL 1626 \\ `MEM (EL 1 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1627 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 1 MILAWA_AXIOMS``] 1628 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1629 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1630 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1631 \\ `formula_ok ctxt (formula_sub [("X1",x);("X2",x);("Y1",y);("Y2",z)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1632 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1633 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1634 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1635 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def] 1636 \\ REPEAT STRIP_TAC 1637 \\ `MilawaTrue ctxt (Or (Not (Equal x z)) (Or (Not (Equal x x)) (Equal y z)))` by 1638 IMP_RES_TAC MilawaTrue_MP 1639 \\ `MilawaTrue ctxt (Or (Or (Not (Equal x z)) (Not (Equal x x))) (Equal y z))` by 1640 IMP_RES_TAC MilawaTrue_Or_ASSOC 1641 \\ `MilawaTrue ctxt (Or (Not (Equal x z)) (Not (Equal x x)))` by 1642 METIS_TAC [MilawaTrue_MP2,MilawaTrue_Or_Sym] 1643 \\ METIS_TAC [MilawaTrue_MP,MilawaTrue_Or_Sym]) |> GEN_ALL; 1644 1645val MilawaTrue_Not_Equal_COMM = prove( 1646 ``context_ok ctxt /\ 1647 MilawaTrue ctxt (Not (Equal y x)) ==> MilawaTrue ctxt (Not (Equal x y))``, 1648 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1649 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1650 \\ IMP_RES_TAC MilawaTrue_REFL 1651 \\ `MEM (EL 1 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1652 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 1 MILAWA_AXIOMS``] 1653 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1654 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1655 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1656 \\ `formula_ok ctxt (formula_sub [("X1",x);("X2",x);("Y1",y);("Y2",x)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1657 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1658 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1659 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1660 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def] 1661 \\ REPEAT STRIP_TAC 1662 \\ IMP_RES_TAC MilawaTrue_Or_ASSOC \\ POP_ASSUM (K ALL_TAC) 1663 \\ IMP_RES_TAC MilawaTrue_Or_ASSOC \\ POP_ASSUM (K ALL_TAC) 1664 \\ IMP_RES_TAC (ONCE_REWRITE_RULE [MilawaTrue_Or_Sym_RW] MilawaTrue_MP2) 1665 \\ METIS_TAC [MilawaTrue_MP,MilawaTrue_Or_Sym]) |> GEN_ALL; 1666 1667val MilawaTrue_AX2 = prove( 1668 ``context_ok ctxt ==> 1669 MilawaTrue ctxt (Equal x1 y1) ==> 1670 MilawaTrue ctxt (Equal x2 y2) ==> 1671 MilawaTrue ctxt (Equal x1 x2) ==> 1672 MilawaTrue ctxt (Equal y1 y2)``, 1673 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1674 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1675 \\ IMP_RES_TAC MilawaTrue_REFL 1676 \\ `MEM (EL 1 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1677 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 1 MILAWA_AXIOMS``] 1678 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1679 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1680 \\ Q.PAT_ABBREV_TAC `orrr = Or xx1 xx2` \\ STRIP_TAC 1681 \\ `formula_ok ctxt (formula_sub [("X1",x1);("X2",x2);("Y1",y1);("Y2",y2)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1682 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1683 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1684 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1685 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def] 1686 \\ METIS_TAC [MilawaTrue_MP,MilawaTrue_Or_Sym]) |> GEN_ALL; 1687 1688val MilawaTrue_AX4 = prove( 1689 ``context_ok ctxt /\ 1690 term_ok ctxt x /\ term_ok ctxt y ==> 1691 MilawaTrue ctxt (Or (Not (Equal x y)) 1692 (Equal (mApp (mPrimitiveFun logic_EQUAL) [x; y]) 1693 (mConst (Sym "T"))))``, 1694 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1695 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1696 \\ IMP_RES_TAC MilawaTrue_REFL 1697 \\ `MEM (EL 3 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1698 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 3 MILAWA_AXIOMS``] 1699 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1700 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1701 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1702 \\ `formula_ok ctxt (formula_sub [("X",x);("Y",y)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1703 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1704 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1705 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1706 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def]); 1707 1708val MilawaTrue_AX5 = prove( 1709 ``context_ok ctxt /\ 1710 term_ok ctxt x /\ term_ok ctxt y ==> 1711 MilawaTrue ctxt (Or (Equal x y) 1712 (Equal (mApp (mPrimitiveFun logic_EQUAL) [x; y]) 1713 (mConst (Sym "NIL"))))``, 1714 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1715 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1716 \\ IMP_RES_TAC MilawaTrue_REFL 1717 \\ `MEM (EL 4 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1718 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 4 MILAWA_AXIOMS``] 1719 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1720 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1721 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1722 \\ `formula_ok ctxt (formula_sub [("X",x);("Y",y)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1723 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1724 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1725 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1726 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def]); 1727 1728val MilawaTrue_AX5 = prove( 1729 ``context_ok ctxt /\ 1730 term_ok ctxt x /\ term_ok ctxt y ==> 1731 MilawaTrue ctxt (Or (Equal x y) 1732 (Equal (mApp (mPrimitiveFun logic_EQUAL) [x; y]) 1733 (mConst (Sym "NIL"))))``, 1734 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1735 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1736 \\ IMP_RES_TAC MilawaTrue_REFL 1737 \\ `MEM (EL 4 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1738 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 4 MILAWA_AXIOMS``] 1739 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1740 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1741 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1742 \\ `formula_ok ctxt (formula_sub [("X",x);("Y",y)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1743 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1744 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1745 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1746 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def]); 1747 1748val NOT_NIL_EQ_T = prove( 1749 ``context_ok ctxt ==> 1750 MilawaTrue ctxt (Not (Equal (mConst (Sym "NIL")) (mConst (Sym "T"))))``, 1751 STRIP_TAC 1752 \\ MATCH_MP_TAC MilawaTrue_Not_Equal_COMM 1753 \\ `MEM (EL 2 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1754 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 2 MILAWA_AXIOMS``] 1755 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1756 \\ FULL_SIMP_TAC std_ss []); 1757 1758val MilawaTrue_IF_LEMMA = prove( 1759 ``context_ok ctxt /\ 1760 MilawaTrue ctxt (Equal e1 (mConst s1)) /\ s1 <> Sym "NIL" ==> 1761 MilawaTrue ctxt (Not (Equal e1 (mConst (Sym "NIL"))))``, 1762 REPEAT STRIP_TAC \\ MATCH_MP_TAC MilawaTrue_Not_Equal 1763 \\ Q.EXISTS_TAC `mConst s1` \\ ASM_SIMP_TAC std_ss [] 1764 \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1765 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1766 \\ `term_ok ctxt (mConst (Sym "NIL"))` by EVAL_TAC 1767 \\ `MilawaTrue ctxt 1768 (Or (Equal 1769 (mApp (mPrimitiveFun logic_EQUAL) 1770 [mConst s1; mConst (Sym "NIL")]) (mConst (Sym "T"))) 1771 (Not (Equal (mConst s1) (mConst (Sym "NIL")))))` 1772 by (IMP_RES_TAC MilawaTrue_AX4 THEN IMP_RES_TAC MilawaTrue_Or_Sym) 1773 \\ MATCH_MP_TAC (GEN_ALL MilawaTrue_MP2) 1774 \\ Q.EXISTS_TAC `(Equal 1775 (mApp (mPrimitiveFun logic_EQUAL) 1776 [mConst s1; mConst (Sym "NIL")]) (mConst (Sym "T")))` 1777 \\ ASM_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 1778 \\ MATCH_MP_TAC MilawaTrue_Not_Equal 1779 \\ Q.EXISTS_TAC `mConst (Sym "NIL")` 1780 \\ ASM_SIMP_TAC std_ss [NOT_NIL_EQ_T] 1781 \\ MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 9 1782 |> Q.SPECL [`logic_EQUAL`,`[s1;Sym"NIL"]`,`ctxt`]) 1783 \\ SIMP_TAC std_ss [primitive_arity_def,LENGTH,EVAL_PRIMITIVE_def] 1784 \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss []); 1785 1786val MilawaTrue_IF2 = prove( 1787 ``context_ok ctxt /\ 1788 MilawaTrue ctxt (Equal e1 (mConst s1)) /\ isTrue s1 /\ 1789 MilawaTrue ctxt (Equal e2 (mConst s)) /\ term_ok ctxt e3 ==> 1790 MilawaTrue ctxt (Equal (mApp (mPrimitiveFun logic_IF) [e1;e2;e3]) (mConst s))``, 1791 REPEAT STRIP_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 1792 \\ FULL_SIMP_TAC std_ss [formula_ok_def] 1793 \\ IMP_RES_TAC MilawaTrue_Sym \\ MATCH_MP_TAC MilawaTrue_TRANS 1794 \\ Q.EXISTS_TAC `e2` \\ FULL_SIMP_TAC std_ss [] 1795 \\ FULL_SIMP_TAC std_ss [isTrue_def] 1796 \\ `MEM (EL 6 MILAWA_AXIOMS) MILAWA_AXIOMS` by EVAL_TAC 1797 \\ FULL_SIMP_TAC std_ss [EVAL ``EL 6 MILAWA_AXIOMS``] 1798 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 10) 1799 \\ POP_ASSUM (MP_TAC o SPEC_ALL) 1800 \\ Q.PAT_ABBREV_TAC `orrr = Or x1 x2` \\ STRIP_TAC 1801 \\ `formula_ok ctxt (formula_sub [("X",e1);("Y",e2);("Z",e3)] orrr)` by (Q.UNABBREV_TAC `orrr` \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1802 \\ IMP_RES_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 1803 \\ REPEAT (Q.PAT_X_ASSUM `!xx.bbb` (K ALL_TAC)) 1804 \\ Q.UNABBREV_TAC `orrr` \\ POP_ASSUM MP_TAC 1805 \\ SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,LOOKUP_def] 1806 \\ IMP_RES_TAC MilawaTrue_IF_LEMMA 1807 \\ METIS_TAC [MilawaTrue_MP2]); 1808 1809val MilawaTrue_or_not_equal_list = prove( 1810 ``!ts_list x. 1811 context_ok ctxt /\ 1812 (!x1 x2. MEM (x1,x2) ts_list ==> MilawaTrue ctxt (Equal x1 x2)) /\ 1813 MilawaTrue ctxt (or_not_equal_list ts_list x) ==> 1814 MilawaTrue ctxt x``, 1815 Induct \\ SIMP_TAC std_ss [or_not_equal_list_def] \\ Cases 1816 \\ FULL_SIMP_TAC std_ss [MEM,or_not_equal_list_def] \\ REPEAT STRIP_TAC 1817 \\ `MilawaTrue ctxt (Equal q r)` by FULL_SIMP_TAC std_ss [] 1818 \\ IMP_RES_TAC MilawaTrue_MP \\ METIS_TAC []); 1819 1820val M_ev_induct = IndDefLib.derive_strong_induction(M_ev_rules,M_ev_ind); 1821 1822val inst_term_def = Define ` 1823 inst_term a exp = term_sub (MAP (\v. (v,mConst (a v))) (free_vars exp)) exp`; 1824 1825val MAP_EQ = prove( 1826 ``!xs f g. (MAP f xs = MAP g xs) = EVERY (\x. f x = g x) xs``, 1827 Induct \\ SRW_TAC [] []); 1828 1829val term_sub_EQ = store_thm("term_sub_EQ", 1830 ``!x xs. (set (free_vars x) SUBSET set xs) ==> 1831 (term_sub (MAP (\v. (v,f v)) xs) x = 1832 term_sub (MAP (\v. (v,f v)) (free_vars x)) x)``, 1833 STRIP_TAC \\ completeInduct_on `logic_term_size x` 1834 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [PULL_IMP] 1835 \\ Cases_on `x` \\ FULL_SIMP_TAC std_ss [term_sub_def,free_vars_def] THEN1 1836 (FULL_SIMP_TAC std_ss [LOOKUP_def,SUBSET_DEF,MEM] 1837 \\ POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1838 \\ Induct_on `xs` \\ FULL_SIMP_TAC (srw_ss()) [LOOKUP_def] \\ METIS_TAC []) 1839 \\ FULL_SIMP_TAC (srw_ss()) [MAP_EQ,EVERY_MEM] \\ REPEAT STRIP_TAC 1840 THEN1 1841 (FULL_SIMP_TAC std_ss [AND_IMP_INTRO] 1842 \\ Q.PAT_X_ASSUM `!x.bbb` (fn th => MP_TAC (Q.SPECL [`a`,`xs`] th) 1843 THEN MP_TAC (Q.SPECL [`a`,`(FLAT (MAP (\a. free_vars a) l))`] th)) 1844 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 1845 (IMP_RES_TAC MEM_logic_term_size 1846 \\ FULL_SIMP_TAC std_ss [logic_term_size_def] \\ STRIP_TAC THEN1 DECIDE_TAC 1847 \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1848 \\ Induct_on `l` \\ FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] \\ METIS_TAC []) 1849 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1850 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 1851 (POP_ASSUM (K ALL_TAC) \\ IMP_RES_TAC MEM_logic_term_size 1852 \\ FULL_SIMP_TAC std_ss [logic_term_size_def] \\ STRIP_TAC THEN1 DECIDE_TAC 1853 \\ MATCH_MP_TAC SUBSET_TRANS 1854 \\ Q.EXISTS_TAC `set (FLAT (MAP (\a. free_vars a) l))` 1855 \\ ASM_SIMP_TAC std_ss [] 1856 \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1857 \\ Induct_on `l` \\ FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] \\ METIS_TAC []) 1858 \\ FULL_SIMP_TAC std_ss []) 1859 THEN1 1860 (Q.ABBREV_TAC `vs = l` \\ POP_ASSUM (K ALL_TAC) 1861 \\ Q.ABBREV_TAC `l = l0` \\ POP_ASSUM (K ALL_TAC) 1862 \\ FULL_SIMP_TAC std_ss [AND_IMP_INTRO] 1863 \\ Q.PAT_X_ASSUM `!x.bbb` (fn th => MP_TAC (Q.SPECL [`a`,`xs`] th) 1864 THEN MP_TAC (Q.SPECL [`a`,`(FLAT (MAP (\a. free_vars a) l))`] th)) 1865 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 1866 (IMP_RES_TAC MEM_logic_term_size 1867 \\ FULL_SIMP_TAC std_ss [logic_term_size_def] \\ STRIP_TAC THEN1 DECIDE_TAC 1868 \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1869 \\ Induct_on `l` \\ FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] \\ METIS_TAC []) 1870 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1871 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 1872 (POP_ASSUM (K ALL_TAC) \\ IMP_RES_TAC MEM_logic_term_size 1873 \\ FULL_SIMP_TAC std_ss [logic_term_size_def] \\ STRIP_TAC THEN1 DECIDE_TAC 1874 \\ MATCH_MP_TAC SUBSET_TRANS 1875 \\ Q.EXISTS_TAC `set (FLAT (MAP (\a. free_vars a) l))` 1876 \\ ASM_SIMP_TAC std_ss [] 1877 \\ POP_ASSUM (K ALL_TAC) \\ POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1878 \\ Induct_on `l` \\ FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] \\ METIS_TAC []) 1879 \\ FULL_SIMP_TAC std_ss [])); 1880 1881val inst_term_thm = prove( 1882 ``(inst_term a (mConst c) = mConst c) /\ 1883 (inst_term a (mVar v) = mConst (a v)) /\ 1884 (inst_term a (mApp f xs) = mApp f (MAP (inst_term a) xs)) /\ 1885 (inst_term a (mLamApp vs x xs) = mLamApp vs x (MAP (inst_term a) xs))``, 1886 SIMP_TAC std_ss [inst_term_def,free_vars_def,MAP,term_sub_def,LOOKUP_def] 1887 \\ SIMP_TAC (srw_ss()) [MAP_EQ] 1888 \\ SIMP_TAC std_ss [EVERY_MEM,inst_term_def] \\ REPEAT STRIP_TAC 1889 \\ HO_MATCH_MP_TAC term_sub_EQ 1890 \\ Induct_on `xs` \\ FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 1891 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,IN_UNION]); 1892 1893val MAP_FST_ZIP = prove( 1894 ``!xs ys. (LENGTH xs = LENGTH ys) ==> (MAP FST (ZIP (xs,ys)) = xs)``, 1895 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ZIP,MAP]); 1896 1897val MAP_SND_ZIP = prove( 1898 ``!xs ys. (LENGTH xs = LENGTH ys) ==> (MAP SND (ZIP (xs,ys)) = ys)``, 1899 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ZIP,MAP]); 1900 1901val formula_ok_or_not_equal_list = prove( 1902 ``!xs x. 1903 formula_ok ctxt x /\ EVERY (\(x,y). term_ok ctxt y /\ term_ok ctxt x) xs ==> 1904 formula_ok ctxt (or_not_equal_list xs x)``, 1905 Induct \\ ASM_SIMP_TAC std_ss [or_not_equal_list_def,EVERY_DEF] 1906 \\ Cases \\ ASM_SIMP_TAC std_ss [or_not_equal_list_def,EVERY_DEF,formula_ok_def]); 1907 1908val EVERY_ZIP = prove( 1909 ``!xs ys. (LENGTH xs = LENGTH ys) ==> 1910 (EVERY (\(x,y). g y /\ f x) (ZIP (xs,ys)) = EVERY f xs /\ EVERY g ys)``, 1911 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ZIP,MAP,EVERY_DEF] 1912 \\ METIS_TAC []); 1913 1914val MEM_ZIP = prove( 1915 ``!xs ys x. MEM x xs /\ (LENGTH xs = LENGTH ys) ==> ?y. MEM (x,y) (ZIP (xs,ys))``, 1916 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ZIP,MAP,MEM] 1917 \\ METIS_TAC []); 1918 1919val MEM_ZIP2 = prove( 1920 ``!xs ys x. MEM x xs /\ (LENGTH xs = LENGTH ys) ==> ?y. MEM (y,x) (ZIP (ys,xs))``, 1921 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ZIP,MAP,MEM] 1922 \\ METIS_TAC []); 1923 1924val ZIP_MAP = prove( 1925 ``!xs ys f g. 1926 (LENGTH xs = LENGTH ys) ==> 1927 (ZIP (MAP f xs, MAP g ys) = MAP (\(x,y). (f x, g y)) (ZIP (xs,ys)))``, 1928 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ZIP,MAP,MEM]); 1929 1930val term_ok_inst_term = prove( 1931 ``!exp. term_ok ctxt exp ==> term_ok ctxt (inst_term a exp)``, 1932 REPEAT STRIP_TAC \\ SIMP_TAC std_ss [inst_term_def] 1933 \\ MATCH_MP_TAC term_ok_sub \\ FULL_SIMP_TAC std_ss [] 1934 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP,term_ok_def]); 1935 1936val MEM_ZIP_IMP = prove( 1937 ``!xs ys. 1938 MEM (x,y) (ZIP (xs,ys)) /\ (LENGTH xs = LENGTH ys) ==> MEM x xs /\ MEM y ys``, 1939 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ZIP,MAP,MEM] 1940 \\ METIS_TAC []); 1941 1942val MAP_LOOKUP_LEMMA = store_thm("MAP_LOOKUP_LEMMA", 1943 ``!args params. 1944 (LENGTH args = LENGTH params) /\ ALL_DISTINCT params ==> 1945 (MAP mConst args = 1946 MAP (\x. LOOKUP x (ZIP (params,MAP mConst args)) (mVar x)) params)``, 1947 Induct \\ Cases_on `params` \\ SIMP_TAC (srw_ss()) [LENGTH,ADD1,LOOKUP_def] 1948 \\ REPEAT STRIP_TAC \\ RES_TAC 1949 \\ POP_ASSUM (fn th => CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [th]))) 1950 \\ SIMP_TAC std_ss [MAP_EQ,EVERY_MEM] \\ REPEAT STRIP_TAC 1951 \\ SRW_TAC [] [] \\ FULL_SIMP_TAC std_ss []); 1952 1953val MAP_FunVarBind_LEMMA = store_thm("MAP_FunVarBind_LEMMA", 1954 ``!params args. 1955 (LENGTH params = LENGTH args) /\ ALL_DISTINCT params ==> 1956 (MAP (\v. (v,mConst (FunVarBind params args v))) params = 1957 ZIP (params,MAP mConst args))``, 1958 Induct \\ Cases_on `args` \\ SIMP_TAC (srw_ss()) [LENGTH,ADD1,FunVarBind_def] 1959 \\ SIMP_TAC std_ss [APPLY_UPDATE_THM] \\ REPEAT STRIP_TAC 1960 \\ sg `MAP (\v. (v,mConst (if h' = v then h else FunVarBind params t v))) 1961 params = MAP (\v. (v,mConst (FunVarBind params t v))) params` 1962 \\ SIMP_TAC std_ss [MAP_EQ,EVERY_MEM] \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []); 1963 1964val inst_term_EQ_term_sub = prove( 1965 ``!xs sl. 1966 set (free_vars e) SUBSET set xs /\ (LENGTH xs = LENGTH sl) ==> 1967 (inst_term (FunVarBind xs sl) e = term_sub (ZIP (xs,MAP mConst sl)) e)``, 1968 completeInduct_on `logic_term_size e` \\ REPEAT STRIP_TAC 1969 \\ FULL_SIMP_TAC std_ss [PULL_IMP] \\ Cases_on `e` 1970 THEN1 (SIMP_TAC std_ss [inst_term_thm,term_sub_def,MilawaTrue_REFL,term_ok_def]) 1971 THEN1 1972 (SIMP_TAC std_ss [inst_term_thm,term_sub_def] 1973 \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 1974 \\ SIMP_TAC std_ss [free_vars_def,SUBSET_DEF,MEM] 1975 \\ Q.SPEC_TAC (`xs`,`xs`) \\ Q.SPEC_TAC (`sl`,`ys`) 1976 \\ Induct \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,MEM] 1977 \\ FULL_SIMP_TAC std_ss [FunVarBind_def,APPLY_UPDATE_THM,MAP,ZIP,LOOKUP_def] 1978 \\ METIS_TAC []) 1979 THEN 1980 (FULL_SIMP_TAC (srw_ss()) [inst_term_thm,term_sub_def,MAP_EQ,EVERY_MEM] 1981 \\ FULL_SIMP_TAC std_ss [free_vars_def] \\ REPEAT STRIP_TAC 1982 \\ FULL_SIMP_TAC std_ss [AND_IMP_INTRO] 1983 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ FULL_SIMP_TAC std_ss [] 1984 \\ IMP_RES_TAC MEM_logic_term_size 1985 \\ STRIP_TAC THEN1 (EVAL_TAC \\ DECIDE_TAC) 1986 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF,MEM_FLAT,PULL_IMP,MEM_MAP] 1987 \\ METIS_TAC [])); 1988 1989val MEM_ZIP_ID = prove( 1990 ``!xs x y. MEM (x,y) (ZIP(xs,xs)) ==> (x = y)``, 1991 Induct \\ SIMP_TAC (srw_ss()) [ZIP] \\ METIS_TAC []); 1992 1993val Equal_term_sub = prove( 1994 ``!vs xs ys. 1995 context_ok ctxt /\ 1996 term_ok ctxt x /\ (LENGTH vs = LENGTH ys) /\ (LENGTH vs = LENGTH xs) /\ 1997 (!x y. MEM (x,y) (ZIP(xs,ys)) ==> MilawaTrue ctxt (Equal x y)) ==> 1998 MilawaTrue ctxt (Equal (term_sub (ZIP (vs,xs)) x) (term_sub (ZIP(vs,ys)) x))``, 1999 completeInduct_on `logic_term_size x` \\ REPEAT STRIP_TAC 2000 \\ FULL_SIMP_TAC std_ss [PULL_IMP] \\ Cases_on `x` 2001 THEN1 (SIMP_TAC std_ss [term_sub_def,MilawaTrue_REFL,term_ok_def]) 2002 THEN1 2003 (POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 2004 \\ REPEAT (POP_ASSUM (K ALL_TAC)) 2005 \\ Q.SPEC_TAC (`xs`,`xs`) \\ Q.SPEC_TAC (`ys`,`ys`) \\ Q.SPEC_TAC (`vs`,`vs`) 2006 \\ Induct \\ Cases_on `xs` \\ Cases_on `ys` 2007 \\ FULL_SIMP_TAC (srw_ss()) [LENGTH,ADD1,term_sub_def,LOOKUP_def] 2008 THEN1 (SIMP_TAC std_ss [term_sub_def,MilawaTrue_REFL,term_ok_def]) 2009 \\ REPEAT STRIP_TAC \\ Cases_on `s = h''` \\ ASM_SIMP_TAC std_ss []) 2010 THEN1 2011 (SIMP_TAC std_ss [term_sub_def] 2012 \\ MATCH_MP_TAC MilawaTrue_or_not_equal_list 2013 \\ Q.LIST_EXISTS_TAC [`ZIP (MAP (\a. term_sub (ZIP (vs,xs)) a) l, 2014 MAP (\a. term_sub (ZIP (vs,ys)) a) l)`] 2015 \\ ASM_SIMP_TAC std_ss [] 2016 \\ STRIP_TAC THEN1 2017 (SIMP_TAC std_ss [ZIP_MAP,MEM_MAP,pairTheory.EXISTS_PROD,PULL_IMP] 2018 \\ REPEAT STRIP_TAC 2019 \\ IMP_RES_TAC MEM_ZIP_ID \\ FULL_SIMP_TAC std_ss [AND_IMP_INTRO] 2020 \\ Q.PAT_X_ASSUM `!x1 x2 x3. bbb` MATCH_MP_TAC \\ IMP_RES_TAC MEM_ZIP_IMP 2021 \\ FULL_SIMP_TAC std_ss [term_ok_def,EVERY_MEM] 2022 \\ IMP_RES_TAC MEM_logic_term_size \\ EVAL_TAC \\ DECIDE_TAC) 2023 \\ MATCH_MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 6) 2024 \\ Q.LIST_EXISTS_TAC [`l0`,`ZIP (MAP (\a. term_sub (ZIP (vs,xs)) a) l, 2025 MAP (\a. term_sub (ZIP (vs,ys)) a) l)`] 2026 \\ FULL_SIMP_TAC std_ss [MAP_FST_ZIP,MAP_SND_ZIP,LENGTH_MAP] 2027 \\ MATCH_MP_TAC formula_ok_or_not_equal_list 2028 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP,EVERY_ZIP] 2029 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP] 2030 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC term_ok_sub 2031 \\ ASM_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,pairTheory.EXISTS_PROD,PULL_IMP] 2032 \\ REPEAT STRIP_TAC 2033 \\ `LENGTH ys = LENGTH xs` by METIS_TAC [] 2034 \\ `LENGTH vs = LENGTH ys` by METIS_TAC [] 2035 \\ IMP_RES_TAC MEM_ZIP_IMP 2036 THENL [IMP_RES_TAC MEM_ZIP, IMP_RES_TAC MEM_ZIP2] 2037 \\ RES_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2038 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP]) 2039 THEN1 2040 (SIMP_TAC std_ss [term_sub_def] 2041 \\ MATCH_MP_TAC (MilawaTrue_AX2 |> SIMP_RULE std_ss [AND_IMP_INTRO]) 2042 \\ Q.ABBREV_TAC `xs1 = MAP (\a. term_sub (ZIP (vs,xs)) a) l0` 2043 \\ Q.ABBREV_TAC `ys1 = MAP (\a. term_sub (ZIP (vs,ys)) a) l0` 2044 \\ Q.LIST_EXISTS_TAC [`term_sub (ZIP(l1,ys1)) l`,`term_sub (ZIP(l1,xs1)) l`] 2045 \\ ASM_SIMP_TAC std_ss [] 2046 \\ REPEAT STRIP_TAC THEN1 2047 (MATCH_MP_TAC MilawaTrue_Sym \\ ASM_SIMP_TAC std_ss [] 2048 \\ MATCH_MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 8) 2049 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def] 2050 \\ Q.UNABBREV_TAC `xs1` \\ Q.UNABBREV_TAC `ys1` 2051 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP,LENGTH_MAP] 2052 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC term_ok_sub 2053 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,pairTheory.EXISTS_PROD,PULL_IMP] 2054 \\ REPEAT STRIP_TAC 2055 \\ `LENGTH ys = LENGTH xs` by METIS_TAC [] 2056 \\ `LENGTH vs = LENGTH ys` by METIS_TAC [] 2057 THEN1 2058 (IMP_RES_TAC MEM_ZIP_IMP \\ IMP_RES_TAC MEM_ZIP 2059 \\ RES_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2060 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP]) 2061 \\ Q.PAT_X_ASSUM `MEM (p_1,e) (ZIP (l1,MAP (\a. term_sub (ZIP (vs,xs)) a) l0))` MP_TAC 2062 \\ ASM_SIMP_TAC std_ss [MEM_MAP,pairTheory.EXISTS_PROD, 2063 ZIP_MAP |> Q.SPECL [`xs`,`ys`] |> Q.ISPEC `I` |> SIMP_RULE std_ss [MAP_ID]] 2064 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2065 \\ MATCH_MP_TAC term_ok_sub 2066 \\ IMP_RES_TAC MEM_ZIP_IMP \\ FULL_SIMP_TAC std_ss [] 2067 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,pairTheory.EXISTS_PROD,PULL_IMP] 2068 \\ REPEAT STRIP_TAC \\ `LENGTH vs = LENGTH xs` by METIS_TAC [] 2069 \\ IMP_RES_TAC MEM_ZIP_IMP \\ FULL_SIMP_TAC std_ss [] 2070 \\ IMP_RES_TAC MEM_ZIP_IMP \\ IMP_RES_TAC MEM_ZIP 2071 \\ RES_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2072 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP]) 2073 THEN1 2074 (MATCH_MP_TAC MilawaTrue_Sym \\ ASM_SIMP_TAC std_ss [] 2075 \\ MATCH_MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 8) 2076 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def] 2077 \\ Q.UNABBREV_TAC `xs1` \\ Q.UNABBREV_TAC `ys1` 2078 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP,LENGTH_MAP] 2079 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC term_ok_sub 2080 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,pairTheory.EXISTS_PROD,PULL_IMP] 2081 \\ REPEAT STRIP_TAC 2082 \\ `LENGTH ys = LENGTH xs` by METIS_TAC [] 2083 \\ `LENGTH vs = LENGTH ys` by METIS_TAC [] 2084 THEN1 2085 (IMP_RES_TAC MEM_ZIP_IMP \\ IMP_RES_TAC MEM_ZIP2 2086 \\ RES_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2087 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP]) 2088 \\ Q.PAT_X_ASSUM `MEM (p_1,e) (ZIP (l1,MAP (\a. term_sub (ZIP (vs,ys)) a) l0))` MP_TAC 2089 \\ ASM_SIMP_TAC std_ss [MEM_MAP,pairTheory.EXISTS_PROD, 2090 ZIP_MAP |> Q.SPECL [`xs`,`ys`] |> Q.ISPEC `I` |> SIMP_RULE std_ss [MAP_ID]] 2091 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2092 \\ MATCH_MP_TAC term_ok_sub 2093 \\ IMP_RES_TAC MEM_ZIP_IMP \\ FULL_SIMP_TAC std_ss [] 2094 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,pairTheory.EXISTS_PROD,PULL_IMP] 2095 \\ REPEAT STRIP_TAC \\ `LENGTH vs = LENGTH ys` by METIS_TAC [] 2096 \\ IMP_RES_TAC MEM_ZIP_IMP \\ FULL_SIMP_TAC std_ss [] 2097 \\ IMP_RES_TAC MEM_ZIP_IMP \\ IMP_RES_TAC MEM_ZIP2 2098 \\ RES_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2099 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP]) 2100 \\ FULL_SIMP_TAC std_ss [AND_IMP_INTRO] 2101 \\ Q.PAT_X_ASSUM `!x1 x2 x3. bbb` (fn th => ASSUME_TAC th THEN MATCH_MP_TAC th) 2102 \\ STRIP_TAC THEN1 (EVAL_TAC \\ DECIDE_TAC) 2103 \\ Q.UNABBREV_TAC `xs1` \\ Q.UNABBREV_TAC `ys1` 2104 \\ FULL_SIMP_TAC std_ss [term_ok_def,LENGTH_MAP,ZIP_MAP,MEM_MAP, 2105 PULL_IMP,pairTheory.FORALL_PROD] \\ REPEAT STRIP_TAC 2106 \\ IMP_RES_TAC MEM_ZIP_ID \\ FULL_SIMP_TAC std_ss [] 2107 \\ Q.PAT_X_ASSUM `!x1 x2 x3. bbb` MATCH_MP_TAC 2108 \\ ASM_SIMP_TAC std_ss [] \\ IMP_RES_TAC MEM_ZIP_IMP 2109 \\ FULL_SIMP_TAC std_ss [EVERY_MEM] 2110 \\ IMP_RES_TAC MEM_logic_term_size 2111 \\ EVAL_TAC \\ DECIDE_TAC)); 2112 2113val MEM_ZIP_MAP_EQ = prove( 2114 ``!xs ys. 2115 (LENGTH xs = LENGTH ys) ==> 2116 (MEM (x,y) (ZIP (MAP f xs, MAP g ys)) = 2117 ?x1 y1. MEM (x1,y1) (ZIP(xs,ys)) /\ (x = f x1) /\ (y = g y1))``, 2118 Induct \\ Cases_on `ys` 2119 \\ FULL_SIMP_TAC (srw_ss()) [LENGTH,ADD1] \\ METIS_TAC []); 2120 2121val term_funs_def = Define ` 2122 term_funs ctxt = 2123 !name params body sem. 2124 name IN FDOM ctxt /\ (ctxt ' name = (params,BODY_FUN body,sem)) ==> 2125 MilawaTrue ctxt (Equal (mApp (mFun name) (MAP mVar params)) body)`; 2126 2127val proof_in_full_ctxt_def = Define ` 2128 proof_in_full_ctxt ctxt full_ctxt = 2129 !x. MilawaTrue ctxt x ==> MilawaTrue full_ctxt x`; 2130 2131val ind = 2132 M_ev_induct 2133 |> Q.SPEC `name` 2134 |> Q.SPEC `\(exp,a,ctxt) result. !ok env. 2135 (!params exp sem. 2136 (ctxt ' name = (params,BODY_FUN exp,sem)) /\ 2137 name IN FDOM ctxt ==> 2138 ?r. (k ' name = (params,r)) /\ name IN FDOM k /\ 2139 term_ok ctxt exp /\ (term2t r = exp) /\ funcs_ok r) /\ 2140 term_funs ctxt /\ 2141 runtime_inv (ctxt \\ name) k /\ proof_in_full_ctxt (ctxt \\ name) ctxt /\ 2142 EVERY (\x. ~(x IN FDOM ctxt)) ["NOT";"RANK";"ORDP";"ORD<"] /\ 2143 EVERY (\x. ~(x IN FDOM ctxt)) fake_ftbl_entries /\ 2144 context_ok ctxt /\ term_ok ctxt exp /\ core_assum k /\ 2145 (!v. MEM v (free_vars exp) ==> v IN FDOM env /\ (env ' v = a v)) ==> 2146 ?ok2. MR_ev (t2term exp,env,ctxt,k,ok) (result,ok2) /\ 2147 (ok2 ==> MilawaTrue ctxt (Equal (inst_term a exp) (mConst result)))` 2148 |> Q.SPEC `\(f,args,ctxt) result. !ok env. 2149 (!params exp sem. 2150 (ctxt ' name = (params,BODY_FUN exp,sem)) /\ 2151 name IN FDOM ctxt ==> 2152 ?r. (k ' name = (params,r)) /\ name IN FDOM k /\ 2153 term_ok ctxt exp /\ (term2t r = exp) /\ funcs_ok r) /\ 2154 term_funs ctxt /\ 2155 runtime_inv (ctxt \\ name) k /\ proof_in_full_ctxt (ctxt \\ name) ctxt /\ 2156 EVERY (\x. ~(x IN FDOM ctxt)) ["NOT";"RANK";"ORDP";"ORD<"] /\ 2157 EVERY (\x. ~(x IN FDOM ctxt)) fake_ftbl_entries /\ 2158 context_ok ctxt /\ core_assum k /\ 2159 ~(f = mPrimitiveFun logic_IF) ==> 2160 ?ok2. MR_ap (f2func f,args,ARB,ctxt,k,ok) (result,ok2) /\ 2161 (ok2 ==> MilawaTrue ctxt (Equal (mApp f (MAP mConst args)) (mConst result)))` 2162 |> Q.SPEC `\(exp,a,ctxt) result. !ok env. 2163 (!params exp sem. 2164 (ctxt ' name = (params,BODY_FUN exp,sem)) /\ 2165 name IN FDOM ctxt ==> 2166 ?r. (k ' name = (params,r)) /\ name IN FDOM k /\ 2167 term_ok ctxt exp /\ (term2t r = exp) /\ funcs_ok r) /\ 2168 term_funs ctxt /\ 2169 runtime_inv (ctxt \\ name) k /\ proof_in_full_ctxt (ctxt \\ name) ctxt /\ 2170 EVERY (\x. ~(x IN FDOM ctxt)) ["NOT";"RANK";"ORDP";"ORD<"] /\ 2171 EVERY (\x. ~(x IN FDOM ctxt)) fake_ftbl_entries /\ 2172 context_ok ctxt /\ EVERY (term_ok ctxt) exp /\ core_assum k /\ 2173 (!v. MEM v (FLAT (MAP free_vars exp)) ==> v IN FDOM env /\ (env ' v = a v)) ==> 2174 ?ok2. MR_evl (MAP t2term exp,env,ctxt,k,ok) (result,ok2) /\ 2175 (ok2 ==> !x1 x2. MEM (x1,x2) (ZIP (exp,result)) ==> 2176 MilawaTrue ctxt (Equal (inst_term a x1) (mConst x2)))` 2177 2178val goal = ind |> concl |> dest_comb |> snd 2179 2180(* 2181 set_goal([],goal) 2182*) 2183 2184val M_ev_IMP_R_ev_lemma = prove(goal, 2185 MATCH_MP_TAC ind \\ SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2186 THEN1 (SIMP_TAC std_ss [t2term_def] \\ ONCE_REWRITE_TAC [MR_ev_cases] 2187 \\ SIMP_TAC (srw_ss()) [] 2188 \\ SIMP_TAC std_ss [inst_term_def,term_sub_def,MilawaTrue_REFL,term_ok_def]) 2189 THEN1 (SIMP_TAC std_ss [t2term_def] \\ ONCE_REWRITE_TAC [MR_ev_cases] 2190 \\ FULL_SIMP_TAC (srw_ss()) [free_vars_def,MEM] 2191 \\ FULL_SIMP_TAC std_ss [inst_term_def,free_vars_def,MAP, 2192 term_sub_def,LOOKUP_def,MilawaTrue_REFL,term_ok_def]) 2193 THEN1 (FULL_SIMP_TAC (srw_ss()) [term_ok_def,EVERY_DEF,free_vars_def, 2194 MAP,FLAT,MEM_APPEND,MEM,t2term_def,LENGTH,LET_DEF] 2195 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC (srw_ss()) [] 2196 \\ `?ok2. MR_ev (t2term e1,env,ctxt,k,ok) (s1,ok2) /\ 2197 (ok2 ==> MilawaTrue ctxt (Equal (inst_term a e1) (mConst s1)))` 2198 by METIS_TAC [] 2199 \\ `?ok3. MR_ev (t2term e3,env,ctxt,k,ok2) (s,ok3) /\ 2200 (ok3 ==> MilawaTrue ctxt (Equal (inst_term a e3) (mConst s)))` 2201 by METIS_TAC [] 2202 \\ Q.EXISTS_TAC `ok3` \\ STRIP_TAC THEN1 (METIS_TAC []) 2203 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2204 \\ IMP_RES_TAC MR_ev_OK \\ FULL_SIMP_TAC std_ss [inst_term_thm,MAP] 2205 \\ MATCH_MP_TAC MilawaTrue_IF1 \\ ASM_SIMP_TAC std_ss [term_ok_inst_term]) 2206 THEN1 (FULL_SIMP_TAC (srw_ss()) [term_ok_def,EVERY_DEF,free_vars_def, 2207 MAP,FLAT,MEM_APPEND,MEM,t2term_def,LENGTH,LET_DEF] 2208 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC (srw_ss()) [] 2209 \\ `?ok2. MR_ev (t2term e1,env,ctxt,k,ok) (s1,ok2) /\ 2210 (ok2 ==> MilawaTrue ctxt (Equal (inst_term a e1) (mConst s1)))` 2211 by METIS_TAC [] 2212 \\ `?ok3. MR_ev (t2term e2,env,ctxt,k,ok2) (s,ok3) /\ 2213 (ok3 ==> MilawaTrue ctxt (Equal (inst_term a e2) (mConst s)))` 2214 by METIS_TAC [] 2215 \\ Q.EXISTS_TAC `ok3` \\ STRIP_TAC THEN1 (METIS_TAC []) 2216 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2217 \\ IMP_RES_TAC MR_ev_OK \\ FULL_SIMP_TAC std_ss [inst_term_thm,MAP] 2218 \\ MATCH_MP_TAC MilawaTrue_IF2 \\ ASM_SIMP_TAC std_ss [term_ok_inst_term]) 2219 THEN1 2220 (SIMP_TAC std_ss [t2term_def] 2221 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [] 2222 \\ FULL_SIMP_TAC std_ss [free_vars_def,term_ok_def,EVERY_MEM] 2223 \\ POP_ASSUM MP_TAC \\ CONV_TAC (DEPTH_CONV ETA_CONV) \\ STRIP_TAC 2224 \\ FULL_SIMP_TAC std_ss [] 2225 \\ Q.PAT_X_ASSUM `!ok:bool. bbb` MP_TAC 2226 \\ Q.PAT_X_ASSUM `!ok:bool. bbb` (MP_TAC o Q.SPECL [`ok`,`env`]) 2227 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2228 \\ POP_ASSUM (MP_TAC o Q.SPECL [`ok2`,`FUNION (VarBind xs sl) env`]) 2229 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2230 (NTAC 2 STRIP_TAC 2231 \\ IMP_RES_TAC MR_evl_LENGTH 2232 \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] \\ RES_TAC 2233 \\ MP_TAC (Q.SPECL [`xs`,`sl`,`v`] params_lemma) \\ ASM_SIMP_TAC std_ss [] 2234 \\ FULL_SIMP_TAC std_ss [FUNION_DEF,LENGTH_MAP,IN_UNION]) 2235 \\ REPEAT STRIP_TAC 2236 \\ Q.EXISTS_TAC `ok2'` \\ STRIP_TAC THEN1 METIS_TAC [] 2237 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2238 \\ IMP_RES_TAC MR_ev_OK \\ FULL_SIMP_TAC std_ss [inst_term_thm] 2239 \\ MATCH_MP_TAC MilawaTrue_TRANS \\ ASM_SIMP_TAC std_ss [] 2240 \\ Q.EXISTS_TAC `(inst_term (FunVarBind xs sl) e)` \\ ASM_SIMP_TAC std_ss [] 2241 \\ MATCH_MP_TAC MilawaTrue_TRANS \\ ASM_SIMP_TAC std_ss [] 2242 \\ Q.EXISTS_TAC `term_sub (ZIP (xs,(MAP (inst_term a) ys))) e` 2243 \\ STRIP_TAC THEN1 2244 (FULL_SIMP_TAC std_ss [] 2245 \\ MATCH_MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 8) 2246 \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2247 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP, 2248 EVERY_MEM,MEM_MAP,PULL_IMP,term_ok_inst_term] 2249 \\ MATCH_MP_TAC term_ok_sub 2250 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP, 2251 EVERY_MEM,MEM_MAP,PULL_IMP,term_ok_inst_term] \\ Cases 2252 \\ ASM_SIMP_TAC std_ss [MEM_MAP,pairTheory.EXISTS_PROD, 2253 ZIP_MAP |> Q.SPECL [`xs`,`ys`] |> Q.ISPEC `I` |> SIMP_RULE std_ss [MAP_ID]] 2254 \\ REPEAT STRIP_TAC \\ RES_TAC \\ IMP_RES_TAC MEM_ZIP_IMP 2255 \\ FULL_SIMP_TAC std_ss [term_ok_inst_term]) 2256 \\ IMP_RES_TAC MR_evl_LENGTH \\ FULL_SIMP_TAC std_ss [LENGTH_MAP] 2257 \\ FULL_SIMP_TAC std_ss [inst_term_EQ_term_sub] 2258 \\ MATCH_MP_TAC Equal_term_sub \\ FULL_SIMP_TAC std_ss [LENGTH_MAP] 2259 \\ IMP_RES_TAC MR_evl_LENGTH \\ FULL_SIMP_TAC std_ss [LENGTH_MAP] 2260 \\ FULL_SIMP_TAC std_ss [MEM_ZIP_MAP_EQ,PULL_IMP]) 2261 THEN1 2262 (SIMP_TAC std_ss [t2term_def] 2263 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) [] 2264 \\ FULL_SIMP_TAC std_ss [free_vars_def,term_ok_def] 2265 \\ NTAC 3 (POP_ASSUM MP_TAC) \\ CONV_TAC (DEPTH_CONV ETA_CONV) 2266 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2267 \\ Q.PAT_X_ASSUM `!ok env. bb ==> bbb` (MP_TAC o Q.SPECL [`ok`,`env`]) 2268 \\ FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2269 \\ FULL_SIMP_TAC std_ss [MR_ap_ARB] 2270 \\ Q.PAT_X_ASSUM `!ok. ?ok2. bbb` (STRIP_ASSUME_TAC o Q.SPEC `ok2`) 2271 \\ Q.EXISTS_TAC `ok2'` \\ STRIP_TAC THEN1 METIS_TAC [] 2272 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2273 \\ IMP_RES_TAC MR_ev_OK \\ FULL_SIMP_TAC std_ss [inst_term_thm] 2274 \\ MATCH_MP_TAC MilawaTrue_TRANS 2275 \\ Q.EXISTS_TAC `mApp fc (MAP mConst args)` \\ ASM_SIMP_TAC std_ss [] 2276 \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2277 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP] 2278 \\ MATCH_MP_TAC MilawaTrue_or_not_equal_list \\ ASM_SIMP_TAC std_ss [] 2279 \\ Q.LIST_EXISTS_TAC [`ZIP (MAP (inst_term a) el,MAP mConst args)`] 2280 \\ STRIP_TAC THEN1 2281 (ASM_SIMP_TAC std_ss [ZIP_MAP,MEM_MAP,pairTheory.EXISTS_PROD,PULL_IMP]) 2282 \\ MATCH_MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 6) 2283 \\ Q.LIST_EXISTS_TAC [`fc`,`ZIP (MAP (inst_term a) el,MAP mConst args)`] 2284 \\ FULL_SIMP_TAC std_ss [MAP_FST_ZIP,MAP_SND_ZIP,LENGTH_MAP] 2285 \\ MATCH_MP_TAC formula_ok_or_not_equal_list 2286 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP,EVERY_ZIP] 2287 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP] 2288 \\ REPEAT STRIP_TAC 2289 \\ `?x. MEM (y,x) (ZIP (el,args))` by METIS_TAC [MEM_ZIP] 2290 \\ RES_TAC \\ IMP_RES_TAC MilawaTrue_IMP_formula_ok 2291 \\ FULL_SIMP_TAC std_ss [formula_ok_def,term_ok_def,LENGTH_MAP]) 2292 THEN1 2293 (Q.EXISTS_TAC `ok` \\ REVERSE STRIP_TAC THEN1 2294 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2295 \\ METIS_TAC [MilawaTrue_cases]) 2296 \\ Cases_on `p` \\ FULL_SIMP_TAC std_ss [f2func_def] 2297 \\ TRY (ONCE_REWRITE_TAC [MR_ev_cases] 2298 \\ SIMP_TAC (srw_ss()) [EVAL_DATA_OP_def,EVAL_PRIMITIVE_def] 2299 \\ FULL_SIMP_TAC std_ss [primitive_arity_def] \\ NO_TAC) 2300 \\ FULL_SIMP_TAC std_ss [primitive_arity_def] 2301 \\ FULL_SIMP_TAC std_ss [LENGTH_EQ_2,LENGTH_EQ_1] 2302 \\ `EVAL_PRIMITIVE logic_NOT [x1] = not x1` by 2303 (FULL_SIMP_TAC (srw_ss()) [EVAL_PRIMITIVE_def,LISP_TEST_def, 2304 not_def,isTrue_def] \\ METIS_TAC []) 2305 \\ `EVAL_PRIMITIVE logic_RANK [x1] = rank x1` by 2306 (FULL_SIMP_TAC (srw_ss()) [EVAL_PRIMITIVE_def,LISP_TEST_def, 2307 not_def,isTrue_def,rank_lemma]) 2308 \\ `EVAL_PRIMITIVE logic_ORD_LESS [x1; x2] = ord_ x1 x2` by 2309 (FULL_SIMP_TAC (srw_ss()) [EVAL_PRIMITIVE_def,ord__lemma]) 2310 \\ `EVAL_PRIMITIVE logic_ORDP [x1] = ordp x1` by 2311 (FULL_SIMP_TAC (srw_ss()) [EVAL_PRIMITIVE_def,ordp_lemma]) 2312 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ FULL_SIMP_TAC (srw_ss()) []) 2313 THEN1 2314 (SIMP_TAC std_ss [f2func_def] 2315 \\ `~(fc = "DEFINE") /\ ~(fc = "PRINT") /\ 2316 ~(fc = "ERROR") /\ ~(fc = "FUNCALL")` by 2317 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [EVERY_DEF,fake_ftbl_entries_def]) 2318 \\ FULL_SIMP_TAC std_ss [] 2319 \\ FULL_SIMP_TAC std_ss [runtime_inv_def,FDOM_DOMSUB,DOMSUB_FAPPLY_THM,IN_DELETE] 2320 \\ Q.PAT_X_ASSUM `!bb.nnn` (MP_TAC o Q.SPECL [`fc`]) 2321 \\ FULL_SIMP_TAC std_ss [] 2322 \\ STRIP_TAC \\ POP_ASSUM (MP_TAC o Q.SPECL [`args`,`ok`]) 2323 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2324 \\ Q.EXISTS_TAC `ok2` \\ STRIP_TAC THEN1 METIS_TAC [MR_ev_CTXT] 2325 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2326 \\ FULL_SIMP_TAC std_ss [MilawaTrueFun_def] 2327 \\ FULL_SIMP_TAC std_ss [proof_in_full_ctxt_def]) 2328 THEN1 2329 (SIMP_TAC std_ss [f2func_def] 2330 \\ `~(name = "DEFINE") /\ ~(name = "PRINT") /\ 2331 ~(name = "ERROR") /\ ~(name = "FUNCALL")` by 2332 (REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [EVERY_DEF,fake_ftbl_entries_def]) 2333 \\ FULL_SIMP_TAC std_ss [] 2334 \\ FULL_SIMP_TAC std_ss [EVERY_DEF] 2335 \\ `~(name = "NOT") /\ ~(name = "ORDP") /\ 2336 ~(name = "RANK") /\ ~(name = "ORD<")` by METIS_TAC [] 2337 \\ ONCE_REWRITE_TAC [MR_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [] 2338 \\ FULL_SIMP_TAC (srw_ss()) [] 2339 \\ Q.PAT_X_ASSUM `term2t r = exp` (ASSUME_TAC o GSYM) 2340 \\ FULL_SIMP_TAC (srw_ss()) [] 2341 \\ Q.PAT_X_ASSUM `!ok env. bbb` (MP_TAC o Q.SPECL [`ok`,`VarBind params args`]) 2342 \\ FULL_SIMP_TAC (srw_ss()) [] 2343 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2344 (FULL_SIMP_TAC std_ss [context_ok_def] 2345 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [SUBSET_DEF] 2346 \\ METIS_TAC [params_lemma]) 2347 \\ STRIP_TAC \\ FULL_SIMP_TAC std_ss [GSYM term2term_def] 2348 \\ IMP_RES_TAC (GEN_ALL MR_ev_term2term) 2349 \\ Q.EXISTS_TAC `ok2` \\ FULL_SIMP_TAC std_ss [] 2350 \\ STRIP_TAC THEN1 2351 (CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [] 2352 \\ FULL_SIMP_TAC std_ss [term2t_def,term_ok_def,func_arity_def,func2f_def] 2353 \\ FULL_SIMP_TAC std_ss [fake_ftbl_entries_def,EVERY_DEF]) 2354 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2355 \\ MATCH_MP_TAC MilawaTrue_TRANS 2356 \\ Q.EXISTS_TAC `(inst_term (FunVarBind params args) (term2t r))` 2357 \\ ASM_SIMP_TAC std_ss [] 2358 \\ `ALL_DISTINCT params` by METIS_TAC [context_ok_def] 2359 \\ `(Equal (mApp (mFun name) (MAP mConst args)) 2360 (inst_term (FunVarBind params args) (term2t r))) = 2361 formula_sub (ZIP(params,MAP mConst args)) 2362 (Equal (mApp (mFun name) (MAP mVar params)) (term2t r))` by 2363 (FULL_SIMP_TAC (srw_ss()) [formula_sub_def,term_sub_def,MAP_MAP_o,o_DEF] 2364 \\ ASM_SIMP_TAC std_ss [MAP_LOOKUP_LEMMA,inst_term_def] 2365 \\ FULL_SIMP_TAC std_ss [context_ok_def] 2366 \\ RES_TAC \\ IMP_RES_TAC (GSYM term_sub_EQ) 2367 \\ POP_ASSUM (ASSUME_TAC o Q.SPEC `mConst o FunVarBind params args`) 2368 \\ FULL_SIMP_TAC std_ss [o_DEF,MAP_FunVarBind_LEMMA]) 2369 \\ ASM_SIMP_TAC std_ss [] 2370 \\ MATCH_MP_TAC (MilawaTrue_rules |> CONJUNCTS |> el 7) 2371 \\ STRIP_TAC THEN1 2372 (FULL_SIMP_TAC std_ss [formula_sub_def,formula_ok_def, 2373 term_sub_def,term_ok_def,func_arity_def,LENGTH_MAP] 2374 \\ FULL_SIMP_TAC std_ss [EVERY_MEM,MEM_MAP,PULL_IMP] 2375 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC term_ok_sub 2376 \\ FULL_SIMP_TAC std_ss [term_ok_def,EVERY_MEM,MEM_MAP,PULL_IMP] 2377 \\ Cases \\ ASM_SIMP_TAC std_ss [MEM_MAP,pairTheory.EXISTS_PROD, 2378 ZIP_MAP |> Q.SPECL [`xs`,`ys`] |> Q.ISPEC `I` |> SIMP_RULE std_ss [MAP_ID]] 2379 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [term_ok_def]) 2380 \\ FULL_SIMP_TAC std_ss [term_funs_def]) 2381 THEN1 (ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC (srw_ss()) []) 2382 THEN1 (ONCE_REWRITE_TAC [MR_ev_cases] \\ SIMP_TAC (srw_ss()) [] 2383 \\ FULL_SIMP_TAC std_ss [EVERY_DEF,MAP,FLAT,MEM_APPEND] 2384 \\ Q.PAT_X_ASSUM `!xx yy. bbb ==> bbbb` MP_TAC 2385 \\ Q.PAT_X_ASSUM `!xx yy. bbb ==> bbbb` (MP_TAC o Q.SPECL [`ok`,`env`]) 2386 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2387 \\ POP_ASSUM (MP_TAC o Q.SPECL [`ok2`,`env`]) 2388 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2389 \\ Q.EXISTS_TAC `ok2'` \\ STRIP_TAC THEN1 METIS_TAC [] 2390 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2391 \\ IMP_RES_TAC MR_ev_OK \\ FULL_SIMP_TAC std_ss [])) 2392 2393val MR_ev_thm = save_thm("MR_ev_thm",M_ev_IMP_R_ev_lemma 2394 |> CONJUNCTS |> el 1 |> Q.SPECL [`(exp,a,ctxt)`,`result`] 2395 |> SIMP_RULE std_ss [PULL_IMP,AND_IMP_INTRO] |> GEN_ALL); 2396 2397val MR_ap_thm = save_thm("MR_ap_thm",M_ev_IMP_R_ev_lemma 2398 |> CONJUNCTS |> el 2 |> Q.SPECL [`(f,args,ctxt)`,`result`] 2399 |> SIMP_RULE std_ss [PULL_IMP,AND_IMP_INTRO] |> GEN_ALL); 2400 2401val _ = export_theory(); 2402