1open HolKernel boolLib bossLib Parse; val _ = new_theory "lisp_compiler"; 2val _ = ParseExtras.temp_loose_equality() 3 4open stringTheory finite_mapTheory pred_setTheory listTheory sumTheory; 5open optionTheory arithmeticTheory relationTheory pairTheory; 6 7open lisp_bytecodeTheory; 8open lisp_sexpTheory lisp_semanticsTheory lisp_alt_semanticsTheory 9 10infix \\ 11val op \\ = op THEN; 12val RW = REWRITE_RULE; 13val RW1 = ONCE_REWRITE_RULE; 14 15 16(* relation defines translation of programs into bytecode *) 17 18val _ = Hol_datatype` 19 stack_slot = ssTEMP 20 | ssVAR of string`; 21 22val stack_slot_11 = fetch "-" "stack_slot_11" 23val stack_slot_distinct = fetch "-" "stack_slot_distinct" 24val stack_slot = simpLib.type_ssfrag ``:stack_slot`` 25 26val _ = Hol_datatype ` 27 bc_state = <| code : num -> bc_inst_type option ; 28 code_end : num; 29 compiled : (string # (num # num)) list ; (* this is an alist *) 30 instr_length : bc_inst_type -> num ; 31 consts : SExp list ; 32 io_out : string ; 33 ok : bool |>`; 34 35val iLENGTH_def = Define ` 36 (iLENGTH il [] = 0) /\ 37 (iLENGTH il (x::xs) = il (x:bc_inst_type) + iLENGTH il xs)`; 38 39val iLENGTH_APPEND = prove( 40 ``!xs ys il. iLENGTH il (xs ++ ys) = iLENGTH il xs + iLENGTH il ys``, 41 Induct \\ SRW_TAC [] [iLENGTH_def,ADD_ASSOC]); 42 43val var_lookup_def = Define ` 44 (var_lookup n v [] = NONE) /\ 45 (var_lookup n v (x::xs) = if x = ssVAR v then SOME n else var_lookup (n+1:num) v xs)`; 46 47val gen_pops_def = Define ` 48 gen_pops n = if n = 0 then [] else [iPOPS n]`; 49 50val gen_popn_def = Define ` 51 gen_popn n = if n = 0 then [] else gen_pops (n-1) ++ [iPOP]`; 52 53val n_times_def = Define ` 54 (n_times 0 x = []) /\ 55 (n_times (SUC n) x = x::n_times n x)`; 56 57val BC_return_code_def = Define ` 58 (BC_return_code F a = []) /\ 59 (BC_return_code T a = gen_pops (LENGTH a - 1) ++ [iRETURN])`; 60 61val BC_return_def = Define ` 62 BC_return ret (code,a:stack_slot list,q,bc) = 63 (code ++ BC_return_code ret a,a, 64 q + iLENGTH bc.instr_length (code ++ BC_return_code ret a),bc)`; 65 66val BC_call_aux_def = Define ` 67 (BC_call_aux F (fc,n,SOME pos) = [iCALL pos]) /\ 68 (BC_call_aux T (fc,n,SOME pos) = [iJUMP pos]) /\ 69 (BC_call_aux F (fc,n,NONE) = [iCONST_NUM n; iCONST_SYM fc; iCALL_SYM]) /\ 70 (BC_call_aux T (fc,n,NONE) = [iCONST_NUM n; iCONST_SYM fc; iJUMP_SYM])`; 71 72val BC_call_def = Define ` 73 (BC_call b (fc,n,NONE) = BC_call_aux b (fc,n,NONE)) /\ 74 (BC_call b (fc,n,SOME (pos,m)) = if m = n then BC_call_aux b (fc,n,SOME pos) 75 else BC_call_aux b (fc,n,NONE))`; 76 77val BC_ADD_CONST_def = Define ` 78 BC_ADD_CONST bc x = bc with consts := (bc.consts ++ [x])`; 79 80val BC_FAIL_def = Define ` 81 BC_FAIL bc = bc with ok := F`; 82 83val FUN_LOOKUP_def = Define ` 84 (FUN_LOOKUP [] name = NONE) /\ 85 (FUN_LOOKUP ((x,y)::xs) name = if x = name then SOME y else FUN_LOOKUP xs name)`; 86 87val (BC_ev_rules,BC_ev_ind,BC_ev_cases) = Hol_reln ` 88 (* constant *) 89 (!s a ret q bc. 90 BC_ev ret (Const s,a,q,bc) 91 (BC_return ret (if isVal s then [iCONST_NUM (getVal s)] else 92 if isSym s then [iCONST_SYM (getSym s)] else 93 [iCONST_NUM (LENGTH (bc.consts));iCONST_LOOKUP] ,ssTEMP::a,q, 94 if isDot s then BC_ADD_CONST bc s else bc))) 95 /\ 96 (* variable lookup *) 97 (!v a ret q bc. 98 BC_ev ret (Var v,a,q,bc) 99 (BC_return ret (if var_lookup 0 v a = NONE then [iFAIL] else 100 [iLOAD (THE (var_lookup 0 v a))],ssTEMP::a,q,bc))) 101 /\ 102 (* function application *) 103 (!xs a q code1 a1 q1 code2 a2 q2 bc bc1 bc2 fc ret. 104 BC_evl (xs,a,q,bc) (code1,a1,q1,bc1) /\ ~(isFun fc) /\ 105 BC_ap ret (fc,LENGTH xs,a1,q1,bc1) (code2,a2,q2,bc2) ==> 106 BC_ev ret (App fc xs,a,q,bc) (code1 ++ code2,a2,q2,bc2)) 107 /\ 108 (* application of built-in function *) 109 (!fc a ret f n1 n2 q bc. 110 (EVAL_DATA_OP fc = (f,n1)) ==> 111 BC_ap ret (PrimitiveFun fc,n2,a,q,bc) 112 (BC_return ret ([if n1 = n2 then iDATA fc else iFAIL],ssTEMP::DROP n2 a,q,bc))) 113 /\ 114 (* normal proc call -- no tail call optimisation possible *) 115 (!fc xs a code a2 q q2 bc bc2. 116 BC_evl (xs,a,q,bc) (code,a2,q2,bc2) ==> 117 BC_ev F (App (Fun fc) xs,a,q,bc) 118 (code ++ BC_call F (fc,LENGTH xs,FUN_LOOKUP bc.compiled fc), 119 ssTEMP::DROP (LENGTH xs) a2, 120 q2 + iLENGTH bc.instr_length (BC_call F (fc,LENGTH xs,FUN_LOOKUP bc.compiled fc)),bc2)) 121 /\ 122 (* normal proc call -- with tail call optimisation *) 123 (!fc xs a code a2 padding q q2 bc bc2. 124 BC_evl (xs,n_times padding ssTEMP ++ a,q + iLENGTH bc.instr_length (n_times padding (iCONST_SYM "NIL")),bc) (code,a2,q2,bc2) /\ 125 (padding = LENGTH xs - LENGTH a) ==> 126 BC_ev T (App (Fun fc) xs,a,q,bc) 127 (n_times padding (iCONST_SYM "NIL") ++ code ++ 128 n_times (LENGTH xs) (iSTORE (LENGTH a + padding - 1)) ++ 129 gen_popn (LENGTH a - LENGTH xs) ++ BC_call T (fc,LENGTH xs,FUN_LOOKUP bc.compiled fc),[], 130 q2 + iLENGTH bc.instr_length (n_times (LENGTH xs) (iSTORE (LENGTH a + padding - 1)) ++ 131 gen_popn (LENGTH a - LENGTH xs) ++ BC_call T (fc,LENGTH xs,FUN_LOOKUP bc.compiled fc)),bc2)) 132 /\ 133 (* if then else *) 134 (!a x y z x_code y_code z_code a1 a2 a3 ret q q1 q2 q3 bc bc1 bc2 bc3. 135 BC_ev F (x,a,q,bc) (x_code,a1,q1,bc1) /\ 136 BC_ev ret (y,a,q1+bc.instr_length(iJNIL (q2+bc.instr_length(iJUMP q3))),bc1) (y_code,a2,q2,bc2) /\ 137 BC_ev ret (z,a,q2+bc.instr_length(iJUMP q3),bc2) (z_code,a3,q3,bc3) ==> 138 BC_ev ret (If x y z,a,q,bc) (x_code ++ [iJNIL (q2+bc.instr_length(iJUMP q3))] ++ 139 y_code ++ [iJUMP q3] ++ 140 z_code,ssTEMP::a,q3,bc3)) 141 /\ 142 (* or -- base case *) 143 (!ret a q bc code a2 q2 bc2. 144 BC_ev ret (Const (Sym "NIL"),a,q,bc) (code,a2,q2,bc2) ==> 145 BC_ev ret (Or [],a,q,bc) (code,a2,q2,bc2)) 146 /\ 147 (* or -- step case *) 148 (!a x_code z_code a1 a3 ret q q1 q3 bc bc1 bc3 t ts addr. 149 BC_ev F (t,a,q,bc) (x_code,a1,q1,bc1) /\ 150 (addr = iLENGTH bc.instr_length (x_code ++ [iLOAD 0; iJNIL (q+addr)] ++ 151 BC_return_code ret (ssTEMP::a) ++ [iJUMP q3])) /\ 152 BC_ev ret (Or ts,a,q1 + iLENGTH bc.instr_length ([iLOAD 0; iJNIL (q+addr)] ++ BC_return_code ret (ssTEMP::a) ++ [iJUMP q3; iPOP]),bc1) (z_code,a3,q3,bc3) ==> 153 BC_ev ret (Or (t::ts),a,q,bc) (x_code ++ [iLOAD 0; iJNIL (q+addr)] ++ 154 BC_return_code ret (ssTEMP::a) ++ [iJUMP q3; iPOP] ++ 155 z_code,ssTEMP::a,q3,bc3)) 156 /\ 157 (* let *) 158 (!a x xs ys code1 code2 a1 a2 ret q q1 q2 bc bc1 bc2. 159 BC_evl (ys,a,q,bc) (code1,a1,q1,bc1) /\ 160 BC_ev ret (x,MAP (ssVAR) (REVERSE xs) ++ DROP (LENGTH xs) a1,q1,bc1) (code2,a2,q2,bc2) ==> 161 BC_ev ret (LamApp xs x ys,a,q,bc) 162 (code1 ++ code2 ++ if ret then [] else [iPOPS (LENGTH xs)],ssTEMP::a, 163 if ret then q2 else q2+bc.instr_length(iPOPS (LENGTH xs)),bc2)) 164 /\ 165 (* print *) 166 (!a ret n q bc. 167 BC_ap ret (Print,n,a,q,bc) 168 (BC_return ret ([iCONST_SYM "NIL"] ++ n_times n (iDATA opCONS) ++ 169 [iCONST_SYM "PRINT"; iLOAD 1; iDATA opCONS; iPRINT; iCONST_SYM "NIL"; iPOPS 2],ssTEMP::DROP n a,q,bc))) 170 /\ 171 (* error *) 172 (!a ret n q bc. 173 BC_ap ret (Error,n,a,q,bc) 174 (BC_return ret ([iCONST_SYM "NIL"] ++ n_times n (iDATA opCONS) ++ 175 [iCONST_SYM "ERROR"; iLOAD 1; iDATA opCONS; iPRINT; iFAIL],ssTEMP::DROP n a,q,bc))) 176 /\ 177 (* define *) 178 (!a ret n q bc. 179 BC_ap ret (Define,n,a,q,bc) 180 (BC_return ret ([iCOMPILE],ssTEMP::DROP n a,q,bc))) 181 /\ 182 (* funcall *) 183 (!a ret n q bc. 184 BC_ap ret (Funcall,n,a,q,bc) 185 (BC_return ret ([iCONST_NUM (n-1); iLOAD n; iCALL_SYM; iPOPS 1],ssTEMP::DROP n a,q,bc))) 186 /\ 187 (* list, base case *) 188 (!a q bc. 189 BC_evl ([],a,q,bc) ([],a,q,bc)) 190 /\ 191 (* list, step case *) 192 (!a x xs q q2 q3 a2 a3 code code2 bc bc2 bc3. 193 BC_ev F (x,a,q,bc) (code,a2,q2,bc2) /\ 194 BC_evl (xs,a2,q2,bc2) (code2,a3,q3,bc3) ==> 195 BC_evl (x::xs,a,q,bc) (code ++ code2,a3,q3,bc3)) 196 /\ 197 198 (* only macros below *) 199 200 (!ret e a q bc code a2 q2 bc2. 201 BC_ev ret (App (PrimitiveFun opCAR) [e],a,q,bc) (code,a2,q2,bc2) ==> 202 BC_ev ret (First e,a,q,bc) (code,a2,q2,bc2)) 203 /\ 204 (!ret e a q bc code a2 q2 bc2. 205 BC_ev ret (First (App (PrimitiveFun opCDR) [e]),a,q,bc) (code,a2,q2,bc2) ==> 206 BC_ev ret (Second e,a,q,bc) (code,a2,q2,bc2)) 207 /\ 208 (!ret e a q bc code a2 q2 bc2. 209 BC_ev ret (Second (App (PrimitiveFun opCDR) [e]),a,q,bc) (code,a2,q2,bc2) ==> 210 BC_ev ret (Third e,a,q,bc) (code,a2,q2,bc2)) 211 /\ 212 (!ret e a q bc code a2 q2 bc2. 213 BC_ev ret (Third (App (PrimitiveFun opCDR) [e]),a,q,bc) (code,a2,q2,bc2) ==> 214 BC_ev ret (Fourth e,a,q,bc) (code,a2,q2,bc2)) 215 /\ 216 (!ret e a q bc code a2 q2 bc2. 217 BC_ev ret (Fourth (App (PrimitiveFun opCDR) [e]),a,q,bc) (code,a2,q2,bc2) ==> 218 BC_ev ret (Fifth e,a,q,bc) (code,a2,q2,bc2)) 219 /\ 220 (!ret zs x a q bc code a2 q2 bc2. 221 BC_ev ret (LamApp (MAP FST zs) x (MAP SND zs),a,q,bc) (code,a2,q2,bc2) ==> 222 BC_ev ret (Let zs x,a,q,bc) (code,a2,q2,bc2)) 223 /\ 224 (!ret x a q bc code a2 q2 bc2. 225 BC_ev ret (x,a,q,bc) (code,a2,q2,bc2) ==> 226 BC_ev ret (LetStar [] x,a,q,bc) (code,a2,q2,bc2)) 227 /\ 228 (!ret z zs x a q bc code a2 q2 bc2. 229 BC_ev ret (Let [z] (LetStar zs x),a,q,bc) (code,a2,q2,bc2) ==> 230 BC_ev ret (LetStar (z::zs) x,a,q,bc) (code,a2,q2,bc2)) 231 /\ 232 (!ret a q bc code a2 q2 bc2. 233 BC_ev ret (Const (Sym "NIL"),a,q,bc) (code,a2,q2,bc2) ==> 234 BC_ev ret (Cond [],a,q,bc) (code,a2,q2,bc2)) 235 /\ 236 (!ret x1 x2 qs a q bc code a2 q2 bc2. 237 BC_ev ret (If x1 x2 (Cond qs),a,q,bc) (code,a2,q2,bc2) ==> 238 BC_ev ret (Cond ((x1,x2)::qs),a,q,bc) (code,a2,q2,bc2)) 239 /\ 240 (!ret a q bc code a2 q2 bc2. 241 BC_ev ret (Const (Sym "T"),a,q,bc) (code,a2,q2,bc2) ==> 242 BC_ev ret (And [],a,q,bc) (code,a2,q2,bc2)) 243 /\ 244 (!ret a q bc code a2 q2 bc2. 245 BC_ev ret (Const (Sym "NIL"),a,q,bc) (code,a2,q2,bc2) ==> 246 BC_ev ret (List [],a,q,bc) (code,a2,q2,bc2)) 247 /\ 248 (!ret t a q bc code a2 q2 bc2. 249 BC_ev ret (t,a,q,bc) (code,a2,q2,bc2) ==> 250 BC_ev ret (And [t],a,q,bc) (code,a2,q2,bc2)) 251 /\ 252 (!ret t1 t2 ts a q bc code a2 q2 bc2. 253 BC_ev ret (If t1 (And (t2::ts)) (Const (Sym "NIL")),a,q,bc) (code,a2,q2,bc2) ==> 254 BC_ev ret (And (t1::t2::ts),a,q,bc) (code,a2,q2,bc2)) 255 /\ 256 (!ret t ts a q bc code a2 q2 bc2. 257 BC_ev ret (App (PrimitiveFun opCONS) [t;List ts],a,q,bc) (code,a2,q2,bc2) ==> 258 BC_ev ret (List (t::ts),a,q,bc) (code,a2,q2,bc2)) 259 /\ 260 (!ret code fname ps body a q bc a2 q2 bc2. 261 BC_ev ret (App Define [Const (Sym fname); Const (list2sexp (MAP Sym ps)); Const body],a,q,bc) (code,a2,q2,bc2) ==> 262 BC_ev ret (Defun fname ps body,a,q,bc) (code,a2,q2,bc2))`; 263 264 265val PULL_EXISTS_IMP = METIS_PROVE [] ``((?x. P x) ==> Q) = (!x. P x ==> Q)``; 266val PULL_FORALL_IMP = METIS_PROVE [] ``(Q ==> !x. P x) = (!x. Q ==> P x)``; 267 268val BC_JUMPS_OK_def = Define ` 269 BC_JUMPS_OK bc = 270 (!a. bc.instr_length (iJUMP a) = bc.instr_length (iJUMP 0)) /\ 271 (!a. bc.instr_length (iJNIL a) = bc.instr_length (iJNIL 0))`; 272 273val BC_CODE_OK_def = Define ` 274 BC_CODE_OK bc = 275 (!h. 0 < bc.instr_length h) /\ 276 (!a. bc.instr_length (iJUMP a) = bc.instr_length (iJUMP 0)) /\ 277 (!a. bc.instr_length (iJNIL a) = bc.instr_length (iJNIL 0)) /\ 278 !i. bc.code_end <= i ==> (bc.code i = NONE)`; 279 280val NOT_isFun = prove( 281 ``!fc. ~isFun fc = !f. ~(fc = Fun f)``, 282 Cases \\ SIMP_TAC (srw_ss()) [isFun_def]); 283 284val BC_JUMPS_OK_BC_ADD_CONST = prove( 285 ``!bc s. BC_JUMPS_OK (BC_ADD_CONST bc s) = BC_JUMPS_OK bc``, 286 EVAL_TAC \\ FULL_SIMP_TAC std_ss []); 287 288fun STRIP_NOT_CONJ_TAC (h,goal) = 289 if not (is_conj goal) then STRIP_TAC (h,goal) else NO_TAC (h,goal) 290 291val DET_TAC = 292 FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_NOT_CONJ_TAC 293 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM MP_TAC 294 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [BC_return_def] 295 \\ REPEAT STRIP_NOT_CONJ_TAC \\ RES_TAC 296 \\ FULL_SIMP_TAC std_ss [] \\ RES_TAC 297 \\ FULL_SIMP_TAC std_ss [] 298 299val DET2_TAC = 300 FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_NOT_CONJ_TAC 301 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM MP_TAC 302 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [BC_return_def] 303 \\ FULL_SIMP_TAC std_ss [NOT_isFun] \\ METIS_TAC [BC_JUMPS_OK_BC_ADD_CONST] 304 305local 306 val BC_ev_DET_ind = BC_ev_ind 307 |> Q.SPEC `\ret (x1,x2,x3,x4,bc) z. !z1 z2 z3 z4. BC_JUMPS_OK bc /\ BC_ap ret (x1,x2,x3,x4,bc) (z1,z2,z3,z4) ==> (z = (z1,z2,z3,z4)) /\ BC_JUMPS_OK z4` 308 |> Q.SPEC `\(x1,x2,x3,bc) z. !z1 z2 z3 z4. BC_JUMPS_OK bc /\ BC_evl (x1,x2,x3,bc) (z1,z2,z3,z4) ==> (z = (z1,z2,z3,z4)) /\ BC_JUMPS_OK z4` 309 |> Q.SPEC `\ret (x1,x2,x3,bc) z. !z1 z2 z3 z4. BC_JUMPS_OK bc /\ BC_ev ret (x1,x2,x3,bc) (z1,z2,z3,z4) ==> (z = (z1,z2,z3,z4)) /\ BC_JUMPS_OK z4` 310 val goal = BC_ev_DET_ind |> concl |> dest_imp |> snd; 311 val BC_ev_DET_lemma = prove(goal, 312 MATCH_MP_TAC BC_ev_DET_ind 313 \\ STRIP_TAC THEN1 DET2_TAC 314 \\ STRIP_TAC THEN1 DET_TAC 315 \\ STRIP_TAC THEN1 DET2_TAC 316 \\ STRIP_TAC THEN1 DET2_TAC 317 \\ STRIP_TAC THEN1 DET2_TAC 318 \\ STRIP_TAC THEN1 DET2_TAC 319 \\ STRIP_TAC THEN1 320 (FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_NOT_CONJ_TAC 321 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM MP_TAC 322 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [BC_return_def] 323 \\ Q.PAT_X_ASSUM `BC_JUMPS_OK bc` (fn th => 324 ASSUME_TAC th THEN ASSUME_TAC (RW [BC_JUMPS_OK_def] th)) 325 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 326 \\ STRIP_TAC THEN1 DET2_TAC 327 \\ STRIP_TAC THEN1 328 (FULL_SIMP_TAC std_ss [] \\ REPEAT STRIP_NOT_CONJ_TAC 329 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM MP_TAC 330 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [BC_return_def] 331 \\ Q.PAT_X_ASSUM `BC_JUMPS_OK bc` (fn th => 332 ASSUME_TAC th THEN ASSUME_TAC (RW [BC_JUMPS_OK_def] th)) 333 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND] 334 \\ REPEAT STRIP_NOT_CONJ_TAC \\ FULL_SIMP_TAC std_ss [] 335 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] \\ RES_TAC 336 \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 337 \\ REPEAT (STRIP_TAC THEN1 DET_TAC)) 338in 339 val BC_ev_DETERMINISTIC = store_thm("BC_ev_DETERMINISTIC", 340 ``!t a q bc y z. 341 BC_CODE_OK bc ==> 342 BC_ev T (t,a,q,bc) y /\ BC_ev T (t,a,q,bc) z ==> (y = z)``, 343 FULL_SIMP_TAC std_ss [FORALL_PROD] \\ REPEAT STRIP_NOT_CONJ_TAC 344 \\ `BC_JUMPS_OK bc` by FULL_SIMP_TAC std_ss [BC_JUMPS_OK_def,BC_CODE_OK_def] 345 \\ IMP_RES_TAC (SIMP_RULE std_ss [FORALL_PROD] BC_ev_DET_lemma) 346 \\ METIS_TAC []) 347end; 348 349 350 351val SUM_def = Define ` 352 (SUM [] = 0) /\ 353 (SUM (x::xs) = x + SUM xs)`; 354 355val MEM_term_size5 = prove( 356 ``!ts a. MEM a ts ==> term_size a < term5_size ts``, 357 Induct \\ SIMP_TAC std_ss [MEM,term_size_def] \\ REPEAT STRIP_TAC \\ RES_TAC 358 \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC); 359 360val MEM_term_size3 = prove( 361 ``!ts a b. MEM (a,b) ts ==> term_size a < term3_size ts /\ 362 term_size b < term3_size ts``, 363 Induct \\ SIMP_TAC std_ss [MEM,term_size_def] \\ REPEAT STRIP_TAC \\ RES_TAC 364 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [term_size_def] \\ DECIDE_TAC); 365 366val MEM_term_size1 = prove( 367 ``!ts a b. MEM (a,b) ts ==> term_size b < term1_size ts``, 368 Induct \\ SIMP_TAC std_ss [MEM,term_size_def] \\ REPEAT STRIP_TAC \\ RES_TAC 369 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [term_size_def] \\ DECIDE_TAC); 370 371val term_depth_def = tDefine "term_depth" ` 372 (term_depth (Const _) = 1) /\ 373 (term_depth (Var _) = 1) /\ 374 (term_depth (App _ xs) = 1 + SUM (MAP term_depth xs)) /\ 375 (term_depth (If x y z) = 1 + term_depth x + term_depth y + term_depth z) /\ 376 (term_depth (LamApp _ y xs) = 1 + term_depth y + SUM (MAP term_depth xs)) /\ 377 (term_depth (Let ys x) = 10 + term_depth x + SUM (MAP (\(x,y). term_depth y) ys)) /\ 378 (term_depth (LetStar ys x) = 10 + term_depth x + SUM (MAP (\(x,y). term_depth y) ys) + 100 * LENGTH ys) /\ 379 (term_depth (Cond qs) = 10 + LENGTH qs + SUM (MAP (\(x,y). term_depth x + term_depth y) qs) + 20 * LENGTH qs) /\ 380 (term_depth (Or ts) = 10 + SUM (MAP term_depth ts)) /\ 381 (term_depth (And ts) = 10 + SUM (MAP term_depth ts)) /\ 382 (term_depth (List ts) = 10 + SUM (MAP term_depth ts) + 10 * LENGTH ts) /\ 383 (term_depth (First x) = 10 + term_depth x) /\ 384 (term_depth (Second x) = 20 + term_depth x) /\ 385 (term_depth (Third x) = 30 + term_depth x) /\ 386 (term_depth (Fourth x) = 40 + term_depth x) /\ 387 (term_depth (Fifth x) = 50 + term_depth x) /\ 388 (term_depth (Defun _ _ _) = 10)` 389 (WF_REL_TAC `measure (term_size)` \\ REPEAT STRIP_TAC 390 \\ IMP_RES_TAC MEM_term_size5 \\ IMP_RES_TAC MEM_term_size1 391 \\ IMP_RES_TAC MEM_term_size3 \\ REPEAT DECIDE_TAC); 392 393val ZERO_LT_term_depth = prove( 394 ``!x. 0 < term_depth x``, 395 Cases \\ EVAL_TAC \\ DECIDE_TAC); 396 397val IMP_BC_evl_EXISTS = prove( 398 ``!l a q bc. 399 (!t ret a q bc. 400 MEM t l /\ BC_JUMPS_OK bc ==> 401 ?y1 y2 y3 bc1. 402 BC_ev ret (t,a,q,bc) (y1,y2,y3,bc1) /\ BC_JUMPS_OK bc1) /\ 403 BC_JUMPS_OK bc ==> 404 ?y1 y2 y3 bc1. 405 BC_evl (l,a,q,bc) (y1,y2,y3,bc1) /\ BC_JUMPS_OK bc1``, 406 Induct \\ FULL_SIMP_TAC std_ss [FORALL_PROD] \\ REPEAT STRIP_TAC 407 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [] 408 \\ FULL_SIMP_TAC std_ss [MEM] \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] 409 \\ METIS_TAC []); 410 411val MEM_SUM_MAP = prove( 412 ``!xs x. MEM x xs ==> term_depth x <= SUM (MAP (\a. term_depth a) xs)``, 413 Induct \\ SIMP_TAC std_ss [MEM] \\ REPEAT STRIP_TAC 414 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [SUM_def,MAP] \\ DECIDE_TAC); 415 416val BC_ap_cases = BC_ev_cases |> CONJUNCTS |> el 1; 417 418val PULL_EXISTS_CONJ = METIS_PROVE [] 419 ``((?x. Q x) /\ P = (?x. Q x /\ P)) /\ (P /\ (?x. Q x) = (?x. P /\ Q x))`` 420 421val BC_ev_TOTAL_LEMMA = prove( 422 ``!ret t a q bc. 423 BC_JUMPS_OK bc ==> 424 ?y1 y2 y3 bc1. BC_ev ret (t,a,q,bc) (y1,y2,y3,bc1) /\ BC_JUMPS_OK bc1``, 425 completeInduct_on `term_depth t` 426 \\ FULL_SIMP_TAC std_ss [PULL_FORALL_IMP] \\ REPEAT STRIP_TAC 427 \\ FULL_SIMP_TAC std_ss [AND_IMP_INTRO] \\ Cases_on `t` 428 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [BC_return_def] 429 \\ METIS_TAC [BC_JUMPS_OK_BC_ADD_CONST]) 430 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [BC_return_def]) 431 THEN1 (`!a q. ?y1 y2 y3 bc1. 432 BC_evl (l,a,q,bc) (y1,y2,y3,bc1) /\ BC_JUMPS_OK bc1` by 433 (REPEAT STRIP_TAC \\ MATCH_MP_TAC IMP_BC_evl_EXISTS \\ ASM_SIMP_TAC std_ss [] 434 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!tttt.bbb` MATCH_MP_TAC 435 \\ ASM_SIMP_TAC std_ss [term_depth_def] 436 \\ IMP_RES_TAC MEM_SUM_MAP \\ DECIDE_TAC) 437 \\ Cases_on `isFun f` THEN1 438 (Cases_on `f` \\ FULL_SIMP_TAC std_ss [isFun_def] \\ Cases_on `ret` 439 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [isFun_def] 440 \\ FULL_SIMP_TAC std_ss [FORALL_PROD,EXISTS_PROD] \\ METIS_TAC []) 441 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ ASM_SIMP_TAC (srw_ss()) [isFun_def] 442 \\ Cases_on `f` \\ FULL_SIMP_TAC (srw_ss()) [isFun_def] 443 \\ SIMP_TAC (srw_ss()) [Once BC_ap_cases,BC_return_def] 444 \\ FULL_SIMP_TAC std_ss [PULL_EXISTS_CONJ] 445 \\ Cases_on `EVAL_DATA_OP l'` \\ FULL_SIMP_TAC std_ss [] 446 \\ METIS_TAC []) 447 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 448 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD,term_depth_def,PULL_EXISTS_CONJ] 449 \\ POP_ASSUM (fn th => MP_TAC th THEN ASSUME_TAC (RW [BC_JUMPS_OK_def] th)) 450 \\ FULL_SIMP_TAC std_ss [] 451 \\ `term_depth t' < 1 + term_depth t' + term_depth t0 + term_depth t1` by DECIDE_TAC 452 \\ `term_depth t0 < 1 + term_depth t' + term_depth t0 + term_depth t1` by DECIDE_TAC 453 \\ `term_depth t1 < 1 + term_depth t' + term_depth t0 + term_depth t1` by DECIDE_TAC 454 \\ RES_TAC \\ METIS_TAC []) 455 THEN1 (`?y1 y2 y3 bc1. 456 BC_evl (l,a,q,bc) (y1,y2,y3,bc1) /\ BC_JUMPS_OK bc1` by 457 (REPEAT STRIP_TAC \\ MATCH_MP_TAC IMP_BC_evl_EXISTS \\ ASM_SIMP_TAC std_ss [] 458 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!tttt.bbb` MATCH_MP_TAC 459 \\ ASM_SIMP_TAC std_ss [term_depth_def] 460 \\ IMP_RES_TAC MEM_SUM_MAP \\ DECIDE_TAC) 461 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 462 \\ FULL_SIMP_TAC std_ss [term_depth_def,PULL_EXISTS_CONJ] 463 \\ `term_depth t' < 1 + term_depth t' + SUM (MAP (\a. term_depth a) l)` by DECIDE_TAC 464 \\ RES_TAC \\ METIS_TAC [PAIR]) 465 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 466 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 467 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] 468 \\ `!l. (MAP (\(x':string,y). term_depth y) l) = 469 (MAP (\a. term_depth a) (MAP SND l))` by 470 (Induct \\ FULL_SIMP_TAC std_ss [MAP] 471 \\ Cases \\ FULL_SIMP_TAC std_ss [MAP]) 472 \\ FULL_SIMP_TAC std_ss []) 473 THEN1 (Cases_on `l` THEN1 474 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 475 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 476 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 477 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 478 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 479 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 480 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] 481 \\ Cases_on `h` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] \\ DECIDE_TAC) 482 THEN1 (Cases_on `l` THEN1 483 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 484 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 485 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 486 \\ Cases_on `h` \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 487 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 488 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def,LENGTH,ADD1] \\ DECIDE_TAC) 489 THEN1 490 (Cases_on `l` THEN1 491 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 492 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 493 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 494 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] 495 \\ `term_depth h < 10 + (term_depth h + SUM (MAP (\a. term_depth a) t))` by DECIDE_TAC 496 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [EXISTS_PROD,PULL_EXISTS_CONJ] 497 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND] 498 \\ Q.PAT_X_ASSUM `BC_JUMPS_OK bc` (fn th => ASSUME_TAC th THEN ASSUME_TAC (RW [BC_JUMPS_OK_def] th)) 499 \\ FULL_SIMP_TAC std_ss [] 500 \\ `term_depth (Or t) < 10 + (term_depth h + SUM (MAP (\a. term_depth a) t))` by 501 (FULL_SIMP_TAC std_ss [term_depth_def,ZERO_LT_term_depth]) 502 \\ RES_TAC \\ METIS_TAC []) 503 THEN1 504 (Cases_on `l` THEN1 505 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 506 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 507 \\ Cases_on `t` THEN1 508 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 509 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] 510 \\ `term_depth h < 10 + term_depth h` by DECIDE_TAC 511 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ METIS_TAC []) 512 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 513 \\ `term_depth (And (h'::t')) < term_depth (And (h::h'::t'))` by 514 (FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def,ZERO_LT_term_depth]) 515 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 516 \\ `term_depth h < term_depth (And (h::h'::t'))` by 517 (FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 518 \\ `term_depth (Const (Sym "NIL")) < term_depth (And (h::h'::t'))` by 519 (FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 520 \\ FULL_SIMP_TAC std_ss [PULL_EXISTS_CONJ] 521 \\ Q.PAT_X_ASSUM `BC_JUMPS_OK bc` (fn th => ASSUME_TAC th THEN ASSUME_TAC (RW [BC_JUMPS_OK_def] th)) 522 \\ FULL_SIMP_TAC std_ss [] 523 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ METIS_TAC []) 524 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 525 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def,EXISTS_PROD]) 526 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 527 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 528 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 529 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 530 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 531 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 532 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 533 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 534 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 535 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 536 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 537 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def] \\ DECIDE_TAC) 538 THEN1 (Cases_on `l` THEN1 539 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 540 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC) 541 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 542 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 543 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def,LENGTH,ADD1] \\ DECIDE_TAC) 544 THEN1 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC (srw_ss()) [] 545 \\ FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ Q.PAT_X_ASSUM `!tt.bbb` MATCH_MP_TAC 546 \\ FULL_SIMP_TAC std_ss [term_depth_def,MAP,SUM_def,LENGTH,ADD1] \\ DECIDE_TAC)); 547 548val BC_ev_TOTAL = store_thm("BC_ev_TOTAL", 549 ``!ret t a q bc. BC_JUMPS_OK bc ==> ?y. BC_ev ret (t,a,q,bc) y``, 550 FULL_SIMP_TAC std_ss [EXISTS_PROD] \\ METIS_TAC [BC_ev_TOTAL_LEMMA]); 551 552val WRITE_BYTECODE_def = Define ` 553 (WRITE_BYTECODE bc p [] = bc) /\ 554 (WRITE_BYTECODE bc p ((c:bc_inst_type)::cs) = 555 (WRITE_BYTECODE (bc with code := ((p =+ SOME c) bc.code)) ((p:num) + bc.instr_length c) cs))`; 556 557val BC_ev_fun_def = Define ` 558 BC_ev_fun (params,body,bc) = 559 @result. if BC_JUMPS_OK bc then BC_ev T (body,MAP ssVAR (REVERSE params),bc.code_end,bc) result 560 else (result = ([],[],bc.code_end,bc))`; 561 562val BC_ev_fun_IMP = prove( 563 ``(((BC_ev_fun (params,body,bc) = result)) /\ BC_JUMPS_OK bc ==> 564 BC_ev T (body,MAP ssVAR (REVERSE params),bc.code_end,bc) result)``, 565 SIMP_TAC std_ss [BC_ev_fun_def] \\ METIS_TAC [BC_ev_TOTAL]); 566 567val BC_ev_fun_thm = prove( 568 ``BC_CODE_OK bc ==> 569 (((BC_ev_fun (params,body,bc) = result)) = 570 BC_ev T (body,MAP ssVAR (REVERSE params),bc.code_end,bc) result)``, 571 SIMP_TAC std_ss [BC_ev_fun_def] 572 \\ METIS_TAC [BC_ev_DETERMINISTIC,BC_ev_TOTAL,BC_JUMPS_OK_def,BC_CODE_OK_def]); 573 574val BC_PRINT_def = Define ` 575 BC_PRINT bc x = bc with io_out := (bc.io_out ++ x)`; 576 577val BC_STORE_COMPILED_def = Define ` 578 BC_STORE_COMPILED bc fc x = bc with compiled := (fc,x)::bc.compiled`; 579 580val BC_ONLY_COMPILE_def = Define ` 581 BC_ONLY_COMPILE (params,body,bc) = 582 let (new_code,a2,q2,bc) = BC_ev_fun (params,body,bc) in 583 let bc = WRITE_BYTECODE bc bc.code_end new_code in 584 let bc = bc with code_end := bc.code_end + iLENGTH bc.instr_length new_code in 585 bc`; 586 587val BC_COMPILE_def = Define ` 588 BC_COMPILE (fname,params,body,bc) = 589 let bc = BC_STORE_COMPILED bc fname (bc.code_end,LENGTH params) in 590 BC_ONLY_COMPILE (params,body,bc)` 591 592val BC_COMPILE_thm = RW [BC_ONLY_COMPILE_def] BC_COMPILE_def; 593 594 595(* semantics *) 596 597val CONTAINS_BYTECODE_def = Define ` 598 (CONTAINS_BYTECODE bc p [] = T) /\ 599 (CONTAINS_BYTECODE bc p (c::cs) = 600 (bc.code p = SOME c) /\ 601 CONTAINS_BYTECODE bc (p + bc.instr_length (c:bc_inst_type)) cs)`; 602 603val BC_STEP_def = Define ` 604 BC_STEP bc p = p + bc.instr_length (THE (bc.code p))`; 605 606val BC_SUBSTATE_def = Define ` 607 BC_SUBSTATE bc1 bc2 = 608 (!i. BC_CODE_OK bc1 /\ ~(bc1.code i = NONE) ==> (bc2.code i = bc1.code i)) /\ 609 (!i. ~(FUN_LOOKUP bc1.compiled i = NONE) ==> (FUN_LOOKUP bc2.compiled i = FUN_LOOKUP bc1.compiled i)) /\ 610 (bc2.instr_length = bc1.instr_length) /\ 611 (BC_CODE_OK bc1 ==> BC_CODE_OK bc2) /\ 612 ?qs. bc2.consts = bc1.consts ++ qs`; 613 614val (iSTEP_rules,iSTEP_ind,iSTEP_cases) = 615 Hol_reln 616 `(!bc p xs x rs. 617 CONTAINS_BYTECODE bc p [iPOP] ==> 618 iSTEP (x::xs,p,rs,bc) (xs,BC_STEP bc p,rs,bc)) /\ 619 (!bc p xs ys x rs. 620 CONTAINS_BYTECODE bc p [iPOPS (LENGTH ys)] ==> 621 iSTEP (x::ys++xs,p,rs,bc) (x::xs,BC_STEP bc p,rs,bc)) /\ 622 (!bc p xs x rs. 623 CONTAINS_BYTECODE bc p [iCONST_NUM x] ==> 624 iSTEP (xs,p,rs,bc) (Val x::xs,BC_STEP bc p,rs,bc)) /\ 625 (!bc p xs x rs. 626 CONTAINS_BYTECODE bc p [iCONST_SYM x] ==> 627 iSTEP (xs,p,rs,bc) (Sym x::xs,BC_STEP bc p,rs,bc)) /\ 628 (!bc p xs x rs. 629 CONTAINS_BYTECODE bc p [iCONST_LOOKUP] /\ x < LENGTH bc.consts ==> 630 iSTEP (Val x::xs,p,rs,bc) (EL x bc.consts::xs,BC_STEP bc p,rs,bc)) /\ 631 (!bc p xs op_name args f rs. 632 CONTAINS_BYTECODE bc p [iDATA op_name] /\ 633 (EVAL_DATA_OP op_name = (f,LENGTH args)) ==> 634 iSTEP (REVERSE args ++ xs,p,rs,bc) (f args::xs,BC_STEP bc p,rs,bc)) /\ 635 (!bc p xs i rs. 636 CONTAINS_BYTECODE bc p [iLOAD i] /\ i < LENGTH xs ==> 637 iSTEP (xs,p,rs,bc) (EL i xs::xs,BC_STEP bc p,rs,bc)) /\ 638 (!bc p x xs i rs. 639 CONTAINS_BYTECODE bc p [iSTORE i] /\ i < LENGTH xs ==> 640 iSTEP (x::xs,p,rs,bc) (UPDATE_NTH i x xs,BC_STEP bc p,rs,bc)) /\ 641 (!bc p xs i rs. 642 CONTAINS_BYTECODE bc p [iJUMP i] ==> 643 iSTEP (xs,p,rs,bc) (xs,i,rs,bc)) /\ 644 (!bc p xs i rs. 645 CONTAINS_BYTECODE bc p [iCALL i] ==> 646 iSTEP (xs,p,rs,bc) (xs,i,(BC_STEP bc p)::rs,bc)) /\ 647 (!bc p xs r rs. 648 CONTAINS_BYTECODE bc p [iRETURN] ==> 649 iSTEP (xs,p,r::rs,bc) (xs,r,rs,bc)) /\ 650 (!bc p x xs i rs. 651 CONTAINS_BYTECODE bc p [iJNIL i] ==> 652 iSTEP (x::xs,p,rs,bc) (xs,if x = Sym "NIL" then i else BC_STEP bc p,rs,bc)) /\ 653 (!bc p fc xs i n rs. 654 CONTAINS_BYTECODE bc p [iJUMP_SYM] /\ (FUN_LOOKUP bc.compiled fc = SOME (i,n)) ==> 655 iSTEP (Sym fc::Val n::xs,p,rs,bc) (xs,i,rs,bc)) /\ 656 (!bc p fc xs i n rs. 657 CONTAINS_BYTECODE bc p [iCALL_SYM] /\ (FUN_LOOKUP bc.compiled fc = SOME (i,n)) ==> 658 iSTEP (Sym fc::Val n::xs,p,rs,bc) (xs,i,(BC_STEP bc p)::rs,bc)) /\ 659 (!bc p xs rs xs2 p2 rs2. 660 CONTAINS_BYTECODE bc p [iFAIL] ==> 661 iSTEP (xs,p,rs,bc) (xs2,p2,rs2,BC_FAIL bc)) /\ 662 (!bc p x xs rs. 663 CONTAINS_BYTECODE bc p [iPRINT] ==> 664 iSTEP (x::xs,p,rs,bc) (x::xs,(BC_STEP bc p),rs,BC_PRINT bc (sexp2string x ++ "\n"))) /\ 665 (!bc p xs rs formals body fname bc1. 666 CONTAINS_BYTECODE bc p [iCOMPILE] /\ (FUN_LOOKUP bc.compiled (getSym fname) = NONE) /\ 667 (BC_COMPILE (getSym fname,MAP getSym (sexp2list formals),sexp2term body,bc) = bc1) ==> 668 iSTEP (body::formals::fname::xs,p,rs,bc) 669 (Sym "NIL"::xs,(BC_STEP bc p),rs,bc1)) /\ 670 (!bc p xs rs formals body fname. 671 CONTAINS_BYTECODE bc p [iCOMPILE] /\ ~(FUN_LOOKUP bc.compiled (getSym fname) = NONE) ==> 672 iSTEP (body::formals::fname::xs,p,rs,bc) 673 (Sym "NIL"::xs,(BC_STEP bc p),rs,BC_FAIL bc)) /\ 674 (!bc p xs rs xs2 p2 rs2. 675 ~bc.ok ==> 676 iSTEP (xs,p,rs,bc) (xs2,p2,rs2,bc))` 677 678val iSTEP_cases_imp = 679 SPEC_ALL iSTEP_cases 680 |> RW [DISJ_ASSOC] 681 |> MATCH_MP (METIS_PROVE [] ``(b = c \/ d) ==> (c ==> b)``) 682 |> RW [GSYM DISJ_ASSOC] 683 684val CONTAINS_BYTECODE_APPEND = prove( 685 ``!c1 c2 bc p. 686 CONTAINS_BYTECODE bc p (c1 ++ c2) = 687 CONTAINS_BYTECODE bc p c1 /\ 688 CONTAINS_BYTECODE bc (p + iLENGTH bc.instr_length c1) c2``, 689 Induct \\ ASM_SIMP_TAC std_ss [APPEND,CONTAINS_BYTECODE_def, 690 LENGTH,ADD1,AC ADD_COMM ADD_ASSOC,iLENGTH_def] \\ METIS_TAC []); 691 692val BC_SUBSTATE_BC_ADD_CONST = prove( 693 ``BC_SUBSTATE bc (BC_ADD_CONST bc s) /\ BC_SUBSTATE bc (BC_FAIL bc)``, 694 SRW_TAC [] [BC_SUBSTATE_def,BC_ADD_CONST_def,BC_CODE_OK_def,BC_FAIL_def]); 695 696val BC_SUBSTATE_REFL = store_thm("BC_SUBSTATE_REFL", 697 ``!x. BC_SUBSTATE x x``, 698 SIMP_TAC std_ss [BC_SUBSTATE_def] \\ REPEAT STRIP_TAC 699 \\ Q.EXISTS_TAC `[]` \\ SIMP_TAC std_ss [APPEND_NIL]); 700 701val BC_SUBSTATE_TRANS = prove( 702 ``!x y z. BC_SUBSTATE x y /\ BC_SUBSTATE y z ==> BC_SUBSTATE x z``, 703 SIMP_TAC std_ss [FORALL_PROD,BC_SUBSTATE_def] 704 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] \\ METIS_TAC []); 705 706val LENGTH_n_times = prove( 707 ``!k n. LENGTH (n_times k n) = k``, 708 Induct \\ ASM_SIMP_TAC std_ss [n_times_def,LENGTH]); 709 710val BC_ADD_CONST_LENGTH = prove( 711 ``!bc s. (BC_ADD_CONST bc s).instr_length = bc.instr_length``, 712 SRW_TAC [] [BC_ADD_CONST_def]); 713 714val BC_ADD_CONST_OK = prove( 715 ``(BC_ADD_CONST bc s).ok = bc.ok``, 716 SRW_TAC [] [BC_ADD_CONST_def]); 717 718val BC_ev_LENGTH = prove( 719 ``(!ret fc_n_a_q_bc code2_a2_q2_bc2. BC_ap ret fc_n_a_q_bc code2_a2_q2_bc2 ==> 720 !fc n a q bc code2 a2 q2 bc2. 721 (fc_n_a_q_bc = (fc,n,a,q,bc)) /\ 722 (code2_a2_q2_bc2 = (code2,a2,q2,bc2)) ==> 723 BC_SUBSTATE bc bc2 /\ 724 (bc2.instr_length = bc.instr_length) /\ 725 (bc2.ok = bc.ok) /\ 726 (q2 = q + iLENGTH bc.instr_length code2)) /\ 727 (!xs_a_q_bc code2_a2_q2_bc2. BC_evl xs_a_q_bc code2_a2_q2_bc2 ==> 728 !xs a q bc code2 a2 q2 bc2. 729 (xs_a_q_bc = (xs,a,q,bc)) /\ 730 (code2_a2_q2_bc2 = (code2,a2,q2,bc2)) ==> 731 BC_SUBSTATE bc bc2 /\ 732 (bc2.instr_length = bc.instr_length) /\ 733 (bc2.ok = bc.ok) /\ 734 (q2 = q + iLENGTH bc.instr_length code2)) /\ 735 (!ret x_a_q_bc code2_a2_q2_bc2. BC_ev ret x_a_q_bc code2_a2_q2_bc2 ==> 736 !x a q bc code2 a2 q2 bc2. 737 (x_a_q_bc = (x,a,q,bc)) /\ 738 (code2_a2_q2_bc2 = (code2,a2,q2,bc2)) ==> 739 BC_SUBSTATE bc bc2 /\ 740 (bc2.instr_length = bc.instr_length) /\ 741 (bc2.ok = bc.ok) /\ 742 (q2 = q + iLENGTH bc.instr_length code2))``, 743 HO_MATCH_MP_TAC BC_ev_ind \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 744 \\ POP_ASSUM (MP_TAC o GSYM) 745 \\ ASM_SIMP_TAC std_ss [BC_return_def,LENGTH,LENGTH_APPEND,ADD_ASSOC] 746 \\ REPEAT STRIP_TAC \\ REPEAT 747 (Q.PAT_X_ASSUM `xxx = code2` (MP_TAC o GSYM) 748 \\ ASM_SIMP_TAC std_ss [iLENGTH_APPEND,LENGTH,ADD_ASSOC,LENGTH_n_times,iLENGTH_def] 749 \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC]) 750 \\ SRW_TAC [] [] \\ SIMP_TAC std_ss [iLENGTH_def,BC_ADD_CONST_LENGTH] 751 \\ REPEAT (Q.PAT_X_ASSUM `pn = qn + nnn:num` (fn th => SIMP_TAC std_ss [Once th])) 752 \\ ASM_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC,iLENGTH_APPEND,iLENGTH_APPEND, 753 BC_SUBSTATE_REFL,BC_SUBSTATE_BC_ADD_CONST,BC_ADD_CONST_LENGTH,BC_ADD_CONST_OK] 754 \\ IMP_RES_TAC BC_SUBSTATE_TRANS 755 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM] 756 \\ Q.PAT_X_ASSUM `addr = xx` (fn th => FULL_SIMP_TAC std_ss [Once th]) 757 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM]) 758 |> SIMP_RULE std_ss [PULL_FORALL_IMP,AND_IMP_INTRO]; 759 760val WRITE_BYTECODE_SKIP = prove( 761 ``!xs a bc. 762 ((WRITE_BYTECODE bc a xs).consts = bc.consts) /\ 763 ((WRITE_BYTECODE bc a xs).code_end = bc.code_end) /\ 764 ((WRITE_BYTECODE bc a xs).compiled = bc.compiled) /\ 765 ((WRITE_BYTECODE bc a xs).instr_length = bc.instr_length)``, 766 Induct \\ ASM_SIMP_TAC (srw_ss()) [WRITE_BYTECODE_def]); 767 768val BC_CODE_OK_SKIP = prove( 769 ``(BC_CODE_OK (bc with compiled := x) = BC_CODE_OK bc) /\ 770 (BC_CODE_OK (bc with io_out := y) = BC_CODE_OK bc)``, 771 SIMP_TAC (srw_ss()) [BC_CODE_OK_def]); 772 773val WRITE_BYTECODE_IGNORE1 = prove( 774 ``!xs a i bc. 775 i < a ==> ((WRITE_BYTECODE bc a xs).code i = bc.code i)``, 776 Induct \\ SIMP_TAC std_ss [WRITE_BYTECODE_def,iLENGTH_def] \\ REPEAT STRIP_TAC 777 \\ `~(a = i) /\ i < a + bc.instr_length h` by DECIDE_TAC \\ RES_TAC 778 \\ ASM_SIMP_TAC (srw_ss()) [combinTheory.APPLY_UPDATE_THM]); 779 780val WRITE_BYTECODE_IGNORE2 = prove( 781 ``!xs a i bc. 782 (!h. 0 < bc.instr_length h) /\ 783 a + iLENGTH bc.instr_length xs <= i ==> 784 ((WRITE_BYTECODE bc a xs).code i = bc.code i)``, 785 Induct \\ SIMP_TAC std_ss [WRITE_BYTECODE_def,iLENGTH_def] \\ REPEAT STRIP_TAC 786 \\ FULL_SIMP_TAC std_ss [ADD_ASSOC] \\ RES_TAC 787 \\ `bc.instr_length = (bc with code := (a =+ SOME h) bc.code).instr_length` by SRW_TAC [] [] 788 \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) [] 789 \\ `0 < bc.instr_length h` by METIS_TAC [] 790 \\ `~(a = i)` by DECIDE_TAC \\ ASM_SIMP_TAC (srw_ss()) [combinTheory.APPLY_UPDATE_THM]); 791 792val WRITE_BYTECODE_code_end = store_thm("WRITE_BYTECODE_code_end", 793 ``!xs a bc. ((WRITE_BYTECODE bc a xs).code_end = bc.code_end) /\ 794 ((WRITE_BYTECODE bc a xs).instr_length = bc.instr_length) /\ 795 ((WRITE_BYTECODE bc a xs).consts = bc.consts) /\ 796 ((WRITE_BYTECODE bc a xs).compiled = bc.compiled) /\ 797 ((WRITE_BYTECODE bc a xs).io_out = bc.io_out) /\ 798 ((WRITE_BYTECODE bc a xs).ok = bc.ok)``, 799 Induct \\ FULL_SIMP_TAC (srw_ss()) [WRITE_BYTECODE_def]); 800 801val BC_SUBSTATE_ONLY_COMPILE = store_thm("BC_SUBSTATE_ONLY_COMPILE", 802 ``!bc. BC_SUBSTATE bc (BC_ONLY_COMPILE (params,body,bc))``, 803 SIMP_TAC std_ss [BC_ONLY_COMPILE_def,LET_DEF] \\ REPEAT STRIP_TAC 804 \\ `?x y z bc8. BC_ev_fun (params,body,bc) = (x,y,z,bc8)` by METIS_TAC [PAIR] 805 \\ REVERSE (Cases_on `BC_JUMPS_OK bc`) THEN1 806 (FULL_SIMP_TAC std_ss [BC_ev_fun_def,WRITE_BYTECODE_def,iLENGTH_def] 807 \\ REPEAT (Q.PAT_X_ASSUM `yyy = xxx` (MP_TAC o GSYM)) \\ REPEAT STRIP_TAC 808 \\ FULL_SIMP_TAC std_ss [BC_ev_fun_def,WRITE_BYTECODE_def,iLENGTH_def] 809 \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `[]` \\ EVAL_TAC) 810 \\ ASM_SIMP_TAC std_ss [] \\ IMP_RES_TAC BC_ev_fun_IMP 811 \\ IMP_RES_TAC BC_ev_LENGTH \\ ASM_SIMP_TAC std_ss [] 812 \\ MATCH_MP_TAC BC_SUBSTATE_TRANS \\ Q.EXISTS_TAC `bc8` 813 \\ STRIP_TAC THEN1 METIS_TAC [BC_SUBSTATE_TRANS] 814 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,WRITE_BYTECODE_SKIP,WRITE_BYTECODE_code_end] 815 \\ Cases_on `BC_CODE_OK bc8` \\ FULL_SIMP_TAC std_ss [] 816 \\ POP_ASSUM MP_TAC 817 \\ ASM_SIMP_TAC (srw_ss()) [BC_CODE_OK_def,WRITE_BYTECODE_SKIP] 818 \\ Q.PAT_X_ASSUM `bc8.instr_length = bc1.instr_length` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 819 \\ Q.SPEC_TAC (`bc8.code_end`,`a`) \\ REPEAT STRIP_TAC THEN1 820 (MATCH_MP_TAC WRITE_BYTECODE_IGNORE1 \\ CCONTR_TAC 821 \\ FULL_SIMP_TAC std_ss [NOT_LESS] \\ RES_TAC \\ FULL_SIMP_TAC std_ss []) 822 \\ IMP_RES_TAC WRITE_BYTECODE_IGNORE2 \\ ASM_SIMP_TAC std_ss [] 823 \\ `a <= i` by DECIDE_TAC \\ ASM_SIMP_TAC std_ss []); 824 825val BC_COMPILE_SUBSTATE = prove( 826 ``!bc1 bc2. 827 (FUN_LOOKUP bc1.compiled fname = NONE) /\ (BC_COMPILE (fname,params,body,bc1) = bc2) ==> 828 BC_SUBSTATE bc1 bc2``, 829 SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 830 \\ SIMP_TAC std_ss [BC_COMPILE_def,LET_DEF] 831 \\ MATCH_MP_TAC BC_SUBSTATE_TRANS 832 \\ Q.EXISTS_TAC `BC_STORE_COMPILED bc1 fname (bc1.code_end,LENGTH params)` 833 \\ ASM_SIMP_TAC std_ss [BC_SUBSTATE_ONLY_COMPILE] 834 \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC THEN1 (METIS_TAC []) 835 \\ Q.EXISTS_TAC `[]` \\ EVAL_TAC); 836 837val BC_SUBSTATE_COMPILE = save_thm("BC_SUBSTATE_COMPILE", 838 SIMP_RULE std_ss [] BC_COMPILE_SUBSTATE); 839 840val iSTEP_BC_SUBSTATE_LEMMA = prove( 841 ``iSTEP (xs1,p1,rs1,bc1) (xs2,p2,rs2,bc2) ==> 842 BC_SUBSTATE bc1 bc2``, 843 SIMP_TAC std_ss [iSTEP_cases,BC_SUBSTATE_def] \\ REPEAT STRIP_TAC 844 \\ SIMP_TAC (srw_ss()) [APPEND_NIL,BC_PRINT_def,BC_STORE_COMPILED_def] 845 \\ IMP_RES_TAC BC_ev_LENGTH \\ IMP_RES_TAC BC_COMPILE_SUBSTATE 846 \\ FULL_SIMP_TAC (srw_ss()) [APPEND_NIL,BC_PRINT_def,BC_SUBSTATE_def, 847 BC_CODE_OK_SKIP,BC_FAIL_def,BC_CODE_OK_def]); 848 849val iSTEP_BC_SUBSTATE = prove( 850 ``!x y. RTC iSTEP x y ==> 851 let (xs1,p1,rs1,bc1) = x in 852 let (xs2,p2,rs2,bc2) = y in 853 BC_SUBSTATE bc1 bc2``, 854 HO_MATCH_MP_TAC RTC_INDUCT \\ FULL_SIMP_TAC std_ss [FORALL_PROD,LET_DEF] 855 \\ REPEAT STRIP_TAC THEN1 SIMP_TAC std_ss [BC_SUBSTATE_REFL] 856 \\ IMP_RES_TAC iSTEP_BC_SUBSTATE_LEMMA 857 \\ IMP_RES_TAC BC_SUBSTATE_TRANS) 858 |> Q.SPECL [`(xs1,p1,rs1,bc1)`,`(xs2,p2,rs2,bc2)`] 859 |> SIMP_RULE std_ss [LET_DEF]; 860 861 862(* prove that translation is semantics preserving *) 863 864val VARS_IN_STACK_def = Define ` 865 VARS_IN_STACK env stack alist_placement = 866 !v. v IN FDOM env ==> 867 ?n. (var_lookup 0 v alist_placement = SOME n) /\ 868 (env ' v = EL n stack) /\ 869 n < LENGTH stack`; 870 871val STACK_INV_def = Define ` 872 STACK_INV env stack alist_placement = 873 VARS_IN_STACK env stack alist_placement /\ 874 LENGTH alist_placement <= LENGTH stack`; 875 876val var_lookup_aux_thm = prove( 877 ``!a v n k. 878 (var_lookup n v a = SOME k) = (var_lookup 0 v a = SOME (k-n)) /\ n <= k``, 879 Induct \\ SIMP_TAC std_ss [var_lookup_def] \\ REPEAT STRIP_TAC 880 \\ Cases_on `ssVAR v = h` \\ POP_ASSUM MP_TAC \\ SIMP_TAC std_ss [] 881 THEN1 (STRIP_TAC \\ DECIDE_TAC) \\ ONCE_ASM_REWRITE_TAC [] 882 \\ SIMP_TAC std_ss [DECIDE ``1<=k-n /\ n <= k = n+1<=(k:num)``,GSYM CONJ_ASSOC] 883 \\ POP_ASSUM (K ALL_TAC) \\ Cases_on `n+1<=k` \\ ASM_SIMP_TAC std_ss [SUB_PLUS]); 884 885val var_lookup_aux = prove( 886 ``!a v n m. 887 (var_lookup n v a = SOME k) ==> (var_lookup (n + m) v a = SOME (k + m))``, 888 ONCE_REWRITE_TAC [var_lookup_aux_thm] \\ ASM_SIMP_TAC std_ss [] 889 \\ REPEAT STRIP_TAC \\ DECIDE_TAC); 890 891val STACK_INV_lemma = prove( 892 ``(STACK_INV env (result::stack) (ssTEMP::a) = STACK_INV env stack a)``, 893 EQ_TAC THEN1 894 (SIMP_TAC std_ss [STACK_INV_def,VARS_IN_STACK_def,LENGTH] 895 \\ REPEAT STRIP_TAC \\ RES_TAC 896 \\ FULL_SIMP_TAC std_ss [var_lookup_def,stack_slot_11,stack_slot_distinct] 897 \\ Q.PAT_X_ASSUM `bbb = SOME n` (STRIP_ASSUME_TAC o RW1[var_lookup_aux_thm]) 898 \\ ASM_SIMP_TAC std_ss [] \\ Cases_on `n` 899 \\ FULL_SIMP_TAC std_ss [EL,TL,ADD1,LENGTH] \\ DECIDE_TAC) 900 \\ SIMP_TAC std_ss [STACK_INV_def,VARS_IN_STACK_def] 901 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ REPEAT STRIP_TAC \\ RES_TAC 902 \\ Q.EXISTS_TAC `SUC n` \\ FULL_SIMP_TAC std_ss [var_lookup_def,LENGTH,EL,TL] 903 \\ IMP_RES_TAC var_lookup_aux \\ FULL_SIMP_TAC std_ss [ADD1,stack_slot_distinct]); 904 905val STACK_INV_lemma2 = prove( 906 ``!result. 907 STACK_INV env (result ++ stack) (MAP (\x.ssTEMP) result ++ a) = 908 STACK_INV env stack a``, 909 Induct \\ ASM_SIMP_TAC std_ss [APPEND,MAP,STACK_INV_lemma]); 910 911val LENGTH_LESS_EQ_LENGTH_IMP = prove( 912 ``!a args. LENGTH args <= LENGTH a ==> 913 ?a1 a2. (a = a1 ++ a2) /\ (LENGTH args = LENGTH a1)``, 914 Induct THEN1 (SIMP_TAC std_ss [LENGTH] \\ METIS_TAC [APPEND,LENGTH]) 915 \\ REPEAT STRIP_TAC \\ Cases_on `args` THEN1 METIS_TAC [APPEND,LENGTH] 916 \\ FULL_SIMP_TAC std_ss [LENGTH] \\ METIS_TAC [APPEND,LENGTH]); 917 918val IMP_MAP_NONE = prove( 919 ``(LENGTH args = LENGTH a1) /\ EVERY (\x. x = ssTEMP) a1 ==> 920 (a1 = MAP (\x. ssTEMP) (REVERSE args))``, 921 ONCE_REWRITE_TAC [GSYM LENGTH_REVERSE] \\ Q.SPEC_TAC (`REVERSE args`,`xs`) 922 \\ SIMP_TAC std_ss [LENGTH_REVERSE] \\ Q.SPEC_TAC (`a1`,`ys`) \\ Induct 923 \\ Cases_on `xs` \\ ASM_SIMP_TAC std_ss [CONS_11,LENGTH,MAP,ADD1,EVERY_DEF]); 924 925val STACK_INV_FUPDATE = prove( 926 ``STACK_INV env stack a ==> 927 STACK_INV (env |+ (v,x')) (x'::stack) (ssVAR v::a)``, 928 SIMP_TAC std_ss [STACK_INV_def,VARS_IN_STACK_def] 929 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [FAPPLY_FUPDATE_THM,FDOM_FUPDATE] 930 \\ Cases_on `v' = v` \\ FULL_SIMP_TAC std_ss [var_lookup_def,EL,HD,LENGTH] 931 \\ FULL_SIMP_TAC std_ss [IN_INSERT,stack_slot_11] \\ RES_TAC 932 \\ ONCE_REWRITE_TAC [var_lookup_aux_thm] 933 \\ Q.EXISTS_TAC `SUC n` \\ SIMP_TAC std_ss [EL,TL] 934 \\ ASM_SIMP_TAC std_ss [ADD1]); 935 936val FDOM_VarBindAux = prove( 937 ``!xs ys v. (LENGTH xs = LENGTH ys) ==> (v IN FDOM (VarBindAux xs ys) = MEM v xs)``, 938 Induct \\ SIMP_TAC std_ss [VarBindAux_def,MEM,FDOM_FEMPTY,NOT_IN_EMPTY] 939 \\ Cases_on `ys` \\ SIMP_TAC std_ss [LENGTH,ADD1,VarBindAux_def] 940 \\ SIMP_TAC std_ss [FDOM_FUPDATE,IN_INSERT] \\ METIS_TAC []); 941 942val IN_UNION_LEMMA = prove( 943 ``x IN (s UNION t) = x IN s \/ (~(x IN s) /\ x IN t)``, 944 SIMP_TAC std_ss [IN_UNION] \\ METIS_TAC []); 945 946val EL_LENGTH_APPEND = prove( 947 ``!xs n ys. EL (LENGTH xs + n) (xs ++ ys) = EL n ys``, 948 Induct \\ ASM_SIMP_TAC std_ss [LENGTH,APPEND,EL,TL,ADD_CLAUSES]); 949 950val VARS_IN_STACK_VarBind_THM = prove( 951 ``!params args. 952 VARS_IN_STACK a stack xs /\ 953 (LENGTH (params:string list) = LENGTH (args:SExp list)) ==> 954 VARS_IN_STACK (FUNION (VarBind params args) a) (REVERSE args ++ stack) 955 (MAP ssVAR (REVERSE params) ++ xs)``, 956 SIMP_TAC std_ss [VarBind_def] \\ NTAC 2 STRIP_TAC 957 \\ ONCE_REWRITE_TAC [GSYM LENGTH_REVERSE] 958 \\ Q.SPEC_TAC (`REVERSE args`,`ys`) 959 \\ Q.SPEC_TAC (`REVERSE params:string list`,`xss`) 960 \\ SIMP_TAC std_ss [VARS_IN_STACK_def,FDOM_VarBindAux,FUNION_DEF,IN_UNION_LEMMA] 961 \\ SIMP_TAC std_ss [METIS_PROVE [] ``b \/ (~b /\ c) = (~b ==> c)``] 962 \\ Induct \\ SIMP_TAC std_ss [MEM,MAP,APPEND,LENGTH] THEN1 963 (REPEAT STRIP_TAC \\ `ys = []` by METIS_TAC [LENGTH_NIL] 964 \\ FULL_SIMP_TAC std_ss [APPEND]) 965 \\ REPEAT STRIP_TAC 966 \\ Cases_on `v = h` \\ FULL_SIMP_TAC std_ss [] THEN1 967 (Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 968 \\ Q.EXISTS_TAC `0` \\ SIMP_TAC std_ss [LENGTH,ADD1,LENGTH_APPEND] 969 \\ FULL_SIMP_TAC std_ss [VarBindAux_def,FAPPLY_FUPDATE_THM,EL,HD,APPEND, 970 var_lookup_def] \\ DECIDE_TAC) 971 \\ Cases_on `MEM v xss` \\ FULL_SIMP_TAC std_ss [] THEN1 972 (Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 973 \\ FULL_SIMP_TAC (srw_ss()) [VarBindAux_def,FAPPLY_FUPDATE_THM,EL,HD,APPEND, 974 var_lookup_def] \\ Q.PAT_X_ASSUM `!ys.bb` MP_TAC 975 \\ Q.PAT_X_ASSUM `!ys.bb` (MP_TAC o Q.SPEC `v` o RW [] o Q.SPEC `t`) 976 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 977 \\ Q.EXISTS_TAC `SUC n` \\ FULL_SIMP_TAC std_ss [EL,TL] 978 \\ ONCE_REWRITE_TAC [var_lookup_aux_thm] 979 \\ ASM_SIMP_TAC std_ss [ADD1] \\ DECIDE_TAC) 980 \\ Cases_on `ys` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1] 981 \\ Q.PAT_X_ASSUM `!ys.bb` MP_TAC 982 \\ Q.PAT_X_ASSUM `!ys.bb` (MP_TAC o Q.SPEC `v` o RW [] o Q.SPEC `t`) 983 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 984 \\ Q.EXISTS_TAC `SUC n` \\ FULL_SIMP_TAC std_ss [EL,TL,APPEND] 985 \\ ASM_SIMP_TAC (srw_ss()) [var_lookup_def] 986 \\ ONCE_REWRITE_TAC [var_lookup_aux_thm] 987 \\ ASM_SIMP_TAC std_ss [ADD1] \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND] \\ DECIDE_TAC) 988 989val VARS_IN_STACK_VarBind = prove( 990 ``!params args. 991 (LENGTH (params:string list) = LENGTH (args:SExp list)) ==> 992 VARS_IN_STACK (VarBind params args) (REVERSE args ++ stack) 993 (MAP ssVAR (REVERSE params))``, 994 NTAC 2 STRIP_TAC 995 \\ MATCH_MP_TAC (RW [APPEND_NIL,FUNION_FEMPTY_2,GSYM AND_IMP_INTRO] 996 (Q.INST [`a`|->`FEMPTY`,`xs`|->`[]`] VARS_IN_STACK_VarBind_THM)) 997 \\ EVAL_TAC \\ SIMP_TAC std_ss []); 998 999val STACK_INV_VarBind_2 = prove( 1000 ``!params args p stack. 1001 STACK_INV a stack xs /\ 1002 (LENGTH (params:string list) = LENGTH (args:SExp list)) ==> 1003 STACK_INV (FUNION (VarBind params args) a) (REVERSE args ++ stack) 1004 (MAP ssVAR (REVERSE params) ++ xs)``, 1005 SIMP_TAC std_ss [STACK_INV_def,VARS_IN_STACK_VarBind_THM, 1006 LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE]); 1007 1008val STACK_INV_VarBind = prove( 1009 ``!params args p stack. 1010 (LENGTH (params:string list) = LENGTH (args:SExp list)) ==> 1011 STACK_INV (VarBind params args) (REVERSE args ++ stack) 1012 (MAP ssVAR (REVERSE params))``, 1013 SIMP_TAC std_ss [STACK_INV_def,STACK_INV_lemma,APPEND,VARS_IN_STACK_VarBind, 1014 isVal_def,LENGTH,LENGTH_APPEND,LENGTH_REVERSE,LENGTH_MAP]); 1015 1016val BC_FNS_ASSUM_def = Define ` 1017 BC_FNS_ASSUM fns bc = 1018 !fc params exp. 1019 fc IN FDOM fns /\ (fns ' fc = (params,exp)) ==> 1020 ?p pcode a5 bc4 bc5. 1021 CONTAINS_BYTECODE bc p pcode /\ 1022 (FUN_LOOKUP bc.compiled fc = SOME (p,LENGTH params)) /\ 1023 BC_ev T (exp,MAP ssVAR (REVERSE params),p,bc4) 1024 (pcode,a5,p + iLENGTH bc.instr_length pcode,bc5) /\ 1025 BC_SUBSTATE bc5 bc`; 1026 1027val BC_REFINES_def = Define ` 1028 BC_REFINES (fns,io) bc = 1029 BC_FNS_ASSUM fns bc /\ (bc.io_out = io) /\ BC_CODE_OK bc /\ 1030 ({ j |j| ~(FUN_LOOKUP bc.compiled j = NONE)} = FDOM fns) /\ 1031 !j. bc.code_end <= j ==> (bc.code j = NONE)`; 1032 1033val iSTEP_ret_state_def = Define ` 1034 iSTEP_ret_state a2 (result,stack,r,rs,bc) = 1035 (result::DROP (LENGTH a2) stack,r,rs,bc)`; 1036 1037val gen_pops_thm = prove( 1038 ``CONTAINS_BYTECODE bc p (gen_pops (LENGTH xs)) ==> 1039 RTC iSTEP (a::xs++stack,p,rs,bc) 1040 (a::stack,p + iLENGTH bc.instr_length (gen_pops (LENGTH xs)),rs,bc)``, 1041 SRW_TAC [] [gen_pops_def,LENGTH_NIL,iLENGTH_def] 1042 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 1043 \\ MATCH_MP_TAC iSTEP_cases_imp 1044 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,CONTAINS_BYTECODE_def, 1045 LENGTH,CONS_11,STACK_INV_lemma,LENGTH_APPEND,APPEND,iLENGTH_def,BC_STEP_def] 1046 \\ METIS_TAC []); 1047 1048val gen_popn_thm = prove( 1049 ``CONTAINS_BYTECODE bc p (gen_popn (LENGTH xs)) ==> 1050 RTC iSTEP (xs++stack,p,rs,bc) 1051 (stack,p+iLENGTH bc.instr_length (gen_popn (LENGTH xs)),rs,bc)``, 1052 SRW_TAC [] [gen_popn_def,LENGTH_NIL,CONTAINS_BYTECODE_def,iLENGTH_def,iLENGTH_APPEND] 1053 \\ Cases_on `xs` \\ FULL_SIMP_TAC std_ss [LENGTH,ADD1,ADD_ASSOC] 1054 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] 1055 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] \\ REPEAT STRIP_TAC 1056 \\ Q.EXISTS_TAC `(h::stack,p + iLENGTH bc.instr_length (gen_pops (LENGTH t)),rs,bc)` 1057 \\ IMP_RES_TAC gen_pops_thm \\ ASM_SIMP_TAC std_ss [] 1058 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 1059 \\ MATCH_MP_TAC iSTEP_cases_imp 1060 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_def] 1061 \\ ASM_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,CONTAINS_BYTECODE_def, 1062 LENGTH,CONS_11,STACK_INV_lemma,LENGTH_APPEND,APPEND,NOT_CONS_NIL,BC_STEP_def]); 1063 1064val BC_return_code_thm = prove( 1065 ``CONTAINS_BYTECODE bc p (BC_return_code T (ssTEMP::a2)) /\ 1066 STACK_INV a stack a2 ==> 1067 RTC iSTEP (result::stack,p,r::rs,bc) (iSTEP_ret_state a2 (result,stack,r,rs,bc))``, 1068 SIMP_TAC std_ss [BC_return_code_def,LENGTH,ADD1,ADD_SUB] 1069 \\ SIMP_TAC std_ss [iSTEP_ret_state_def] 1070 \\ SIMP_TAC std_ss [STACK_INV_def,CONTAINS_BYTECODE_APPEND] 1071 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] \\ REPEAT STRIP_TAC 1072 \\ Q.EXISTS_TAC `(result::DROP (LENGTH a2)stack,(p + iLENGTH bc.instr_length (gen_pops (LENGTH a2))),r::rs,bc)` 1073 \\ REVERSE STRIP_TAC THEN1 1074 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 1075 \\ MATCH_MP_TAC iSTEP_cases_imp 1076 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_def] 1077 \\ ASM_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,CONTAINS_BYTECODE_def, 1078 LENGTH,CONS_11,STACK_INV_lemma,LENGTH_APPEND,APPEND,NOT_CONS_NIL,BC_STEP_def]) 1079 \\ IMP_RES_TAC LENGTH_LESS_EQ_LENGTH_IMP 1080 \\ FULL_SIMP_TAC std_ss [rich_listTheory.BUTFIRSTN_LENGTH_APPEND] 1081 \\ FULL_SIMP_TAC std_ss [GSYM APPEND] 1082 \\ MATCH_MP_TAC gen_pops_thm \\ ASM_SIMP_TAC std_ss []); 1083 1084val DROP_LENGTH_ADD = prove( 1085 ``!xs ys n. DROP (LENGTH xs + n) (xs ++ ys) = DROP n ys``, 1086 Induct \\ SIMP_TAC std_ss [LENGTH,APPEND,DROP_def,ADD1] 1087 \\ REPEAT STRIP_TAC \\ `LENGTH xs + 1 + n - 1 = LENGTH xs + n` by DECIDE_TAC 1088 \\ ASM_SIMP_TAC std_ss []); 1089 1090val iSTEP_ret_state_APPEND_MAP = prove( 1091 ``(LENGTH ys = LENGTH xs) ==> 1092 (iSTEP_ret_state (MAP f (REVERSE xs) ++ a2) 1093 (result,REVERSE ys ++ stack,r,rs,bc) = 1094 iSTEP_ret_state a2 (result,stack,r,rs,bc))``, 1095 SIMP_TAC std_ss [iSTEP_ret_state_def,LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE] 1096 \\ ONCE_REWRITE_TAC [GSYM LENGTH_REVERSE] \\ METIS_TAC [DROP_LENGTH_ADD]); 1097 1098val n_times_iSTORE = prove( 1099 ``!ys args xs bc p stack rs. 1100 (LENGTH ys = LENGTH args) /\ 1101 CONTAINS_BYTECODE bc p (n_times (LENGTH args) (iSTORE (LENGTH (args++xs)-1))) ==> 1102 RTC iSTEP (args++xs++ys++stack,p,rs,bc) 1103 (xs++args++stack,p+iLENGTH bc.instr_length (n_times (LENGTH args) (iSTORE (LENGTH (args++xs)-1))),rs,bc)``, 1104 Induct \\ Cases_on `args` 1105 \\ SIMP_TAC std_ss [APPEND,APPEND_NIL,RTC_REFL,LENGTH,ADD1] 1106 \\ SIMP_TAC std_ss [GSYM ADD1,n_times_def,CONTAINS_BYTECODE_def,iLENGTH_def] 1107 \\ ASM_SIMP_TAC std_ss [RTC_REFL] 1108 \\ SIMP_TAC std_ss [ADD1] \\ NTAC 7 STRIP_TAC 1109 \\ Q.PAT_X_ASSUM `!args.bbb` (MP_TAC o Q.SPECL [`t`,`xs++[h]`,`bc`,`p+bc.instr_length (iSTORE (LENGTH (t:SExp list) + LENGTH (xs:SExp list)))`,`stack`,`rs`]) 1110 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH,ADD_ASSOC] 1111 \\ REPEAT STRIP_TAC \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1112 \\ Q.EXISTS_TAC `(t ++ (xs ++ [h]) ++ ys ++ stack,p + bc.instr_length (iSTORE (LENGTH t + LENGTH xs)),rs,bc)` 1113 \\ REVERSE STRIP_TAC \\ RES_TAC 1114 THEN1 (FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND,AC ADD_ASSOC ADD_COMM]) 1115 \\ MATCH_MP_TAC RTC_SINGLE 1116 \\ MATCH_MP_TAC iSTEP_cases_imp 1117 \\ ASM_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,CONTAINS_BYTECODE_def, 1118 LENGTH,CONS_11,STACK_INV_lemma,LENGTH_APPEND,BC_STEP_def] 1119 \\ REVERSE STRIP_TAC THEN1 DECIDE_TAC 1120 \\ SIMP_TAC std_ss [APPEND_ASSOC,GSYM LENGTH_APPEND] 1121 \\ Q.SPEC_TAC (`t++xs`,`zs`) 1122 \\ SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 1123 \\ Q.SPEC_TAC (`ys++stack`,`qss`) 1124 \\ Induct_on `zs` \\ ASM_SIMP_TAC std_ss [LENGTH,APPEND,UPDATE_NTH_def,CONS_11]); 1125 1126val n_times_iLOAD = prove( 1127 ``!xs ys bc p stack. 1128 CONTAINS_BYTECODE bc p (n_times (LENGTH xs) (iLOAD (LENGTH (xs ++ ys) - 1))) ==> 1129 RTC iSTEP (ys++xs++stack,p,rs,bc) 1130 (xs++ys++xs++stack,p+iLENGTH bc.instr_length (n_times (LENGTH xs) (iLOAD (LENGTH (xs ++ ys) - 1))),rs,bc)``, 1131 HO_MATCH_MP_TAC rich_listTheory.SNOC_INDUCT 1132 \\ SIMP_TAC std_ss [APPEND_NIL,APPEND,LENGTH,RTC_REFL,n_times_def] 1133 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_def,SNOC_APPEND,APPEND_ASSOC, 1134 LENGTH_APPEND,LENGTH,ADD_CLAUSES,GSYM ADD1,n_times_def,iLENGTH_def,RTC_REFL] 1135 \\ REPEAT STRIP_TAC 1136 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1137 \\ Q.EXISTS_TAC `([x] ++ ys ++ xs ++ [x] ++ stack,p+bc.instr_length(iLOAD (LENGTH xs + LENGTH ys)),rs,bc)` 1138 \\ REPEAT STRIP_TAC THEN1 1139 (MATCH_MP_TAC RTC_SINGLE 1140 \\ MATCH_MP_TAC iSTEP_cases_imp 1141 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,CONTAINS_BYTECODE_def, 1142 LENGTH,CONS_11,STACK_INV_lemma,LENGTH_APPEND,LENGTH_APPEND,BC_STEP_def] 1143 \\ `LENGTH xs + LENGTH ys = LENGTH ys + LENGTH xs` by DECIDE_TAC 1144 \\ FULL_SIMP_TAC std_ss [APPEND,CONS_11] 1145 \\ FULL_SIMP_TAC std_ss [rich_listTheory.EL_APPEND2,GSYM APPEND_ASSOC] 1146 \\ SIMP_TAC std_ss [APPEND,EL,HD] \\ DECIDE_TAC) 1147 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC] 1148 \\ `[x] ++ (ys ++ (xs ++ ([x] ++ stack))) = (x::ys) ++ xs ++ (x::stack)` by 1149 FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 1150 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC] 1151 \\ Q.PAT_X_ASSUM `!ys.bbb` (MP_TAC o Q.SPECL [`x::ys`,`bc`, 1152 `p + bc.instr_length (iLOAD (LENGTH (xs:SExp list) + LENGTH (ys:SExp list)))`,`x::stack`]) 1153 \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,ADD_SUB,ADD_ASSOC]); 1154 1155val LESS_EQ_IMP_APPEND = prove( 1156 ``!n ys. n <= LENGTH ys ==> ?ys1 ys2. (ys = ys1 ++ ys2) /\ (LENGTH ys2 = n)``, 1157 Induct \\ SIMP_TAC std_ss [LENGTH_NIL,APPEND,APPEND_NIL] \\ STRIP_TAC 1158 \\ STRIP_ASSUME_TAC (Q.SPEC `ys` rich_listTheory.SNOC_CASES) 1159 \\ ASM_SIMP_TAC std_ss [LENGTH_SNOC,LENGTH,ADD1] \\ REPEAT STRIP_TAC 1160 \\ RES_TAC \\ Q.EXISTS_TAC `ys1` \\ Q.EXISTS_TAC `ys2++[x]` 1161 \\ ASM_SIMP_TAC std_ss [APPEND,LENGTH,ADD1,LENGTH_SNOC,SNOC_APPEND] 1162 \\ ASM_SIMP_TAC std_ss [APPEND_ASSOC,LENGTH_APPEND,LENGTH]); 1163 1164val BC_ev_CONSTS = prove( 1165 ``(!ret fc_n_a_q_bc code2_a2_q2_bc2. BC_ap ret fc_n_a_q_bc code2_a2_q2_bc2 ==> 1166 !fc n a q bc code2 a2 q2 bc2. 1167 (fc_n_a_q_bc = (fc,n,a,q,bc)) /\ 1168 (code2_a2_q2_bc2 = (code2,a2,q2,bc2)) ==> 1169 (bc2.io_out = bc.io_out) /\ 1170 (bc2.code = bc.code) /\ 1171 (bc2.ok = bc.ok) /\ 1172 (bc2.compiled = bc.compiled) /\ 1173 (bc2.code_end = bc.code_end) /\ 1174 (bc2.instr_length = bc.instr_length)) /\ 1175 (!xs_a_q_bc code2_a2_q2_bc2. BC_evl xs_a_q_bc code2_a2_q2_bc2 ==> 1176 !xs a q bc code2 a2 q2 bc2. 1177 (xs_a_q_bc = (xs,a,q,bc)) /\ 1178 (code2_a2_q2_bc2 = (code2,a2,q2,bc2)) ==> 1179 (bc2.io_out = bc.io_out) /\ 1180 (bc2.code = bc.code) /\ 1181 (bc2.ok = bc.ok) /\ 1182 (bc2.compiled = bc.compiled) /\ 1183 (bc2.code_end = bc.code_end) /\ 1184 (bc2.instr_length = bc.instr_length)) /\ 1185 (!ret x_a_q_bc code2_a2_q2_bc2. BC_ev ret x_a_q_bc code2_a2_q2_bc2 ==> 1186 !x a q bc code2 a2 q2 bc2. 1187 (x_a_q_bc = (x,a,q,bc)) /\ 1188 (code2_a2_q2_bc2 = (code2,a2,q2,bc2)) ==> 1189 (bc2.io_out = bc.io_out) /\ 1190 (bc2.code = bc.code) /\ 1191 (bc2.ok = bc.ok) /\ 1192 (bc2.compiled = bc.compiled) /\ 1193 (bc2.code_end = bc.code_end) /\ 1194 (bc2.instr_length = bc.instr_length))``, 1195 HO_MATCH_MP_TAC BC_ev_ind \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 1196 \\ POP_ASSUM (MP_TAC o GSYM) 1197 \\ ASM_SIMP_TAC std_ss [BC_return_def,LENGTH,LENGTH_APPEND,ADD_ASSOC] 1198 \\ SRW_TAC [] [] \\ SIMP_TAC (srw_ss()) [BC_ADD_CONST_def]) 1199 |> SIMP_RULE std_ss [PULL_FORALL_IMP]; 1200 1201val BC_ev_fun_CONSTS = store_thm("BC_ev_fun_CONSTS", 1202 ``(BC_ev_fun (params,body,bcA) = (new_code,a2,q2,bcB)) /\ BC_JUMPS_OK bcA ==> 1203 (bcA.code = bcB.code) /\ (bcA.code_end = bcB.code_end) /\ 1204 (bcA.instr_length = bcB.instr_length) /\ (bcA.io_out = bcB.io_out) /\ 1205 (bcA.compiled = bcB.compiled) /\ 1206 (bcA.ok = bcB.ok)``, 1207 STRIP_TAC \\ IMP_RES_TAC BC_ev_fun_IMP 1208 \\ IMP_RES_TAC BC_ev_CONSTS \\ ASM_SIMP_TAC std_ss []); 1209 1210val WRITE_BYTECODE_io_out = prove( 1211 ``!xs a bc. ((WRITE_BYTECODE bc a xs).io_out = bc.io_out) /\ 1212 ((WRITE_BYTECODE bc a xs).ok = bc.ok)``, 1213 Induct \\ FULL_SIMP_TAC (srw_ss()) [WRITE_BYTECODE_def]); 1214 1215val BC_ev_fun_io_out = prove( 1216 ``(BC_ev_fun(params,body,bc) = (z1,z2,z3,bc2)) ==> (bc.io_out = bc2.io_out) /\ 1217 (bc.ok = bc2.ok)``, 1218 Cases_on `BC_JUMPS_OK bc` THEN1 (METIS_TAC [BC_ev_fun_CONSTS]) 1219 \\ ASM_SIMP_TAC std_ss [BC_ev_fun_def]); 1220 1221val BC_ONLY_COMPILE_io_out = store_thm("BC_ONLY_COMPILE_io_out", 1222 ``((BC_ONLY_COMPILE (params,body,bc)).io_out = bc.io_out) /\ 1223 ((BC_ONLY_COMPILE (params,body,bc)).ok = bc.ok)``, 1224 SIMP_TAC std_ss [BC_ONLY_COMPILE_def,LET_DEF,BC_ev_fun_io_out] 1225 \\ `?z1 z2 z3 bc2. BC_ev_fun(params,body,bc) = (z1,z2,z3,bc2)` by METIS_TAC [PAIR] 1226 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC BC_ev_fun_io_out 1227 \\ FULL_SIMP_TAC (srw_ss()) [WRITE_BYTECODE_io_out]); 1228 1229val BC_COMPILE_io_out = store_thm("BC_COMPILE_io_out", 1230 ``((BC_COMPILE (fname,params,body,bc)).io_out = bc.io_out) /\ 1231 ((BC_COMPILE (fname,params,body,bc)).ok = bc.ok)``, 1232 SIMP_TAC std_ss [BC_COMPILE_def,LET_DEF,BC_ONLY_COMPILE_io_out] \\ EVAL_TAC); 1233 1234fun MOVE_TAC (gs,tm) = if is_forall tm then STRIP_TAC (gs,tm) else 1235 if is_imp tm then STRIP_TAC (gs,tm) else NO_TAC (gs,tm) 1236 1237val n_times_APPEND = prove( 1238 ``!k x xs. n_times k x ++ x::xs = n_times (SUC k) x ++ xs``, 1239 Induct \\ ASM_SIMP_TAC std_ss [n_times_def,APPEND]); 1240 1241val n_times_iCONST = prove( 1242 ``!k a stack env bc p. 1243 CONTAINS_BYTECODE bc p (n_times k (iCONST_SYM "NIL")) /\ 1244 STACK_INV env stack a ==> 1245 STACK_INV env (n_times k (Sym "NIL") ++ stack) (n_times k ssTEMP ++ a) /\ 1246 RTC iSTEP (stack,p,r::rs,bc) (n_times k (Sym "NIL") ++ stack,p + iLENGTH bc.instr_length (n_times k (iCONST_SYM "NIL")),r::rs,bc)``, 1247 Induct \\ SIMP_TAC std_ss [n_times_def,APPEND,iLENGTH_def,RTC_REFL] 1248 \\ REPEAT MOVE_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_def] 1249 \\ `STACK_INV env (Sym "NIL"::stack) (ssTEMP::a)` by 1250 ASM_SIMP_TAC std_ss [STACK_INV_lemma,LENGTH,ADD1,AC ADD_ASSOC ADD_COMM] 1251 \\ RES_TAC \\ ASM_SIMP_TAC std_ss [STACK_INV_lemma,LENGTH,ADD1,AC ADD_ASSOC ADD_COMM] 1252 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1253 \\ Q.EXISTS_TAC `(Sym "NIL" :: stack,p+bc.instr_length(iCONST_SYM "NIL"),r::rs,bc)` \\ STRIP_TAC THEN1 1254 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 1255 \\ MATCH_MP_TAC iSTEP_cases_imp 1256 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,CONTAINS_BYTECODE_def, 1257 LENGTH,CONS_11,STACK_INV_lemma,EL,STACK_INV_def,BC_STEP_def] 1258 \\ FULL_SIMP_TAC std_ss [LENGTH_NIL,DECIDE ``0<n = ~(n = 0:num)``]) 1259 \\ FULL_SIMP_TAC std_ss [HD,GSYM n_times_def,GSYM APPEND,n_times_APPEND] 1260 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM]) 1261 1262val MAP_EQ_GENLIST = prove( 1263 ``!xs. MAP (\x.b) xs = GENLIST (\x.b) (LENGTH xs)``, 1264 HO_MATCH_MP_TAC rich_listTheory.SNOC_INDUCT 1265 \\ SRW_TAC [] [] \\ ASM_SIMP_TAC std_ss [] 1266 \\ SIMP_TAC std_ss [GENLIST,GSYM ADD1,SNOC_APPEND]); 1267 1268val MAP_CONST_REVERSE = prove( 1269 ``MAP (\x.b) (REVERSE xs) = MAP (\x.b) xs``, 1270 FULL_SIMP_TAC std_ss [MAP_EQ_GENLIST,LENGTH_REVERSE]); 1271 1272val BC_SUBSTATE_IMP = prove( 1273 ``(bc.code p = SOME x) /\ BC_SUBSTATE bc bc1 /\ BC_REFINES (y1,y2) bc ==> 1274 (bc1.code p = SOME x)``, 1275 SIMP_TAC std_ss [BC_SUBSTATE_def,BC_REFINES_def] \\ METIS_TAC []); 1276 1277val BC_SUBSTATE_BYTECODE = prove( 1278 ``!code p il ns ns1. 1279 CONTAINS_BYTECODE bc p code /\ BC_SUBSTATE bc bc1 /\ BC_REFINES (y1,y2) bc ==> 1280 CONTAINS_BYTECODE bc1 p code``, 1281 Induct \\ SIMP_TAC std_ss [CONTAINS_BYTECODE_def] 1282 \\ METIS_TAC [BC_SUBSTATE_IMP,BC_SUBSTATE_def]); 1283 1284val BC_SUBSTATE_IMP_OK = prove( 1285 ``(bc.code p = SOME x) /\ BC_SUBSTATE bc bc1 /\ BC_CODE_OK bc ==> 1286 (bc1.code p = SOME x)``, 1287 SIMP_TAC std_ss [BC_SUBSTATE_def,BC_CODE_OK_def] \\ METIS_TAC []); 1288 1289val BC_SUBSTATE_BYTECODE_OK = prove( 1290 ``!code p il ns ns1. 1291 CONTAINS_BYTECODE bc p code /\ BC_SUBSTATE bc bc1 /\ BC_CODE_OK bc ==> 1292 CONTAINS_BYTECODE bc1 p code``, 1293 Induct \\ SIMP_TAC std_ss [CONTAINS_BYTECODE_def] 1294 \\ METIS_TAC [BC_SUBSTATE_IMP_OK,BC_SUBSTATE_def]); 1295 1296val BC_call_thm = prove( 1297 ``!fc n. 1298 CONTAINS_BYTECODE bc p (BC_call T (fc,n,NONE)) /\ (FUN_LOOKUP bc.compiled fc = SOME (pos,n)) ==> 1299 RTC iSTEP (stack,p,rs,bc) (stack,pos,rs,bc)``, 1300 SIMP_TAC std_ss [BC_call_def,BC_call_aux_def,CONTAINS_BYTECODE_def] \\ REPEAT STRIP_TAC 1301 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1302 \\ Q.EXISTS_TAC `(Val n::stack,p + bc.instr_length (iCONST_NUM n),rs,bc)` 1303 \\ STRIP_TAC THEN1 1304 (REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 1305 \\ MATCH_MP_TAC iSTEP_cases_imp 1306 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,ADD_ASSOC,isVal_def, 1307 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND,iLENGTH_APPEND, 1308 iLENGTH_def,CONTAINS_BYTECODE_def,BC_STEP_def]) 1309 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1310 \\ Q.EXISTS_TAC `(Sym fc::Val n::stack,p + bc.instr_length (iCONST_NUM n) + bc.instr_length (iCONST_SYM fc),rs,bc)` 1311 \\ STRIP_TAC THEN1 1312 (REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 1313 \\ MATCH_MP_TAC iSTEP_cases_imp 1314 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,ADD_ASSOC, 1315 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND,iLENGTH_APPEND, 1316 iLENGTH_def,CONTAINS_BYTECODE_def,BC_STEP_def]) 1317 THEN1 1318 (REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 1319 \\ MATCH_MP_TAC iSTEP_cases_imp 1320 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,ADD_ASSOC, 1321 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND,iLENGTH_APPEND, 1322 iLENGTH_def,CONTAINS_BYTECODE_def,BC_STEP_def] 1323 \\ METIS_TAC [])); 1324 1325val IMP_IMP = METIS_PROVE [] ``b /\ (c ==> d) ==> ((b ==> c) ==> d)`` 1326 1327val BC_PRINT_CONTAINS_BYTECODE = prove( 1328 ``!code p bc s. 1329 CONTAINS_BYTECODE (BC_PRINT bc s) p code = CONTAINS_BYTECODE bc p code``, 1330 Induct \\ ASM_SIMP_TAC std_ss [CONTAINS_BYTECODE_def] 1331 \\ SIMP_TAC (srw_ss()) [BC_PRINT_def]); 1332 1333val BC_FAIL_CONTAINS_BYTECODE = prove( 1334 ``!code p bc s. 1335 CONTAINS_BYTECODE (BC_FAIL bc) p code = CONTAINS_BYTECODE bc p code``, 1336 Induct \\ ASM_SIMP_TAC std_ss [CONTAINS_BYTECODE_def] 1337 \\ SIMP_TAC (srw_ss()) [BC_FAIL_def]); 1338 1339val n_times_CONS = prove( 1340 ``!args p stack. 1341 CONTAINS_BYTECODE bc p 1342 ([iCONST_SYM "NIL"] ++ n_times (LENGTH args) (iDATA opCONS)) ==> 1343 iSTEP^* (REVERSE args ++ stack,p,rs,bc) 1344 (list2sexp args::stack,p + iLENGTH bc.instr_length ([iCONST_SYM "NIL"] ++ n_times (LENGTH args) (iDATA opCONS)),rs,bc)``, 1345 Induct (* HO_MATCH_MP_TAC rich_listTheory.SNOC_INDUCT *) \\ REPEAT STRIP_TAC THEN1 1346 (FULL_SIMP_TAC std_ss [REVERSE_DEF,APPEND,n_times_def,LENGTH,list2sexp_def] 1347 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 1348 \\ MATCH_MP_TAC iSTEP_cases_imp 1349 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1350 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def]) 1351 \\ SIMP_TAC std_ss [REVERSE_DEF,GSYM APPEND_ASSOC,APPEND,LENGTH] 1352 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1353 \\ FULL_SIMP_TAC std_ss [GSYM (RW [APPEND_NIL] (Q.SPECL [`n`,`x`,`[]`] n_times_APPEND)),LENGTH] 1354 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC] \\ POP_ASSUM MP_TAC 1355 \\ SIMP_TAC std_ss [Once CONTAINS_BYTECODE_APPEND] \\ REPEAT STRIP_TAC 1356 \\ Q.EXISTS_TAC `(list2sexp args::h::stack, 1357 p + iLENGTH bc.instr_length ([iCONST_SYM "NIL"] ++ n_times 1358 (LENGTH args) (iDATA opCONS)),rs,bc)` 1359 \\ STRIP_TAC THEN1 (RES_TAC \\ ASM_SIMP_TAC std_ss []) 1360 \\ FULL_SIMP_TAC std_ss [list2sexp_def] 1361 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 1362 \\ MATCH_MP_TAC iSTEP_cases_imp 1363 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1364 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def] 1365 \\ FULL_SIMP_TAC std_ss [EVAL_DATA_OP_def,iLENGTH_def,iLENGTH_APPEND, 1366 AC ADD_COMM ADD_ASSOC] \\ Q.EXISTS_TAC `[h;list2sexp args]` 1367 \\ FULL_SIMP_TAC std_ss [LISP_CONS_def,EL,HD,TL] \\ EVAL_TAC); 1368 1369val BC_PRINT_code = prove( 1370 ``((BC_PRINT bc z).code = bc.code) /\ 1371 ((BC_PRINT bc z).instr_length = bc.instr_length) /\ 1372 ((BC_FAIL bc).code = bc.code) /\ 1373 ((BC_FAIL bc).instr_length = bc.instr_length)``, 1374 SRW_TAC [] [BC_PRINT_def,BC_FAIL_def]); 1375 1376val BC_SUBSTATE_TAC = 1377 FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE 1378 \\ IMP_RES_TAC BC_ev_LENGTH \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 1379 \\ IMP_RES_TAC BC_SUBSTATE_TRANS \\ FULL_SIMP_TAC std_ss [] 1380 1381val EXISTS_LEMMA = METIS_PROVE [] 1382 ``(?y. (?x. P1 x /\ P2 x y) /\ Q y) = ?x. P1 x /\ ?y. P2 x y /\ Q y`` 1383 1384val WRITE_BYTECODE_SKIP = store_thm("WRITE_BYTECODE_SKIP", 1385 ``!new_code bc n i. 1386 n + iLENGTH bc.instr_length new_code <= i /\ (!h. 0 < bc.instr_length h) ==> 1387 ((WRITE_BYTECODE bc n new_code).code i = bc.code i)``, 1388 Induct \\ SIMP_TAC std_ss [WRITE_BYTECODE_def,iLENGTH_def,ADD_ASSOC] 1389 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!bc n.bbb` 1390 (MP_TAC o Q.SPEC `(bc with code := (n =+ SOME h) bc.code)`) 1391 \\ FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC \\ RES_TAC 1392 \\ FULL_SIMP_TAC std_ss [combinTheory.APPLY_UPDATE_THM] 1393 \\ `0 < bc.instr_length h` by FULL_SIMP_TAC std_ss [] 1394 \\ `~(n = i)` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss []); 1395 1396val BC_CODE_OK_BC_ONLY_COMPILE = store_thm("BC_CODE_OK_BC_ONLY_COMPILE", 1397 ``BC_CODE_OK bc ==> BC_CODE_OK (BC_ONLY_COMPILE (params,body,bc))``, 1398 SIMP_TAC std_ss [BC_ONLY_COMPILE_def,LET_DEF] 1399 \\ `?new_code a2 q2 bcB. BC_ev_fun (params,body,bc) = (new_code,a2,q2,bcB)` by METIS_TAC [PAIR] 1400 \\ ASM_SIMP_TAC std_ss [NOT_CONS_NIL] 1401 \\ STRIP_TAC 1402 \\ `BC_JUMPS_OK bc` by FULL_SIMP_TAC std_ss [BC_CODE_OK_def,BC_JUMPS_OK_def] 1403 \\ IMP_RES_TAC BC_ev_fun_CONSTS \\ FULL_SIMP_TAC std_ss [] 1404 \\ FULL_SIMP_TAC (srw_ss()) [BC_CODE_OK_def,WRITE_BYTECODE_code_end] 1405 \\ FULL_SIMP_TAC std_ss [] 1406 \\ REPEAT STRIP_TAC 1407 \\ `!h. 0 < bcB.instr_length h` by METIS_TAC [] 1408 \\ IMP_RES_TAC WRITE_BYTECODE_SKIP 1409 \\ ASM_SIMP_TAC std_ss [] 1410 \\ Q.PAT_X_ASSUM `bc.code = bcB.code` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 1411 \\ Q.PAT_X_ASSUM `!i. bcB.code_end <= i ==> (bc.code i = NONE)` MATCH_MP_TAC 1412 \\ DECIDE_TAC); 1413 1414val BC_CODE_OK_BC_COMPILE = prove( 1415 ``BC_CODE_OK bc ==> BC_CODE_OK (BC_COMPILE (fname,params,body,bc))``, 1416 REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [BC_COMPILE_def,LET_DEF] 1417 \\ MATCH_MP_TAC BC_CODE_OK_BC_ONLY_COMPILE 1418 \\ POP_ASSUM MP_TAC \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []); 1419 1420val BC_ONLY_COMPILE_compiled_instr_length = prove( 1421 ``BC_CODE_OK bc ==> 1422 ((BC_ONLY_COMPILE (syms,body,bc)).compiled = bc.compiled) /\ 1423 ((BC_ONLY_COMPILE (syms,body,bc)).instr_length = bc.instr_length) /\ 1424 ((BC_ONLY_COMPILE (syms,body,bc)).io_out = bc.io_out) /\ 1425 ((BC_ONLY_COMPILE (syms,body,bc)).ok = bc.ok)``, 1426 STRIP_TAC \\ SIMP_TAC std_ss [BC_ONLY_COMPILE_def] 1427 \\ FULL_SIMP_TAC std_ss [LET_DEF] 1428 \\ `BC_JUMPS_OK bc` by 1429 (POP_ASSUM MP_TAC \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1430 \\ `?new_code a2 q2 bcB. BC_ev_fun (syms,body,bc) = (new_code,a2,q2,bcB)` by METIS_TAC [PAIR] 1431 \\ IMP_RES_TAC BC_ev_fun_CONSTS 1432 \\ FULL_SIMP_TAC (srw_ss()) [WRITE_BYTECODE_code_end]); 1433 1434val BC_COMPILE_compiled_instr_length = prove( 1435 ``BC_CODE_OK bc ==> 1436 ((BC_COMPILE (fc,syms,body,bc)).compiled = 1437 (BC_STORE_COMPILED bc fc (bc.code_end,LENGTH syms)).compiled) /\ 1438 ((BC_COMPILE (fc,syms,body,bc)).instr_length = bc.instr_length) /\ 1439 ((BC_COMPILE (fc,syms,body,bc)).io_out = bc.io_out) /\ 1440 ((BC_COMPILE (fc,syms,body,bc)).ok = bc.ok)``, 1441 STRIP_TAC \\ FULL_SIMP_TAC std_ss [BC_COMPILE_def,LET_DEF] 1442 \\ `BC_CODE_OK (BC_STORE_COMPILED bc fc (bc.code_end,LENGTH syms))` by 1443 (POP_ASSUM MP_TAC \\ EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 1444 \\ FULL_SIMP_TAC std_ss [BC_ONLY_COMPILE_compiled_instr_length] \\ EVAL_TAC); 1445 1446val WRITE_BYTECODE_SKIP_LESS = store_thm("WRITE_BYTECODE_SKIP_LESS", 1447 ``!new_code bc n i. 1448 i < n ==> ((WRITE_BYTECODE bc n new_code).code i = bc.code i)``, 1449 Induct \\ SIMP_TAC std_ss [WRITE_BYTECODE_def,iLENGTH_def,ADD_ASSOC] 1450 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!bc n.bbb` 1451 (MP_TAC o Q.SPEC `(bc with code := (n =+ SOME h) bc.code)`) 1452 \\ `i < (n + bc.instr_length h)` by DECIDE_TAC 1453 \\ FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC \\ RES_TAC 1454 \\ FULL_SIMP_TAC std_ss [combinTheory.APPLY_UPDATE_THM] 1455 \\ `~(n = i)` by DECIDE_TAC \\ FULL_SIMP_TAC std_ss []); 1456 1457val CONTAINS_BYTECODE_WRITE_BYTECODE = store_thm("CONTAINS_BYTECODE_WRITE_BYTECODE", 1458 ``!xs bc a. 1459 (!h. 0 < bc.instr_length h) ==> 1460 CONTAINS_BYTECODE (WRITE_BYTECODE bc a xs) a xs``, 1461 Induct \\ ASM_SIMP_TAC std_ss [CONTAINS_BYTECODE_def,WRITE_BYTECODE_code_end, 1462 WRITE_BYTECODE_def] \\ REVERSE (REPEAT STRIP_TAC) \\ FULL_SIMP_TAC std_ss [] 1463 \\ Q.PAT_X_ASSUM `!bc a. bbb` 1464 (MP_TAC o Q.SPEC `(bc with code := (a =+ SOME h) bc.code)`) 1465 \\ FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 1466 \\ `0 < bc.instr_length h` by FULL_SIMP_TAC std_ss [] 1467 \\ `a < a + bc.instr_length h` by DECIDE_TAC 1468 \\ IMP_RES_TAC WRITE_BYTECODE_SKIP_LESS \\ FULL_SIMP_TAC std_ss [] 1469 \\ FULL_SIMP_TAC (srw_ss()) [combinTheory.APPLY_UPDATE_THM]); 1470 1471val CONTAINS_BYTECODE_code_end = prove( 1472 ``!xs a bc. CONTAINS_BYTECODE (bc with code_end := x) a xs = CONTAINS_BYTECODE bc a xs``, 1473 Induct \\ ASM_SIMP_TAC (srw_ss()) [CONTAINS_BYTECODE_def]); 1474 1475val BC_REFINES_ONLY_COMPILE = store_thm("BC_REFINES_ONLY_COMPILE", 1476 ``BC_REFINES (fns,io) bc7 ==> 1477 BC_REFINES (fns,io) (BC_ONLY_COMPILE (syms,body,bc7))``, 1478 SIMP_TAC std_ss [BC_REFINES_def] \\ REVERSE (REPEAT STRIP_TAC) 1479 \\ FULL_SIMP_TAC std_ss [BC_ONLY_COMPILE_io_out,BC_CODE_OK_BC_ONLY_COMPILE] 1480 \\ IMP_RES_TAC BC_CODE_OK_BC_ONLY_COMPILE 1481 \\ IMP_RES_TAC BC_ONLY_COMPILE_compiled_instr_length 1482 THEN1 (FULL_SIMP_TAC std_ss [BC_CODE_OK_def]) 1483 \\ FULL_SIMP_TAC std_ss [] 1484 \\ FULL_SIMP_TAC std_ss [BC_FNS_ASSUM_def,FAPPLY_FUPDATE_THM,FDOM_FUPDATE,IN_INSERT] 1485 \\ REPEAT STRIP_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 1486 \\ Q.LIST_EXISTS_TAC [`pcode`,`a5`,`bc4`,`bc5`] \\ ASM_SIMP_TAC std_ss [] 1487 \\ REVERSE STRIP_TAC THEN1 (METIS_TAC [BC_SUBSTATE_ONLY_COMPILE,BC_SUBSTATE_TRANS]) 1488 \\ `?new_code a2 q2 bcB. BC_ev_fun (syms,body,bc7) = (new_code,a2,q2,bcB)` by METIS_TAC [PAIR] 1489 \\ ASM_SIMP_TAC std_ss [BC_ONLY_COMPILE_def,LET_DEF,WRITE_BYTECODE_code_end] 1490 \\ MATCH_MP_TAC (GEN_ALL BC_SUBSTATE_BYTECODE_OK) \\ Q.EXISTS_TAC `bc7` 1491 \\ ASM_SIMP_TAC std_ss [] 1492 \\ `BC_SUBSTATE bc7 (BC_ONLY_COMPILE (syms,body,bc7))` by 1493 ASM_SIMP_TAC std_ss [BC_SUBSTATE_ONLY_COMPILE] 1494 \\ POP_ASSUM MP_TAC 1495 \\ FULL_SIMP_TAC std_ss [BC_ONLY_COMPILE_def,LET_DEF,WRITE_BYTECODE_code_end]); 1496 1497val BC_REFINES_COMPILE = store_thm("BC_REFINES_COMPILE", 1498 ``fc NOTIN FDOM fns /\ BC_REFINES (fns,io) bc7 ==> 1499 BC_REFINES (fns |+ (fc,syms,body),io) (BC_COMPILE (fc,syms,body,bc7))``, 1500 SIMP_TAC std_ss [BC_REFINES_def] \\ REVERSE (REPEAT STRIP_TAC) 1501 \\ FULL_SIMP_TAC std_ss [BC_COMPILE_io_out,BC_CODE_OK_BC_COMPILE] 1502 \\ IMP_RES_TAC BC_CODE_OK_BC_COMPILE 1503 \\ IMP_RES_TAC BC_COMPILE_compiled_instr_length 1504 THEN1 (FULL_SIMP_TAC std_ss [BC_CODE_OK_def]) 1505 \\ FULL_SIMP_TAC std_ss [] THEN1 1506 (FULL_SIMP_TAC std_ss [FUN_LOOKUP_def,FDOM_FUPDATE] 1507 \\ FULL_SIMP_TAC (srw_ss()) [BC_STORE_COMPILED_def,FUN_LOOKUP_def,LET_DEF] 1508 \\ FULL_SIMP_TAC std_ss [EXTENSION,GSPECIFICATION,IN_INSERT] 1509 \\ STRIP_TAC \\ Cases_on `fc = x` \\ FULL_SIMP_TAC std_ss []) 1510 \\ FULL_SIMP_TAC std_ss [BC_FNS_ASSUM_def,FAPPLY_FUPDATE_THM,FDOM_FUPDATE, 1511 IN_INSERT] 1512 \\ STRIP_TAC \\ REVERSE (Cases_on `fc' = fc`) \\ FULL_SIMP_TAC std_ss [] 1513 \\ FULL_SIMP_TAC (srw_ss()) [BC_STORE_COMPILED_def,FUN_LOOKUP_def] 1514 \\ REPEAT STRIP_TAC \\ RES_TAC \\ FULL_SIMP_TAC std_ss [] 1515 \\ `BC_CODE_OK bc7` by METIS_TAC [BC_CODE_OK_def] 1516 \\ `BC_SUBSTATE bc7 (BC_COMPILE (fc,syms,body,bc7))` by 1517 (MATCH_MP_TAC (SIMP_RULE std_ss [] BC_COMPILE_SUBSTATE) 1518 \\ Q.PAT_X_ASSUM `zzz = FDOM fns` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 1519 \\ FULL_SIMP_TAC std_ss [GSPECIFICATION]) 1520 THEN1 (METIS_TAC [BC_SUBSTATE_TRANS,BC_SUBSTATE_BYTECODE_OK]) 1521 \\ `BC_CODE_OK (BC_COMPILE (fc,syms,body,bc7))` by METIS_TAC [BC_CODE_OK_BC_COMPILE] 1522 \\ POP_ASSUM MP_TAC \\ POP_ASSUM MP_TAC 1523 \\ SIMP_TAC std_ss [BC_COMPILE_thm] 1524 \\ Q.PAT_ABBREV_TAC `bcA = BC_STORE_COMPILED bc fc zzz` 1525 \\ FULL_SIMP_TAC std_ss [LET_DEF] 1526 \\ `?new_code a2 q2 bcB. BC_ev_fun (syms,body,bcA) = (new_code,a2,q2,bcB)` by METIS_TAC [PAIR] 1527 \\ ASM_SIMP_TAC (srw_ss()) [NOT_CONS_NIL,WRITE_BYTECODE_code_end] 1528 \\ REPEAT STRIP_TAC \\ `BC_JUMPS_OK bcA` by 1529 (Q.UNABBREV_TAC `bcA` 1530 \\ FULL_SIMP_TAC (srw_ss()) [BC_JUMPS_OK_def,BC_STORE_COMPILED_def,BC_CODE_OK_def]) 1531 \\ IMP_RES_TAC BC_ev_fun_IMP 1532 \\ Q.LIST_EXISTS_TAC [`new_code`,`a2`,`bcA`,`bcB`] 1533 \\ IMP_RES_TAC BC_ev_LENGTH \\ FULL_SIMP_TAC std_ss [] 1534 \\ `(bc7.code_end = bcA.code_end) /\ (bc7.instr_length = bcA.instr_length)` by 1535 (Q.UNABBREV_TAC `bcA` \\ FULL_SIMP_TAC (srw_ss()) [BC_STORE_COMPILED_def]) 1536 \\ IMP_RES_TAC BC_ev_CONSTS \\ FULL_SIMP_TAC std_ss [] 1537 \\ REPEAT STRIP_TAC THEN1 1538 (SIMP_TAC std_ss [CONTAINS_BYTECODE_code_end] 1539 \\ MATCH_MP_TAC CONTAINS_BYTECODE_WRITE_BYTECODE 1540 \\ FULL_SIMP_TAC std_ss [BC_CODE_OK_def]) 1541 \\ SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,WRITE_BYTECODE_code_end] 1542 \\ Cases_on `BC_CODE_OK bcB` \\ FULL_SIMP_TAC std_ss [] 1543 \\ METIS_TAC [BC_CODE_OK_def,NOT_LESS,WRITE_BYTECODE_SKIP_LESS]); 1544 1545val BC_CODE_OK_PRINT = prove( 1546 ``BC_CODE_OK (BC_PRINT bc str) = BC_CODE_OK bc``, 1547 SIMP_TAC (srw_ss()) [BC_PRINT_def,BC_CODE_OK_def]); 1548 1549val BC_CODE_OK_FAIL = prove( 1550 ``BC_CODE_OK (BC_FAIL bc) = BC_CODE_OK bc``, 1551 SIMP_TAC (srw_ss()) [BC_FAIL_def,BC_CODE_OK_def]); 1552 1553val lemma = BC_ev_ind 1554 |> Q.SPEC `\ret x y. 1555 let (fc,n,a1,q1,bc1) = x in 1556 let (code,a2,p2,bc0) = y in 1557 (~ret ==> (a2 = ssTEMP::DROP n a1))` 1558 |> Q.SPEC `\x y. 1559 let (xs,a1,q1,bc1) = x in 1560 let (code,a2,p2,bc0) = y in 1561 (a2 = MAP (\x.ssTEMP) xs ++ a1)` 1562 |> Q.SPEC `\ret x y. 1563 let (xs,a1,q1,bc1) = x in 1564 let (code,a2,p2,bc0) = y in 1565 (~ret ==> (a2 = ssTEMP :: a1))` 1566 1567val drop_map = 1568 RW [LENGTH_MAP] (Q.SPEC `MAP f xs` rich_listTheory.BUTFIRSTN_LENGTH_APPEND) 1569 1570val BC_ev_lemma_ret = prove(lemma |> concl |> rand, 1571 MATCH_MP_TAC lemma \\ SIMP_TAC std_ss [LET_DEF] \\ REPEAT STRIP_TAC 1572 \\ TRY (Cases_on `ret`) \\ SIMP_TAC std_ss [BC_return_def,drop_map,MAP,APPEND] 1573 \\ Induct_on `xs` \\ ASM_SIMP_TAC std_ss [MAP,APPEND,CONS_11]) 1574 1575val BC_ev_NOT_RET_LEMMA = prove( 1576 ``BC_ev ret (exp,a,p,bc) (code,a2,p2,bc0) ==> 1577 (~ret ==> (a2 = ssTEMP::a))``, 1578 REPEAT STRIP_TAC \\ IMP_RES_TAC BC_ev_lemma_ret 1579 \\ FULL_SIMP_TAC std_ss [LET_DEF]); 1580 1581val add_def_NOP = prove( 1582 ``!x y fns. x IN FDOM fns ==> (add_def fns (x,y) = fns)``, 1583 SIMP_TAC std_ss [add_def_def,FUNION_DEF,fmap_EXT] 1584 \\ SRW_TAC [] [EXTENSION] \\ METIS_TAC []); 1585 1586val add_def_FUPDATE = prove( 1587 ``!x y fns. ~(x IN FDOM fns) ==> (add_def fns (x,y) = fns |+ (x,y))``, 1588 SIMP_TAC std_ss [add_def_def,FUNION_DEF,fmap_EXT,FAPPLY_FUPDATE_THM] 1589 \\ SRW_TAC [] [EXTENSION] \\ METIS_TAC []); 1590 1591val lemma = RR_ev_ind 1592 |> Q.SPEC `\fc_args_env_fns_io_ok result_fns8_io8_ok8. 1593 !fc args a code a2 env stack p r rs fns fns8 io io8 ret p2 bc bc0 bc7 result ok ok8. 1594 (fc_args_env_fns_io_ok = (fc,args,env,fns,io,ok)) /\ 1595 (result_fns8_io8_ok8 = (result,fns8,io8,ok8)) /\ 1596 BC_REFINES (fns,io) bc7 /\ BC_SUBSTATE bc0 bc7 /\ 1597 BC_ap ret (fc,LENGTH args,MAP (\x.ssTEMP) args ++ a,p,bc) (code,a2,p2,bc0) /\ 1598 CONTAINS_BYTECODE bc7 p code /\ 1599 STACK_INV env stack a /\ (bc7.ok = ok) ==> 1600 ?bc8. 1601 RTC iSTEP (REVERSE args ++ stack,p,r::rs,bc7) 1602 (if ret then iSTEP_ret_state a (result,stack,r,rs,bc8) 1603 else (result::stack,p+iLENGTH bc.instr_length code,r::rs,bc8)) /\ 1604 BC_REFINES (fns8,io8) bc8 /\ (bc8.ok = ok8) /\ 1605 (~ret ==> (a2 = ssTEMP::a)) /\ fns SUBMAP fns8` 1606 |> Q.SPEC `\cs_env_fns_io_ok result_fns8_io8_ok8. 1607 !cs a code a2 env stack p ns r rs fns fns8 io io8 p2 bc bc0 bc7 result ok ok8. 1608 (cs_env_fns_io_ok = (cs,env,fns,io,ok)) /\ 1609 (result_fns8_io8_ok8 = (result,fns8,io8,ok8)) /\ 1610 BC_REFINES (fns,io) bc7 /\ BC_SUBSTATE bc0 bc7 /\ 1611 BC_evl (cs,a,p,bc) (code,a2,p2,bc0) /\ 1612 CONTAINS_BYTECODE bc7 p code /\ 1613 STACK_INV env stack a /\ (bc7.ok = ok) ==> 1614 ?bc8. 1615 RTC iSTEP (stack,p,r::rs,bc7) (REVERSE result++stack,p+iLENGTH bc.instr_length code,r::rs,bc8) /\ 1616 BC_REFINES (fns8,io8) bc8 /\ (bc8.ok = ok8) /\ 1617 (a2 = MAP (\x.ssTEMP) (REVERSE result) ++ a) /\ 1618 (LENGTH result = LENGTH cs) /\ fns SUBMAP fns8` 1619 |> Q.SPEC `\c_env_fns_io_ok result_fns8_io8_ok8. 1620 !c a code a2 env stack p r rs fns fns8 io io8 ret p2 bc bc0 bc7 result ok ok8. 1621 (c_env_fns_io_ok = (c,env,fns,io,ok)) /\ 1622 (result_fns8_io8_ok8 = (result,fns8,io8,ok8)) /\ 1623 BC_REFINES (fns,io) bc7 /\ BC_SUBSTATE bc0 bc7 /\ 1624 BC_ev ret (c,a,p,bc) (code,a2,p2,bc0) /\ 1625 CONTAINS_BYTECODE bc7 p code /\ 1626 STACK_INV env stack a /\ (bc7.ok = ok) ==> 1627 ?bc8. 1628 RTC iSTEP (stack,p,r::rs,bc7) 1629 (if ret then iSTEP_ret_state a (result,stack,r,rs,bc8) 1630 else (result::stack,p+iLENGTH bc.instr_length code,r::rs,bc8)) /\ 1631 BC_REFINES (fns8,io8) bc8 /\ (bc8.ok = ok8) /\ 1632 (~ret ==> (a2 = ssTEMP::a)) /\ fns SUBMAP fns8` 1633 1634val goal = lemma |> concl |> rand 1635 1636(* 1637 set_goal([],goal) 1638*) 1639 1640val BC_ev_lemma = prove(goal, 1641 1642 MATCH_MP_TAC lemma \\ SIMP_TAC std_ss [] 1643 \\ STRIP_TAC THEN1 (* constant *) 1644 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 1645 \\ SIMP_TAC std_ss [term_distinct,term_11,CONTAINS_BYTECODE_def, 1646 CONTAINS_BYTECODE_APPEND,SUBMAP_REFL] 1647 \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [BC_return_code_def,APPEND_NIL,LENGTH] 1648 \\ SIMP_TAC std_ss [LENGTH_APPEND,LENGTH,ADD_ASSOC] 1649 \\ Q.EXISTS_TAC `bc7` \\ ASM_SIMP_TAC std_ss [] 1650 \\ Q.ABBREV_TAC `bc_insts = 1651 (if isVal s then 1652 [iCONST_NUM (getVal s)] 1653 else if isSym s then 1654 [iCONST_SYM (getSym s)] 1655 else 1656 [iCONST_NUM (LENGTH bc.consts); iCONST_LOOKUP])` 1657 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1658 \\ Q.EXISTS_TAC `(s::stack,p + iLENGTH bc.instr_length bc_insts,r::rs,bc7)` 1659 \\ REVERSE STRIP_TAC THEN1 1660 (REVERSE (Cases_on `ret`) 1661 \\ FULL_SIMP_TAC std_ss [RTC_REFL,iLENGTH_def,BC_return_code_def,APPEND_NIL] 1662 \\ MATCH_MP_TAC BC_return_code_thm \\ ASM_SIMP_TAC std_ss [BC_return_code_def] 1663 \\ `bc.instr_length = bc7.instr_length` by (Cases_on `isDot s` 1664 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,BC_ADD_CONST_def]) 1665 \\ METIS_TAC [BC_return_code_thm]) 1666 \\ Q.UNABBREV_TAC `bc_insts` 1667 \\ Cases_on `isVal s` \\ FULL_SIMP_TAC std_ss [iLENGTH_def] THEN1 1668 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 1669 \\ MATCH_MP_TAC iSTEP_cases_imp 1670 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1671 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def] 1672 \\ Cases_on `s` \\ FULL_SIMP_TAC (srw_ss()) [getVal_def,isVal_def] 1673 \\ FULL_SIMP_TAC std_ss [isDot_def,BC_SUBSTATE_def]) 1674 \\ Cases_on `isSym s` \\ FULL_SIMP_TAC std_ss [iLENGTH_def] THEN1 1675 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 1676 \\ MATCH_MP_TAC iSTEP_cases_imp 1677 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1678 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def] 1679 \\ Cases_on `s` \\ FULL_SIMP_TAC (srw_ss()) [getSym_def,isSym_def] 1680 \\ FULL_SIMP_TAC std_ss [isDot_def,BC_SUBSTATE_def]) 1681 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1682 \\ Q.EXISTS_TAC `(Val (LENGTH bc.consts)::stack,p + bc7.instr_length (iCONST_NUM (LENGTH bc.consts)),r::rs,bc7)` 1683 \\ STRIP_TAC THEN1 1684 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 1685 \\ MATCH_MP_TAC iSTEP_cases_imp 1686 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1687 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def]) 1688 THEN1 1689 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 1690 \\ MATCH_MP_TAC iSTEP_cases_imp 1691 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1692 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def] 1693 \\ `isDot s` by (Cases_on `s` \\ FULL_SIMP_TAC (srw_ss()) [isVal_def,isSym_def,isDot_def]) 1694 \\ FULL_SIMP_TAC std_ss [BC_SUBSTATE_def,GSYM APPEND_ASSOC,BC_ADD_CONST_def] 1695 \\ SIMP_TAC (srw_ss()) [] 1696 \\ FULL_SIMP_TAC std_ss [BC_SUBSTATE_def,GSYM APPEND_ASSOC,BC_ADD_CONST_def] 1697 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH,rich_listTheory.EL_APPEND2,EL,HD] 1698 \\ FULL_SIMP_TAC std_ss [APPEND,HD] \\ DECIDE_TAC)) 1699 \\ STRIP_TAC THEN1 (* var lookup *) 1700 (ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 1701 \\ SIMP_TAC std_ss [term_distinct,term_11] 1702 \\ SIMP_TAC std_ss [GSYM AND_IMP_INTRO,PULL_EXISTS_IMP,CONTAINS_BYTECODE_def, 1703 CONTAINS_BYTECODE_APPEND,SUBMAP_REFL] 1704 \\ REPEAT STRIP_TAC \\ SIMP_TAC std_ss [BC_return_code_def,APPEND_NIL,LENGTH] 1705 \\ `VARS_IN_STACK a stack a'` by METIS_TAC [STACK_INV_def] 1706 \\ FULL_SIMP_TAC std_ss [VARS_IN_STACK_def] \\ RES_TAC 1707 \\ Q.EXISTS_TAC `bc7` \\ ASM_SIMP_TAC std_ss [] 1708 \\ SIMP_TAC std_ss [LENGTH_APPEND,LENGTH,ADD_ASSOC] 1709 \\ FULL_SIMP_TAC std_ss [] 1710 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1711 \\ Q.EXISTS_TAC `(a ' x::stack,p + bc.instr_length (iLOAD n),r::rs,bc7)` \\ STRIP_TAC THEN1 1712 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 1713 \\ MATCH_MP_TAC iSTEP_cases_imp 1714 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1715 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def] 1716 \\ FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 1717 \\ METIS_TAC [STACK_INV_def,SOME_11,VARS_IN_STACK_def]) 1718 \\ REVERSE (Cases_on `ret`) \\ FULL_SIMP_TAC std_ss [RTC_REFL,iLENGTH_def] 1719 \\ METIS_TAC [BC_return_code_thm,BC_SUBSTATE_def]) 1720 \\ STRIP_TAC THEN1 1721 (REPEAT STRIP_TAC (* Or [] *) 1722 \\ Q.PAT_X_ASSUM `BC_ev ret xxx yyy` MP_TAC 1723 \\ ONCE_REWRITE_TAC [BC_ev_cases] 1724 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,NOT_CONS_NIL,CONS_11] 1725 \\ METIS_TAC []) 1726 \\ STRIP_TAC THEN1 1727 (REPEAT STRIP_TAC 1728 \\ Q.PAT_X_ASSUM `BC_ev xxx (Or e1,pppp) qqq` MP_TAC 1729 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 1730 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH,NOT_CONS_NIL,CONS_11] 1731 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1732 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 1733 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL,NOT_CONS_NIL,CONS_11] 1734 \\ Q.PAT_X_ASSUM `!env.bbb` (MP_TAC o 1735 Q.SPECL [`a'`,`x_code`,`a1`,`stack`,`p`,`r`,`rs`,`F`,`q1`,`bc`,`bc1`,`bc7`]) 1736 \\ ASM_SIMP_TAC std_ss [] \\ MATCH_MP_TAC IMP_IMP 1737 \\ STRIP_TAC THEN1 (METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_TRANS]) 1738 \\ REPEAT STRIP_TAC 1739 \\ Q.ABBREV_TAC `jump = iJUMP p2` 1740 \\ Q.ABBREV_TAC `jnil = iJNIL (p+addr)` 1741 \\ Q.EXISTS_TAC `bc8` \\ ASM_SIMP_TAC std_ss [] 1742 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1743 \\ Q.EXISTS_TAC `(s1::stack,p + iLENGTH bc.instr_length x_code,r::rs,bc8)` 1744 \\ ASM_SIMP_TAC std_ss [] 1745 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1746 \\ Q.EXISTS_TAC `(s1::s1::stack,p + iLENGTH bc.instr_length (x_code ++ [iLOAD 0]),r::rs,bc8)` 1747 \\ STRIP_TAC THEN1 1748 (MATCH_MP_TAC RTC_SINGLE 1749 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1750 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1751 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1752 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1753 \\ MATCH_MP_TAC iSTEP_cases_imp 1754 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1755 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def,isTrue_def] 1756 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND,EL,HD,ADD_ASSOC]) 1757 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1758 \\ Q.EXISTS_TAC `(s1::stack,p + iLENGTH bc.instr_length (x_code ++ [iLOAD 0; jnil]),r::rs,bc8)` 1759 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC THEN1 1760 (MATCH_MP_TAC RTC_SINGLE 1761 \\ Q.UNABBREV_TAC `jnil` 1762 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND,AC ADD_ASSOC ADD_COMM] 1763 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1764 \\ `BC_SUBSTATE bc7 bc8` by 1765 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1766 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1767 \\ FULL_SIMP_TAC std_ss []) 1768 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1769 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1770 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1771 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_def,AC ADD_COMM ADD_ASSOC] 1772 \\ MATCH_MP_TAC iSTEP_cases_imp 1773 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1774 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def,isTrue_def] 1775 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM]) 1776 \\ REVERSE (Cases_on `ret`) \\ FULL_SIMP_TAC std_ss [BC_return_code_def,APPEND] THEN1 1777 (Q.UNABBREV_TAC `jump` 1778 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND,AC ADD_ASSOC ADD_COMM] 1779 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1780 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1781 \\ MATCH_MP_TAC RTC_SINGLE 1782 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1783 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1784 \\ MATCH_MP_TAC iSTEP_cases_imp 1785 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1786 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def,isTrue_def] 1787 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND,EL,HD,ADD_ASSOC] 1788 \\ Q.PAT_X_ASSUM `p2 = xxx` (fn th => SIMP_TAC std_ss [Once th]) 1789 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM]) 1790 \\ MATCH_MP_TAC BC_return_code_thm \\ ASM_SIMP_TAC std_ss [] 1791 \\ FULL_SIMP_TAC std_ss [BC_return_code_def,LENGTH,ADD1] 1792 \\ `BC_SUBSTATE bc7 bc8` by METIS_TAC [iSTEP_BC_SUBSTATE] 1793 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1794 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1795 \\ FULL_SIMP_TAC std_ss []) 1796 \\ STRIP_TAC THEN1 1797 (REPEAT STRIP_TAC 1798 \\ Q.PAT_X_ASSUM `BC_ev xxx (Or e1,pppp) qqq` MP_TAC 1799 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 1800 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH,NOT_CONS_NIL,CONS_11] 1801 \\ REPEAT STRIP_TAC \\ ASM_SIMP_TAC std_ss [] 1802 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 1803 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL,NOT_CONS_NIL,CONS_11] 1804 \\ Q.PAT_X_ASSUM `!env.bbb` MP_TAC 1805 \\ Q.PAT_X_ASSUM `!env.bbb` (MP_TAC o 1806 Q.SPECL [`a'`,`x_code`,`a1`,`stack`,`p`,`r`,`rs`,`F`,`q1`,`bc`,`bc1`,`bc7`]) 1807 \\ ASM_SIMP_TAC std_ss [] \\ MATCH_MP_TAC IMP_IMP 1808 \\ STRIP_TAC THEN1 (METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_TRANS]) 1809 \\ REPEAT STRIP_TAC 1810 \\ Q.ABBREV_TAC `jump = iJUMP p2` 1811 \\ Q.ABBREV_TAC `jnil = iJNIL (p+addr)` 1812 \\ Q.PAT_X_ASSUM `!env.bbb` (MP_TAC o 1813 Q.SPECL [`a'`,`z_code`,`a3`,`stack`,`p + addr + bc.instr_length iPOP`,`r`,`rs`,`ret`,`p2`,`bc1`,`bc0`,`bc8`]) 1814 \\ ASM_SIMP_TAC std_ss [] \\ MATCH_MP_TAC IMP_IMP 1815 \\ STRIP_TAC THEN1 1816 (IMP_RES_TAC BC_ev_LENGTH 1817 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM] 1818 \\ IMP_RES_TAC iSTEP_BC_SUBSTATE 1819 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ ASM_SIMP_TAC std_ss [] 1820 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_SUBSTATE_def,BC_SUBSTATE_TRANS] 1821 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM] 1822 \\ METIS_TAC [BC_SUBSTATE_TRANS,BC_SUBSTATE_BYTECODE]) 1823 \\ REPEAT STRIP_TAC 1824 \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [] 1825 \\ `fns SUBMAP fns2` by METIS_TAC [SUBMAP_TRANS] \\ ASM_SIMP_TAC std_ss [] 1826 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1827 \\ Q.EXISTS_TAC `(s1::stack,p + iLENGTH bc.instr_length x_code,r::rs,bc8)` 1828 \\ ASM_SIMP_TAC std_ss [] 1829 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1830 \\ Q.EXISTS_TAC `(stack,p + addr + bc.instr_length iPOP,r::rs,bc8)` 1831 \\ ASM_SIMP_TAC std_ss [] \\ REVERSE STRIP_TAC THEN1 1832 (`bc1.instr_length = bc.instr_length` by METIS_TAC [BC_SUBSTATE_def,BC_ev_LENGTH] 1833 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM] 1834 \\ Q.PAT_X_ASSUM `RTC iSTEP xxx yyy` MP_TAC 1835 \\ ASM_SIMP_TAC std_ss [ADD_ASSOC]) 1836 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1837 \\ Q.EXISTS_TAC `(s1::s1::stack,p + iLENGTH bc.instr_length (x_code ++ [iLOAD 0]),r::rs,bc8)` 1838 \\ STRIP_TAC THEN1 1839 (MATCH_MP_TAC RTC_SINGLE 1840 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1841 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1842 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1843 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1844 \\ MATCH_MP_TAC iSTEP_cases_imp 1845 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1846 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def,isTrue_def] 1847 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND,EL,HD,ADD_ASSOC]) 1848 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1849 \\ Q.EXISTS_TAC `(s1::stack,p + addr,r::rs,bc8)` 1850 \\ REVERSE STRIP_TAC THEN1 1851 (MATCH_MP_TAC RTC_SINGLE 1852 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1853 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1854 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1855 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1856 \\ MATCH_MP_TAC iSTEP_cases_imp 1857 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1858 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def,isTrue_def] 1859 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND,EL,HD,ADD_ASSOC]) 1860 \\ MATCH_MP_TAC RTC_SINGLE 1861 \\ Q.UNABBREV_TAC `jnil` 1862 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,iLENGTH_APPEND,AC ADD_ASSOC ADD_COMM] 1863 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1864 \\ `BC_SUBSTATE bc7 bc8` by 1865 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1866 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1867 \\ FULL_SIMP_TAC std_ss []) 1868 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1869 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1870 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1871 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_def,AC ADD_COMM ADD_ASSOC] 1872 \\ MATCH_MP_TAC iSTEP_cases_imp 1873 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1874 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def,isTrue_def]) 1875 \\ STRIP_TAC THEN1 1876 (REPEAT STRIP_TAC 1877 \\ Q.PAT_X_ASSUM `BC_ev xxx (If e1 e2 e3,pppp) qqq` MP_TAC 1878 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 1879 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH] 1880 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 1881 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL] 1882 \\ Q.PAT_X_ASSUM `!env. bbb` MP_TAC 1883 \\ Q.PAT_X_ASSUM `!env.bbb` (MP_TAC o 1884 Q.SPECL [`a'`,`x_code`,`a1`,`stack`,`p`,`r`,`rs`,`F`,`q1`,`bc`,`bc1`,`bc7`]) 1885 \\ ASM_SIMP_TAC std_ss [] \\ MATCH_MP_TAC IMP_IMP 1886 \\ STRIP_TAC THEN1 METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_TRANS] 1887 \\ REPEAT STRIP_TAC 1888 \\ Q.ABBREV_TAC `jump = iJUMP p2` 1889 \\ Q.ABBREV_TAC `jnil = iJNIL (q2 + bc.instr_length jump)` 1890 \\ Q.PAT_X_ASSUM `!env.bbb` (MP_TAC o 1891 Q.SPECL [`a'`,`z_code`,`a3`,`stack`,`p + iLENGTH bc.instr_length (x_code ++ [jnil] ++ y_code ++ [jump])`,`r`,`rs`,`ret`,`p2`,`bc2`,`bc0`,`bc8`]) 1892 \\ ASM_SIMP_TAC std_ss [] 1893 \\ `q2 + bc.instr_length jump = p + iLENGTH bc.instr_length (x_code ++ [jnil] ++ y_code ++ [jump])` by 1894 (IMP_RES_TAC BC_ev_LENGTH 1895 \\ SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def] 1896 \\ NTAC 3 (POP_ASSUM MP_TAC) 1897 \\ ASM_SIMP_TAC std_ss [] \\ DECIDE_TAC) 1898 \\ IMP_RES_TAC iSTEP_BC_SUBSTATE 1899 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 1900 (IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1901 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1902 \\ FULL_SIMP_TAC std_ss []) 1903 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1904 \\ REPEAT STRIP_TAC 1905 \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [] 1906 \\ IMP_RES_TAC SUBMAP_TRANS \\ ASM_SIMP_TAC std_ss [] 1907 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1908 \\ Q.EXISTS_TAC `(s1::stack,p + iLENGTH bc.instr_length x_code,r::rs,bc8)` 1909 \\ ASM_SIMP_TAC std_ss [] 1910 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1911 \\ Q.EXISTS_TAC `(stack,p + iLENGTH bc.instr_length (x_code ++ [jnil] ++ y_code ++ [jump]),r::rs,bc8)` 1912 \\ `bc2.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1913 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,ADD_ASSOC] 1914 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 1915 \\ MATCH_MP_TAC RTC_SINGLE 1916 \\ MATCH_MP_TAC iSTEP_cases_imp 1917 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1918 LENGTH,CONS_11,STACK_INV_lemma,getSym_def,CONTAINS_BYTECODE_def,isTrue_def]) 1919 \\ STRIP_TAC THEN1 1920 (REPEAT STRIP_TAC 1921 \\ Q.PAT_X_ASSUM `BC_ev xxx (If e1 e2 e3,pppp) qqq` MP_TAC 1922 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 1923 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH] 1924 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 1925 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL] 1926 \\ Q.PAT_X_ASSUM `!env. bbb` MP_TAC 1927 \\ Q.PAT_X_ASSUM `!env.bbb` (MP_TAC o 1928 Q.SPECL [`a'`,`x_code`,`a1`,`stack`,`p`,`r`,`rs`,`F`,`q1`,`bc`,`bc1`,`bc7`]) 1929 \\ ASM_SIMP_TAC std_ss [] \\ MATCH_MP_TAC IMP_IMP 1930 \\ STRIP_TAC THEN1 METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_TRANS] 1931 \\ REPEAT STRIP_TAC 1932 \\ Q.ABBREV_TAC `jump = iJUMP p2` 1933 \\ Q.ABBREV_TAC `jnil = iJNIL (q2 + bc.instr_length jump)` 1934 \\ Q.PAT_X_ASSUM `!env.bbb` (MP_TAC o 1935 Q.SPECL [`a'`,`y_code`,`a2'`,`stack`,`p + iLENGTH bc.instr_length (x_code ++ [jnil])`,`r`,`rs`,`ret`,`q2`,`bc1`,`bc2`,`bc8`]) 1936 \\ `q1 + bc.instr_length jnil = p + iLENGTH bc.instr_length (x_code ++ [jnil])` by 1937 (IMP_RES_TAC BC_ev_LENGTH 1938 \\ ASM_SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def] \\ DECIDE_TAC) 1939 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 1940 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1941 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1942 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1943 \\ FULL_SIMP_TAC std_ss []) 1944 \\ REPEAT STRIP_TAC 1945 \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [] 1946 \\ IMP_RES_TAC SUBMAP_TRANS \\ ASM_SIMP_TAC std_ss [] 1947 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1948 \\ Q.EXISTS_TAC `(s1::stack,p + iLENGTH bc.instr_length x_code,r::rs,bc8)` 1949 \\ ASM_SIMP_TAC std_ss [] 1950 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1951 \\ FULL_SIMP_TAC std_ss [] 1952 \\ `BC_SUBSTATE bc7 bc8` by 1953 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1954 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1955 \\ FULL_SIMP_TAC std_ss []) 1956 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1957 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1958 \\ Q.EXISTS_TAC `(stack,p + iLENGTH bc.instr_length (x_code ++ [jnil]),r::rs,bc8)` 1959 \\ REPEAT STRIP_TAC THEN1 1960 (MATCH_MP_TAC RTC_SINGLE 1961 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 1962 \\ Q.UNABBREV_TAC `jnil` 1963 \\ MATCH_MP_TAC iSTEP_cases_imp 1964 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,iLENGTH_APPEND,BC_STEP_def, 1965 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,isTrue_def,iLENGTH_def,ADD_ASSOC]) 1966 \\ Cases_on `ret` \\ FULL_SIMP_TAC std_ss [] 1967 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 1968 \\ Q.EXISTS_TAC `(s::stack,p + iLENGTH bc.instr_length (x_code ++ [jnil] ++ y_code),r::rs,bc8')` 1969 \\ `bc1.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1970 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,ADD_ASSOC] 1971 \\ `BC_SUBSTATE bc7 bc8'` by 1972 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1973 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1974 \\ FULL_SIMP_TAC std_ss []) 1975 \\ MATCH_MP_TAC RTC_SINGLE 1976 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 1977 \\ Q.UNABBREV_TAC `jump` 1978 \\ MATCH_MP_TAC iSTEP_cases_imp 1979 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 1980 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,isTrue_def] 1981 \\ IMP_RES_TAC BC_ev_LENGTH 1982 \\ FULL_SIMP_TAC std_ss [iLENGTH_def] 1983 \\ Q.PAT_X_ASSUM `bc1.instr_length = bc.instr_length` MP_TAC 1984 \\ `bc2.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 1985 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] \\ DECIDE_TAC) 1986 \\ STRIP_TAC THEN1 1987 (REPEAT STRIP_TAC 1988 \\ Q.PAT_X_ASSUM `BC_ev zzz (LamApp xs e ys,aaaa) xzzz` MP_TAC 1989 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 1990 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH,NOT_CONS_NIL,CONS_11] 1991 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 1992 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL] 1993 \\ REPEAT STRIP_TAC \\ Q.PAT_X_ASSUM `!env. bbb` MP_TAC 1994 \\ Q.PAT_X_ASSUM `!env. bbb` 1995 (MP_TAC o Q.SPECL [`a'`,`code1`,`a1`,`stack`,`p`,`r`,`rs`,`q1`,`bc`,`bc1`,`bc7`]) 1996 \\ `BC_SUBSTATE bc1 bc7` by 1997 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 1998 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 1999 \\ FULL_SIMP_TAC std_ss []) 2000 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [] 2001 \\ Q.PAT_X_ASSUM `!env. bbb` 2002 (MP_TAC o Q.SPECL [`MAP (ssVAR) (REVERSE xs) ++ a'`, 2003 `code2`,`a2'`,`REVERSE sl ++ stack`,`p + iLENGTH bc.instr_length code1`,`r`,`rs`,`ret`,`q2`,`bc1`,`bc0`,`bc8`]) 2004 \\ `BC_SUBSTATE bc0 bc8` by 2005 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 2006 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 2007 \\ FULL_SIMP_TAC std_ss []) \\ ASM_SIMP_TAC std_ss [] 2008 \\ `BC_SUBSTATE bc7 bc8` by 2009 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 2010 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 2011 \\ FULL_SIMP_TAC std_ss []) \\ ASM_SIMP_TAC std_ss [] 2012 \\ MATCH_MP_TAC IMP_IMP 2013 \\ STRIP_TAC THEN1 2014 (`DROP (LENGTH ys) (MAP (\x. ssTEMP) (REVERSE sl) ++ a') = a'` by 2015 (`LENGTH ys = LENGTH (MAP (\x. ssTEMP) (REVERSE sl))` by ASM_SIMP_TAC std_ss [LENGTH_MAP,LENGTH_REVERSE] 2016 \\ METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND]) 2017 \\ IMP_RES_TAC BC_ev_LENGTH \\ FULL_SIMP_TAC std_ss [] 2018 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ FULL_SIMP_TAC std_ss [] 2019 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2020 \\ FULL_SIMP_TAC std_ss [] 2021 \\ ASM_SIMP_TAC std_ss [] \\ MATCH_MP_TAC STACK_INV_VarBind_2 2022 \\ ASM_SIMP_TAC std_ss [LENGTH_MAP]) 2023 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [] 2024 \\ IMP_RES_TAC SUBMAP_TRANS \\ ASM_SIMP_TAC std_ss [] 2025 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2026 \\ Q.EXISTS_TAC `(REVERSE sl ++ stack,p + iLENGTH bc.instr_length code1,r::rs,bc8)` 2027 \\ ASM_SIMP_TAC std_ss [] 2028 \\ FULL_SIMP_TAC std_ss [LENGTH_MAP,iSTEP_ret_state_APPEND_MAP] 2029 \\ `LENGTH sl = LENGTH xs` by FULL_SIMP_TAC std_ss [] 2030 \\ FULL_SIMP_TAC std_ss [LENGTH_MAP,iSTEP_ret_state_APPEND_MAP] 2031 \\ Cases_on `ret` \\ FULL_SIMP_TAC std_ss [] 2032 \\ REPEAT STRIP_TAC 2033 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2034 \\ Q.EXISTS_TAC `(x::(REVERSE sl ++ stack), 2035 p + iLENGTH bc.instr_length code1 + 2036 iLENGTH bc1.instr_length code2,r::rs,bc8')` 2037 \\ ASM_SIMP_TAC std_ss [] 2038 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_def,iLENGTH_APPEND,ADD_ASSOC] 2039 \\ `BC_SUBSTATE bc7 bc8'` by 2040 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 2041 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 2042 \\ FULL_SIMP_TAC std_ss []) 2043 \\ IMP_RES_TAC BC_SUBSTATE_IMP 2044 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2045 \\ `bc1.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2046 \\ `bc8'.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2047 \\ FULL_SIMP_TAC std_ss [] 2048 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2049 \\ MATCH_MP_TAC iSTEP_cases_imp 2050 \\ ASM_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11, 2051 LENGTH,CONS_11,STACK_INV_lemma,APPEND,BC_STEP_def,CONTAINS_BYTECODE_def] 2052 \\ Q.EXISTS_TAC `REVERSE sl` 2053 \\ ASM_SIMP_TAC std_ss [LENGTH_REVERSE,iLENGTH_def]) 2054 \\ STRIP_TAC THEN1 2055 (REVERSE (REPEAT STRIP_TAC) 2056 \\ Q.PAT_X_ASSUM `BC_ev xxx (App fc el,yyy) ddd` MP_TAC 2057 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2058 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH] 2059 \\ `!f. fc <> Fun f` by FULL_SIMP_TAC std_ss [NOT_isFun] 2060 \\ FULL_SIMP_TAC std_ss [] \\ POP_ASSUM (K ALL_TAC) 2061 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 2062 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL] 2063 \\ Q.PAT_X_ASSUM `!env. bbb` MP_TAC 2064 \\ Q.PAT_X_ASSUM `!env. bbb` 2065 (MP_TAC o Q.SPECL [`a'`,`code1`,`a1`,`stack`,`p`,`r`,`rs`,`q1`,`bc`,`bc1`,`bc7`]) 2066 \\ `BC_SUBSTATE bc1 bc7` by 2067 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 2068 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 2069 \\ FULL_SIMP_TAC std_ss []) 2070 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2071 \\ Q.PAT_X_ASSUM `!env code. bbb` 2072 (MP_TAC o Q.SPECL [`a'`,`code2`,`a2`,`stack`,`q1`,`r`,`rs`,`ret`,`p2`,`bc1`,`bc0`,`bc8`]) 2073 \\ `BC_SUBSTATE bc0 bc8` by 2074 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 2075 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 2076 \\ FULL_SIMP_TAC std_ss []) 2077 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2078 (FULL_SIMP_TAC std_ss [MAP_CONST_REVERSE] 2079 \\ IMP_RES_TAC BC_ev_LENGTH \\ FULL_SIMP_TAC std_ss [] 2080 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2081 \\ FULL_SIMP_TAC std_ss [] 2082 \\ `BC_SUBSTATE bc7 bc8` by 2083 (FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC iSTEP_BC_SUBSTATE \\ IMP_RES_TAC BC_ev_LENGTH 2084 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ IMP_RES_TAC BC_SUBSTATE_TRANS 2085 \\ FULL_SIMP_TAC std_ss []) 2086 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE \\ FULL_SIMP_TAC std_ss []) 2087 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [] 2088 \\ IMP_RES_TAC SUBMAP_TRANS \\ ASM_SIMP_TAC std_ss [] 2089 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2090 \\ Q.EXISTS_TAC `(REVERSE args ++ stack,q1,r::rs,bc8)` \\ ASM_SIMP_TAC std_ss [] 2091 \\ IMP_RES_TAC BC_ev_LENGTH \\ FULL_SIMP_TAC std_ss [] 2092 \\ ASM_SIMP_TAC std_ss [iLENGTH_APPEND,iLENGTH_def,ADD_ASSOC]) 2093 \\ STRIP_TAC THEN1 2094 (REVERSE (REPEAT STRIP_TAC) 2095 \\ Q.PAT_X_ASSUM `BC_ap zzz (PrimitiveFun fc,sdf) szzz` MP_TAC 2096 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2097 \\ ASM_SIMP_TAC std_ss [term_distinct,func_distinct,term_11,func_11,LENGTH_REVERSE,LENGTH] 2098 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 2099 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL] 2100 \\ `DROP (LENGTH args) (MAP (\x. ssTEMP) args ++ a') = a'` by (METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE]) 2101 \\ ASM_SIMP_TAC std_ss [] 2102 \\ FULL_SIMP_TAC std_ss [BC_return_code_def,LENGTH,iLENGTH_def,APPEND] 2103 \\ Q.EXISTS_TAC `bc7` \\ ASM_SIMP_TAC std_ss [] 2104 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2105 \\ Q.EXISTS_TAC `(f args::stack,p + bc.instr_length (iDATA fc),r::rs,bc7)` 2106 \\ ASM_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH] 2107 \\ STRIP_TAC THEN1 2108 (REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2109 \\ MATCH_MP_TAC iSTEP_cases_imp 2110 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11, 2111 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,BC_STEP_def] 2112 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2113 \\ ASM_SIMP_TAC std_ss [APPEND_11] \\ METIS_TAC []) 2114 \\ REVERSE (Cases_on `ret`) THEN1 (ASM_SIMP_TAC std_ss [RTC_REFL]) 2115 \\ FULL_SIMP_TAC std_ss [LENGTH] 2116 \\ MATCH_MP_TAC (GEN_ALL BC_return_code_thm) 2117 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2118 \\ Q.EXISTS_TAC `a` \\ ASM_SIMP_TAC std_ss [] 2119 \\ METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE]) 2120 \\ STRIP_TAC THEN1 2121 (REPEAT MOVE_TAC 2122 \\ Q.PAT_X_ASSUM `BC_ev zzz (App (Fun xx) yy,xxxx) yyyyyyy` MP_TAC 2123 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2124 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH] 2125 \\ ASM_SIMP_TAC std_ss [isFun_def,func_11] 2126 \\ REVERSE (Cases_on `ret`) \\ ASM_SIMP_TAC std_ss [] THEN1 2127 (REVERSE (REPEAT STRIP_TAC) \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 2128 LENGTH,LENGTH_APPEND,ADD_ASSOC] 2129 \\ POP_ASSUM MP_TAC 2130 \\ SIMP_TAC std_ss [BC_return_def] 2131 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,LENGTH_REVERSE,LENGTH] 2132 \\ REPEAT STRIP_TAC 2133 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND,BC_return_code_def,APPEND_NIL] 2134 \\ Q.PAT_X_ASSUM `!env. bbb` MP_TAC 2135 \\ Q.PAT_X_ASSUM `!env. bbb` 2136 (MP_TAC o Q.SPECL [`a'`,`code'`,`a2'`,`stack`,`p`,`r`,`rs`,`q2`,`bc`,`bc0`,`bc7`]) 2137 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] 2138 \\ REPEAT STRIP_TAC 2139 \\ Q.PAT_X_ASSUM `BC_REFINES (fns1,io1) bc8` (fn th => 2140 ASSUME_TAC th THEN MP_TAC th) 2141 \\ SIMP_TAC std_ss [Once BC_FNS_ASSUM_def,Once BC_REFINES_def] 2142 \\ REPEAT STRIP_TAC 2143 \\ Q.PAT_X_ASSUM `!fc params.bbb` (MP_TAC o Q.SPECL [`fc`,`params`,`exp`]) 2144 \\ ASM_SIMP_TAC std_ss [] 2145 \\ SIMP_TAC std_ss [PULL_EXISTS_IMP,PULL_FORALL_IMP,GSYM AND_IMP_INTRO] 2146 \\ `DROP (LENGTH (el:term list)) (MAP (\x. ssTEMP) (REVERSE args) ++ a') = a'` by (METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE]) 2147 \\ ASM_SIMP_TAC std_ss [AND_IMP_INTRO] 2148 (* \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 METIS_TAC [SUBMAP_DEF] *) 2149 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] 2150 \\ Q.PAT_X_ASSUM `!a code.bbb` (MP_TAC o 2151 Q.SPECL [`MAP ssVAR (REVERSE params)`,`pcode`,`a5`, 2152 `REVERSE args ++ stack`,`p'`,`(p + 2153 iLENGTH bc.instr_length (code' ++ BC_call F (fc,LENGTH (el:term list),FUN_LOOKUP bc.compiled fc)))`,`r::rs`,`T`,`p' + iLENGTH bc8.instr_length pcode`,`bc4`,`bc5`,`bc8`]) 2154 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC 2155 THEN1 (ASM_SIMP_TAC std_ss [STACK_INV_VarBind,BC_SUBSTATE_REFL]) 2156 \\ REPEAT STRIP_TAC 2157 \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [] 2158 \\ IMP_RES_TAC SUBMAP_TRANS \\ ASM_SIMP_TAC std_ss [] 2159 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2160 \\ Q.EXISTS_TAC `(REVERSE args ++ stack,p',(p + 2161 iLENGTH bc.instr_length (code' ++ BC_call F (fc,LENGTH el,FUN_LOOKUP bc.compiled fc)))::r::rs,bc8)` 2162 \\ REVERSE STRIP_TAC THEN1 2163 (FULL_SIMP_TAC std_ss [iSTEP_ret_state_def,HD,getVal_def,APPEND,BC_call_def,BC_call_aux_def,BC_call_aux_def] 2164 \\ `DROP (LENGTH params) (REVERSE args ++ stack) = stack` by 2165 METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE] 2166 \\ FULL_SIMP_TAC std_ss [LENGTH_MAP,LENGTH_REVERSE]) 2167 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2168 \\ Q.EXISTS_TAC `(REVERSE args ++ stack,p + iLENGTH bc.instr_length code',r::rs,bc8)` 2169 \\ ASM_SIMP_TAC std_ss [] 2170 \\ REVERSE (Cases_on `FUN_LOOKUP bc.compiled fc`) THEN1 2171 (`BC_SUBSTATE bc bc7` by BC_SUBSTATE_TAC 2172 \\ `BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2173 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2174 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2175 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2176 \\ `FUN_LOOKUP bc8.compiled fc = FUN_LOOKUP bc.compiled fc` by (METIS_TAC [BC_SUBSTATE_def,NOT_SOME_NONE]) 2177 \\ FULL_SIMP_TAC std_ss [BC_call_def,BC_call_aux_def,CONTAINS_BYTECODE_def] 2178 \\ FULL_SIMP_TAC std_ss [] \\ IMP_RES_TAC BC_SUBSTATE_IMP 2179 \\ REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2180 \\ MATCH_MP_TAC iSTEP_cases_imp 2181 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,ADD_ASSOC,BC_STEP_def, 2182 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND,iLENGTH_APPEND,iLENGTH_def]) 2183 \\ FULL_SIMP_TAC std_ss [BC_call_def,BC_call_aux_def,CONTAINS_BYTECODE_def] 2184 \\ `BC_SUBSTATE bc bc7` by BC_SUBSTATE_TAC 2185 \\ `BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2186 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2187 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2188 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2189 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND,CONTAINS_BYTECODE_def] 2190 \\ IMP_RES_TAC BC_SUBSTATE_IMP 2191 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2192 \\ Q.EXISTS_TAC `(Val (LENGTH el)::(REVERSE args ++ stack),p + iLENGTH bc.instr_length (code' ++ [iCONST_NUM (LENGTH el)]),r::rs,bc8)` 2193 \\ STRIP_TAC THEN1 2194 (REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2195 \\ MATCH_MP_TAC iSTEP_cases_imp 2196 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,ADD_ASSOC,BC_STEP_def, 2197 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND,iLENGTH_APPEND,iLENGTH_def]) 2198 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2199 \\ Q.EXISTS_TAC `(Sym fc::Val (LENGTH el)::(REVERSE args ++ stack),p + iLENGTH bc.instr_length (code' ++ [iCONST_NUM (LENGTH el);iCONST_SYM fc]),r::rs,bc8)` 2200 \\ STRIP_TAC THEN1 2201 (REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2202 \\ MATCH_MP_TAC iSTEP_cases_imp 2203 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,ADD_ASSOC,BC_STEP_def, 2204 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND,iLENGTH_APPEND,iLENGTH_def]) 2205 THEN1 2206 (REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2207 \\ MATCH_MP_TAC iSTEP_cases_imp 2208 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,ADD_ASSOC, 2209 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND,iLENGTH_APPEND,iLENGTH_def] 2210 \\ FULL_SIMP_TAC (srw_ss()) [BC_STEP_def])) 2211 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 2212 LENGTH,LENGTH_APPEND,ADD_ASSOC] 2213 \\ REPEAT STRIP_TAC 2214 \\ Q.ABBREV_TAC `padding = LENGTH el - LENGTH a'` 2215 \\ Q.ABBREV_TAC `a9 = n_times padding ssTEMP ++ a'` 2216 \\ Q.ABBREV_TAC `stack9 = n_times padding (Sym "NIL") ++ stack` 2217 \\ `STACK_INV a stack9 a9` by 2218 (Q.UNABBREV_TAC `stack9` \\ Q.UNABBREV_TAC `a9` \\ IMP_RES_TAC n_times_iCONST) 2219 \\ MP_TAC (Q.SPECL [`padding`,`a'`,`stack`,`a`,`bc7`,`p`] n_times_iCONST) 2220 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2221 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2222 \\ SIMP_TAC std_ss [EXISTS_LEMMA] 2223 \\ Q.EXISTS_TAC `(stack9,p + iLENGTH bc.instr_length (n_times padding (iCONST_SYM "NIL")),r::rs,bc7)` 2224 \\ `BC_SUBSTATE bc bc7` by BC_SUBSTATE_TAC 2225 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_SUBSTATE_def] 2226 \\ FULL_SIMP_TAC std_ss [] 2227 \\ Q.PAT_X_ASSUM `!env. bbb` MP_TAC 2228 \\ Q.PAT_X_ASSUM `!env. bbb` 2229 (MP_TAC o Q.SPECL [`a9`,`code'`,`a2'`,`stack9`,`p + iLENGTH bc.instr_length (n_times padding (iCONST_SYM "NIL"))`,`r`,`rs`,`q2`,`bc`,`bc0`,`bc7`]) 2230 \\ FULL_SIMP_TAC std_ss [] 2231 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] 2232 \\ REPEAT STRIP_TAC 2233 \\ IMP_RES_TAC BC_ev_LENGTH 2234 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] 2235 \\ Q.PAT_X_ASSUM `BC_REFINES (fns1,io1) bc8` (fn th => 2236 ASSUME_TAC th THEN MP_TAC th) 2237 \\ SIMP_TAC std_ss [Once BC_FNS_ASSUM_def,Once BC_REFINES_def] 2238 \\ REPEAT STRIP_TAC 2239 \\ Q.PAT_X_ASSUM `!fc params. bbb` (MP_TAC o Q.SPECL [`fc`,`params`,`exp`]) 2240 \\ ASM_SIMP_TAC std_ss [] \\ STRIP_TAC 2241 \\ `BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2242 \\ `bc.instr_length = bc8.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2243 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2244 \\ SIMP_TAC std_ss [EXISTS_LEMMA] 2245 \\ Q.EXISTS_TAC `(REVERSE args ++ stack9,p + iLENGTH bc.instr_length (n_times padding (iCONST_SYM "NIL") ++ code'),r::rs,bc8)` 2246 \\ STRIP_TAC THEN1 (FULL_SIMP_TAC std_ss [iLENGTH_APPEND,ADD_ASSOC]) 2247 \\ Q.PAT_X_ASSUM `!a b.bbb` (MP_TAC o Q.SPECL 2248 [`MAP ssVAR (REVERSE params)`,`pcode`,`a5`,`REVERSE args++DROP (LENGTH (a':stack_slot list)) stack`,`p'`,`r`,`rs`,`T`,`p' + iLENGTH bc.instr_length pcode`,`bc4`,`bc5`,`bc8`]) 2249 \\ ASM_SIMP_TAC std_ss [] 2250 \\ MATCH_MP_TAC IMP_IMP 2251 \\ STRIP_TAC THEN1 2252 (ASM_SIMP_TAC std_ss [STACK_INV_VarBind,iSTEP_ret_state_APPEND_MAP]) 2253 \\ REPEAT STRIP_TAC 2254 \\ `fns SUBMAP fns2` by METIS_TAC [SUBMAP_TRANS] 2255 \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [] 2256 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2257 \\ Q.EXISTS_TAC `(REVERSE args ++ DROP (LENGTH a') stack,p',r::rs,bc8)` 2258 \\ ASM_SIMP_TAC std_ss [] 2259 \\ REVERSE STRIP_TAC THEN1 2260 (Q.PAT_X_ASSUM `RTC iSTEP xxx yyy` MP_TAC 2261 \\ ASM_SIMP_TAC std_ss [(RW[APPEND_NIL](Q.INST [`a2`|->`[]`] iSTEP_ret_state_APPEND_MAP))] 2262 \\ ASM_SIMP_TAC std_ss [iSTEP_ret_state_def,LENGTH,DROP_0]) 2263 \\ Q.UNABBREV_TAC `a9` \\ Q.UNABBREV_TAC `stack9` 2264 \\ `?stack1 stack2. (LENGTH a' = LENGTH stack1) /\ 2265 (stack = stack1 ++ stack2)` by 2266 METIS_TAC [LENGTH_LESS_EQ_LENGTH_IMP,STACK_INV_def] 2267 \\ FULL_SIMP_TAC std_ss [rich_listTheory.BUTFIRSTN_LENGTH_APPEND] 2268 \\ SIMP_TAC std_ss [APPEND_ASSOC] 2269 \\ REVERSE (Cases_on `padding = 0`) THEN1 2270 (`LENGTH stack1 <= LENGTH el /\ 2271 (padding + LENGTH stack1 = LENGTH el)` by 2272 (Q.UNABBREV_TAC `padding` \\ POP_ASSUM MP_TAC 2273 \\ REPEAT (POP_ASSUM (K ALL_TAC)) \\ DECIDE_TAC) 2274 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2275 \\ Q.EXISTS_TAC `(REVERSE args ++ stack2, 2276 p + iLENGTH bc.instr_length (n_times padding (iCONST_SYM "NIL")) + iLENGTH bc.instr_length code' + iLENGTH bc.instr_length (n_times (LENGTH (REVERSE args)) (iSTORE (LENGTH (REVERSE args) - 1))),r::rs,bc8)` 2277 \\ STRIP_TAC THEN1 2278 (FULL_SIMP_TAC std_ss [iLENGTH_APPEND,ADD_ASSOC] 2279 \\ `BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2280 \\ `bc.instr_length = bc8.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2281 \\ FULL_SIMP_TAC std_ss [] 2282 \\ MATCH_MP_TAC (RW [APPEND,APPEND_NIL,APPEND_ASSOC] 2283 (Q.SPECL [`xs1++xs2`,`REVERSE args`,`[]`,`bc8`,`q`,`stack2`] n_times_iSTORE)) 2284 \\ ASM_SIMP_TAC std_ss [LENGTH_n_times,LENGTH_REVERSE,LENGTH_APPEND] 2285 \\ Q.PAT_X_ASSUM `padding + LENGTH stack1 = LENGTH el` (MP_TAC o GSYM) 2286 \\ `~(padding + LENGTH stack1 <= LENGTH stack1)` by DECIDE_TAC 2287 \\ FULL_SIMP_TAC std_ss [AC ADD_COMM ADD_ASSOC,iLENGTH_APPEND] 2288 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2289 \\ REPEAT STRIP_TAC \\ MATCH_MP_TAC (GEN_ALL BC_SUBSTATE_BYTECODE) 2290 \\ FULL_SIMP_TAC std_ss [] 2291 \\ Q.LIST_EXISTS_TAC [`io`,`fns`,`bc7`] 2292 \\ FULL_SIMP_TAC std_ss []) 2293 \\ `LENGTH stack1 - LENGTH el = 0` by DECIDE_TAC 2294 \\ FULL_SIMP_TAC std_ss [gen_popn_def,APPEND_NIL,LENGTH] 2295 \\ REVERSE (Cases_on `FUN_LOOKUP bc.compiled fc`) THEN1 2296 (`BC_SUBSTATE bc bc7` by BC_SUBSTATE_TAC 2297 \\ `BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2298 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2299 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2300 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2301 \\ `FUN_LOOKUP bc8.compiled fc = FUN_LOOKUP bc.compiled fc` by METIS_TAC [BC_SUBSTATE_def,NOT_SOME_NONE] 2302 \\ FULL_SIMP_TAC std_ss [] 2303 \\ FULL_SIMP_TAC std_ss [BC_call_def,BC_call_aux_def,CONTAINS_BYTECODE_def] 2304 \\ IMP_RES_TAC BC_SUBSTATE_IMP 2305 \\ `LENGTH el = LENGTH args` by DECIDE_TAC 2306 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,AC ADD_ASSOC ADD_COMM,LENGTH_REVERSE] 2307 \\ Q.PAT_X_ASSUM `padding + LENGTH stack1 = LENGTH args` ASSUME_TAC 2308 \\ FULL_SIMP_TAC std_ss [] 2309 \\ REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2310 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,LENGTH_REVERSE] 2311 \\ MATCH_MP_TAC iSTEP_cases_imp 2312 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11, 2313 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND, 2314 AC ADD_ASSOC ADD_COMM,LENGTH_REVERSE,iLENGTH_APPEND]) 2315 \\ MATCH_MP_TAC (GEN_ALL BC_call_thm) 2316 \\ Q.EXISTS_TAC `fc` \\ ASM_SIMP_TAC std_ss [] 2317 \\ FULL_SIMP_TAC std_ss [LENGTH_REVERSE] 2318 \\ FULL_SIMP_TAC std_ss [BC_call_def,BC_call_aux_def,CONTAINS_BYTECODE_def] 2319 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2320 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2321 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2322 \\ `FUN_LOOKUP bc8.compiled fc = FUN_LOOKUP bc8.compiled fc` by METIS_TAC [BC_SUBSTATE_def,NOT_SOME_NONE] 2323 \\ FULL_SIMP_TAC std_ss [] 2324 \\ IMP_RES_TAC BC_SUBSTATE_IMP 2325 \\ `LENGTH el = LENGTH args` by DECIDE_TAC 2326 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM,iLENGTH_APPEND] 2327 \\ Q.PAT_X_ASSUM `padding + LENGTH stack1 = LENGTH args` ASSUME_TAC 2328 \\ FULL_SIMP_TAC std_ss []) 2329 \\ FULL_SIMP_TAC std_ss [n_times_def,APPEND_NIL,APPEND] 2330 \\ `LENGTH args <= LENGTH stack1` by METIS_TAC [markerTheory.Abbrev_def] 2331 \\ `?stack1A stack1B. (stack1 = stack1A ++ stack1B) /\ (LENGTH stack1B = LENGTH args)` 2332 by METIS_TAC [LESS_EQ_IMP_APPEND] 2333 \\ FULL_SIMP_TAC std_ss [APPEND_ASSOC,iLENGTH_def] 2334 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2335 \\ Q.EXISTS_TAC `(stack1A ++ REVERSE args ++ stack2,p + iLENGTH bc.instr_length code' + iLENGTH bc.instr_length (n_times (LENGTH (REVERSE args)) (iSTORE (LENGTH (REVERSE args ++ stack1A) - 1))),r::rs,bc8)` 2336 \\ STRIP_TAC THEN1 2337 (`BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2338 \\ `bc.instr_length = bc8.instr_length` by METIS_TAC [BC_SUBSTATE_def] 2339 \\ FULL_SIMP_TAC std_ss [] 2340 \\ MATCH_MP_TAC n_times_iSTORE 2341 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND,LENGTH_REVERSE,LENGTH_n_times] 2342 \\ Q.PAT_X_ASSUM `LENGTH args = LENGTH el` ASSUME_TAC 2343 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM,iLENGTH_APPEND,iLENGTH_def] 2344 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2345 \\ METIS_TAC [BC_SUBSTATE_BYTECODE,ADD_ASSOC,iLENGTH_APPEND]) 2346 \\ ASM_SIMP_TAC std_ss [LENGTH_REVERSE] 2347 \\ FULL_SIMP_TAC std_ss [LENGTH_APPEND] 2348 \\ Q.PAT_X_ASSUM `LENGTH args = LENGTH el` ASSUME_TAC 2349 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2350 \\ FULL_SIMP_TAC std_ss [] 2351 \\ Q.EXISTS_TAC `(REVERSE args ++ stack2,p + iLENGTH bc.instr_length code' + 2352 iLENGTH bc.instr_length (n_times (LENGTH el) (iSTORE (LENGTH (REVERSE args) + LENGTH stack1A - 1)) ++ gen_popn (LENGTH stack1A)),r::rs,bc8)` 2353 \\ STRIP_TAC THEN1 2354 (`BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2355 \\ `bc.instr_length = bc8.instr_length` by METIS_TAC [BC_SUBSTATE_def] 2356 \\ FULL_SIMP_TAC std_ss [GSYM APPEND_ASSOC,iLENGTH_APPEND,ADD_ASSOC] 2357 \\ MATCH_MP_TAC gen_popn_thm 2358 \\ FULL_SIMP_TAC std_ss [iLENGTH_def,AC ADD_ASSOC ADD_COMM,LENGTH_REVERSE] 2359 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2360 \\ METIS_TAC [BC_SUBSTATE_BYTECODE,ADD_ASSOC,iLENGTH_APPEND]) 2361 \\ REVERSE (Cases_on `FUN_LOOKUP bc.compiled fc`) THEN1 2362 (`BC_SUBSTATE bc bc7` by BC_SUBSTATE_TAC 2363 \\ `BC_SUBSTATE bc bc8` by BC_SUBSTATE_TAC 2364 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2365 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2366 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2367 \\ `FUN_LOOKUP bc8.compiled fc = FUN_LOOKUP bc.compiled fc` by METIS_TAC [BC_SUBSTATE_def,NOT_SOME_NONE] 2368 \\ FULL_SIMP_TAC std_ss [] 2369 \\ FULL_SIMP_TAC std_ss [BC_call_def,BC_call_aux_def,CONTAINS_BYTECODE_def] 2370 \\ IMP_RES_TAC BC_SUBSTATE_IMP 2371 \\ `LENGTH el = LENGTH args` by DECIDE_TAC 2372 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,AC ADD_ASSOC ADD_COMM,LENGTH_REVERSE] 2373 \\ FULL_SIMP_TAC std_ss [] 2374 \\ REPEAT STRIP_TAC \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2375 \\ FULL_SIMP_TAC std_ss [iLENGTH_APPEND,LENGTH_REVERSE] 2376 \\ MATCH_MP_TAC iSTEP_cases_imp 2377 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11, 2378 LENGTH,CONS_11,STACK_INV_lemma,CONTAINS_BYTECODE_def,APPEND, 2379 AC ADD_ASSOC ADD_COMM,LENGTH_REVERSE,iLENGTH_APPEND]) 2380 \\ MATCH_MP_TAC (GEN_ALL BC_call_thm) 2381 \\ Q.EXISTS_TAC `fc` \\ ASM_SIMP_TAC std_ss [] 2382 \\ FULL_SIMP_TAC std_ss [LENGTH_REVERSE] 2383 \\ FULL_SIMP_TAC std_ss [BC_call_def,BC_call_aux_def,CONTAINS_BYTECODE_def] 2384 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2385 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2386 \\ `bc8.instr_length = bc.instr_length` by METIS_TAC [BC_ev_LENGTH,BC_SUBSTATE_def] 2387 \\ FULL_SIMP_TAC std_ss [] 2388 \\ IMP_RES_TAC BC_SUBSTATE_IMP 2389 \\ `LENGTH el = LENGTH args` by DECIDE_TAC 2390 \\ FULL_SIMP_TAC std_ss [AC ADD_ASSOC ADD_COMM,iLENGTH_APPEND] 2391 \\ Q.PAT_X_ASSUM `padding + LENGTH stack1 = LENGTH args` ASSUME_TAC 2392 \\ FULL_SIMP_TAC std_ss []) 2393 \\ STRIP_TAC THEN1 2394 (REVERSE (REPEAT STRIP_TAC) 2395 \\ Q.PAT_X_ASSUM `BC_ap zzz (Print,xxx) szzz` MP_TAC 2396 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2397 \\ ASM_SIMP_TAC std_ss [term_distinct,func_distinct,term_11,func_11,LENGTH_REVERSE,LENGTH] 2398 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [ 2399 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL] 2400 \\ `DROP (LENGTH args) (MAP (\x. ssTEMP) args ++ a') = a'` by 2401 (METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE]) 2402 \\ ASM_SIMP_TAC std_ss [] 2403 \\ Q.EXISTS_TAC `BC_PRINT bc7 (sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n")` 2404 \\ REVERSE STRIP_TAC THEN1 2405 (FULL_SIMP_TAC std_ss [BC_REFINES_def,BC_CODE_OK_PRINT] \\ REVERSE STRIP_TAC 2406 THEN1 (FULL_SIMP_TAC (srw_ss()) [BC_PRINT_def]) 2407 \\ Q.PAT_X_ASSUM `BC_FNS_ASSUM fns bc7` MP_TAC 2408 \\ SIMP_TAC std_ss [BC_FNS_ASSUM_def,BC_PRINT_CONTAINS_BYTECODE] 2409 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,BC_CODE_OK_PRINT] 2410 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,BC_PRINT_def] \\ METIS_TAC []) 2411 \\ Q.ABBREV_TAC `ys = [iCONST_SYM "NIL"] ++ n_times (LENGTH args) (iDATA opCONS)` 2412 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2413 \\ Q.EXISTS_TAC `(list2sexp args :: stack,p + iLENGTH bc.instr_length ys,r::rs,bc7)` 2414 \\ STRIP_TAC THEN1 2415 (FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] \\ Q.UNABBREV_TAC `ys` 2416 \\ `bc7.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2417 \\ IMP_RES_TAC n_times_CONS \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 2418 \\ `bc7.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2419 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND,CONTAINS_BYTECODE_def] 2420 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2421 \\ Q.EXISTS_TAC `(Sym "PRINT" :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "PRINT"]),r::rs,bc7)` 2422 \\ STRIP_TAC THEN1 2423 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2424 \\ MATCH_MP_TAC iSTEP_cases_imp 2425 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2426 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2427 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM]) 2428 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2429 \\ Q.EXISTS_TAC `(list2sexp args :: Sym "PRINT" :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "PRINT"; iLOAD 1]),r::rs,bc7)` 2430 \\ STRIP_TAC THEN1 2431 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2432 \\ MATCH_MP_TAC iSTEP_cases_imp 2433 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2434 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2435 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def] 2436 \\ EVAL_TAC \\ DECIDE_TAC) 2437 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2438 \\ Q.EXISTS_TAC `(list2sexp (Sym "PRINT"::args) :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "PRINT"; iLOAD 1; iDATA opCONS]),r::rs,bc7)` 2439 \\ STRIP_TAC THEN1 2440 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2441 \\ MATCH_MP_TAC iSTEP_cases_imp 2442 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2443 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2444 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def] 2445 \\ Q.EXISTS_TAC `[Sym "PRINT";list2sexp args]` \\ EVAL_TAC) 2446 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2447 \\ Q.EXISTS_TAC `(list2sexp (Sym "PRINT"::args) :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "PRINT"; iLOAD 1; iDATA opCONS; iPRINT]),r::rs,BC_PRINT bc7 (sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n"))` 2448 \\ STRIP_TAC THEN1 2449 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2450 \\ MATCH_MP_TAC iSTEP_cases_imp 2451 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2452 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2453 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def]) 2454 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2455 \\ Q.EXISTS_TAC `(Sym "NIL" :: list2sexp (Sym "PRINT"::args) :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "PRINT"; iLOAD 1; iDATA opCONS; iPRINT; iCONST_SYM "NIL"]),r::rs,BC_PRINT bc7 (sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n"))` 2456 \\ STRIP_TAC THEN1 2457 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2458 \\ MATCH_MP_TAC iSTEP_cases_imp 2459 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2460 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2461 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code]) 2462 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2463 \\ Q.EXISTS_TAC `(Sym "NIL" :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "PRINT"; iLOAD 1; iDATA opCONS; iPRINT; iCONST_SYM "NIL"; iPOPS 2]),r::rs,BC_PRINT bc7 (sexp2string (list2sexp (Sym "PRINT"::args)) ++ "\n"))` 2464 \\ STRIP_TAC THEN1 2465 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2466 \\ MATCH_MP_TAC iSTEP_cases_imp 2467 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2468 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2469 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code] 2470 \\ Q.EXISTS_TAC `list2sexp (Sym "PRINT"::args)::list2sexp args::[]` \\ EVAL_TAC) 2471 THEN 2472 (REVERSE (Cases_on `ret`) 2473 \\ FULL_SIMP_TAC std_ss [RTC_REFL,iLENGTH_def,BC_return_code_def,APPEND_NIL] 2474 \\ MATCH_MP_TAC BC_return_code_thm 2475 \\ FULL_SIMP_TAC std_ss [BC_return_code_def,BC_PRINT_CONTAINS_BYTECODE])) 2476 \\ STRIP_TAC THEN1 2477 (REVERSE (REPEAT STRIP_TAC) 2478 \\ Q.PAT_X_ASSUM `BC_ap zzz (Error,xxx) szzz` MP_TAC 2479 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2480 \\ ASM_SIMP_TAC std_ss [term_distinct,func_distinct,term_11,func_11,LENGTH_REVERSE,LENGTH] 2481 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [ 2482 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL] 2483 \\ `DROP (LENGTH args) (MAP (\x. ssTEMP) args ++ a') = a'` by 2484 (METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,LENGTH_MAP,LENGTH_REVERSE]) 2485 \\ ASM_SIMP_TAC std_ss [] 2486 \\ Q.EXISTS_TAC `BC_FAIL (BC_PRINT bc7 (sexp2string (list2sexp (Sym "ERROR"::args)) ++ "\n"))` 2487 \\ REVERSE STRIP_TAC THEN1 2488 (REVERSE STRIP_TAC THEN1 EVAL_TAC 2489 \\ FULL_SIMP_TAC std_ss [BC_REFINES_def,BC_CODE_OK_PRINT,BC_CODE_OK_FAIL] 2490 \\ REVERSE STRIP_TAC 2491 THEN1 (FULL_SIMP_TAC (srw_ss()) [BC_PRINT_def,BC_FAIL_def]) 2492 \\ Q.PAT_X_ASSUM `BC_FNS_ASSUM fns bc7` MP_TAC 2493 \\ SIMP_TAC std_ss [BC_FNS_ASSUM_def,BC_PRINT_CONTAINS_BYTECODE,BC_FAIL_CONTAINS_BYTECODE] 2494 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,BC_CODE_OK_PRINT,BC_CODE_OK_FAIL] 2495 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,BC_PRINT_def,BC_FAIL_def] 2496 \\ METIS_TAC []) 2497 \\ Q.ABBREV_TAC `ys = [iCONST_SYM "NIL"] ++ n_times (LENGTH args) (iDATA opCONS)` 2498 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2499 \\ Q.EXISTS_TAC `(list2sexp args :: stack,p + iLENGTH bc.instr_length ys,r::rs,bc7)` 2500 \\ STRIP_TAC THEN1 2501 (FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] \\ Q.UNABBREV_TAC `ys` 2502 \\ `bc7.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2503 \\ IMP_RES_TAC n_times_CONS \\ FULL_SIMP_TAC std_ss [] \\ METIS_TAC []) 2504 \\ `bc7.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2505 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND,CONTAINS_BYTECODE_def] 2506 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2507 \\ Q.EXISTS_TAC `(Sym "ERROR" :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "ERROR"]),r::rs,bc7)` 2508 \\ STRIP_TAC THEN1 2509 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2510 \\ MATCH_MP_TAC iSTEP_cases_imp 2511 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2512 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2513 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM]) 2514 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2515 \\ Q.EXISTS_TAC `(list2sexp args :: Sym "ERROR" :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "ERROR"; iLOAD 1]),r::rs,bc7)` 2516 \\ STRIP_TAC THEN1 2517 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2518 \\ MATCH_MP_TAC iSTEP_cases_imp 2519 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2520 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2521 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def] 2522 \\ EVAL_TAC \\ DECIDE_TAC) 2523 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2524 \\ Q.EXISTS_TAC `(list2sexp (Sym "ERROR"::args) :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "ERROR"; iLOAD 1; iDATA opCONS]),r::rs,bc7)` 2525 \\ STRIP_TAC THEN1 2526 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2527 \\ MATCH_MP_TAC iSTEP_cases_imp 2528 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2529 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2530 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def] 2531 \\ Q.EXISTS_TAC `[Sym "ERROR";list2sexp args]` \\ EVAL_TAC) 2532 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2533 \\ Q.EXISTS_TAC `(list2sexp (Sym "ERROR"::args) :: list2sexp args :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "ERROR"; iLOAD 1; iDATA opCONS; iPRINT]),r::rs,BC_PRINT bc7 (sexp2string (list2sexp (Sym "ERROR"::args)) ++ "\n"))` 2534 \\ STRIP_TAC THEN1 2535 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2536 \\ MATCH_MP_TAC iSTEP_cases_imp 2537 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2538 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2539 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def]) 2540 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2541 \\ Q.EXISTS_TAC `(anything :: stack,p + iLENGTH bc.instr_length (ys ++ [iCONST_SYM "ERROR"; iLOAD 1; iDATA opCONS; iPRINT; iFAIL]),r::rs,BC_FAIL (BC_PRINT bc7 (sexp2string (list2sexp (Sym "ERROR"::args)) ++ "\n")))` 2542 \\ STRIP_TAC THEN1 2543 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2544 \\ MATCH_MP_TAC iSTEP_cases_imp 2545 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2546 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2547 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code]) 2548 THEN 2549 (REVERSE (Cases_on `ret`) 2550 \\ FULL_SIMP_TAC std_ss [RTC_REFL,iLENGTH_def,BC_return_code_def,APPEND_NIL] 2551 \\ MATCH_MP_TAC BC_return_code_thm 2552 \\ FULL_SIMP_TAC std_ss [BC_return_code_def,BC_PRINT_CONTAINS_BYTECODE, 2553 BC_FAIL_CONTAINS_BYTECODE])) 2554 2555 \\ STRIP_TAC THEN1 2556 (REPEAT STRIP_TAC 2557 \\ Q.PAT_X_ASSUM `BC_ap zzz (Define,xxx) szzz` MP_TAC 2558 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2559 \\ ASM_SIMP_TAC std_ss [term_distinct,func_distinct,term_11,func_11,LENGTH_REVERSE,LENGTH] 2560 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 2561 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL,MAP] 2562 \\ `DROP 3 ([ssTEMP; ssTEMP; ssTEMP] ++ a') = a'` by FULL_SIMP_TAC std_ss [DROP_def,APPEND,DROP_0] 2563 \\ FULL_SIMP_TAC std_ss [REVERSE_DEF,APPEND] 2564 \\ REVERSE (Cases_on `getSym fc NOTIN FDOM fns`) 2565 \\ FULL_SIMP_TAC std_ss [add_def_NOP,SUBMAP_REFL] THEN1 2566 (Q.EXISTS_TAC `BC_FAIL bc7` 2567 \\ REVERSE STRIP_TAC THEN1 2568 (REVERSE STRIP_TAC THEN1 EVAL_TAC 2569 \\ FULL_SIMP_TAC (srw_ss()) [BC_REFINES_def] 2570 \\ Q.PAT_X_ASSUM `BC_FNS_ASSUM fns bc7` MP_TAC 2571 \\ FULL_SIMP_TAC std_ss [BC_FNS_ASSUM_def,BC_FAIL_CONTAINS_BYTECODE] 2572 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,BC_CODE_OK_FAIL] 2573 \\ FULL_SIMP_TAC (srw_ss()) [BC_SUBSTATE_def,BC_FAIL_def] \\ METIS_TAC []) 2574 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2575 \\ Q.EXISTS_TAC `(Sym "NIL"::stack,p + iLENGTH bc.instr_length [iCOMPILE],r::rs,BC_FAIL bc7)` 2576 \\ STRIP_TAC THEN1 2577 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2578 \\ MATCH_MP_TAC iSTEP_cases_imp 2579 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2580 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2581 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code] 2582 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_SUBSTATE_def] 2583 \\ FULL_SIMP_TAC std_ss [BC_REFINES_def] 2584 \\ FULL_SIMP_TAC std_ss [GSPECIFICATION,EXTENSION]) 2585 \\ ASSUME_TAC (EVAL ``(BC_FAIL bc7).ok``) \\ FULL_SIMP_TAC std_ss [] 2586 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2587 \\ Cases_on `ret` 2588 \\ ONCE_REWRITE_TAC [iSTEP_cases] 2589 \\ FULL_SIMP_TAC std_ss [iSTEP_ret_state_def]) 2590 \\ FULL_SIMP_TAC std_ss [add_def_FUPDATE] 2591 \\ `?bc5. BC_COMPILE (getSym fc,MAP getSym (sexp2list formals),sexp2term body,bc7) = bc5` by METIS_TAC [] 2592 \\ Q.EXISTS_TAC `bc5` 2593 \\ `fns SUBMAP fns |+ (getSym fc,MAP getSym (sexp2list formals),sexp2term body)` by 2594 (FULL_SIMP_TAC std_ss [SUBMAP_DEF,FDOM_FUPDATE,FAPPLY_FUPDATE_THM,IN_INSERT] 2595 \\ METIS_TAC []) \\ ASM_SIMP_TAC std_ss [] 2596 \\ REVERSE (REPEAT STRIP_TAC) THEN1 2597 (POP_ASSUM (K ALL_TAC) 2598 \\ POP_ASSUM (fn th => SIMP_TAC std_ss [GSYM th]) 2599 \\ FULL_SIMP_TAC std_ss [BC_COMPILE_compiled_instr_length,BC_REFINES_def]) 2600 THEN1 2601 (Q.PAT_X_ASSUM `xxx = bc5` (fn th => SIMP_TAC std_ss [GSYM th]) 2602 \\ METIS_TAC [BC_REFINES_COMPILE]) 2603 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2604 \\ Q.EXISTS_TAC `(Sym "NIL"::stack,p + iLENGTH bc.instr_length [iCOMPILE],r::rs,bc5)` 2605 \\ STRIP_TAC THEN1 2606 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2607 \\ MATCH_MP_TAC iSTEP_cases_imp 2608 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2609 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2610 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code] 2611 \\ `bc7.instr_length = bc.instr_length` by METIS_TAC [BC_SUBSTATE_def] 2612 \\ FULL_SIMP_TAC std_ss [BC_REFINES_def] 2613 \\ Q.PAT_X_ASSUM `xxx = FDOM fns` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 2614 \\ FULL_SIMP_TAC std_ss [GSPECIFICATION]) 2615 \\ REVERSE (Cases_on `ret`) 2616 \\ FULL_SIMP_TAC std_ss [RTC_REFL,iLENGTH_def,BC_return_code_def,APPEND_NIL] 2617 \\ MATCH_MP_TAC BC_return_code_thm \\ ASM_SIMP_TAC std_ss [] 2618 \\ `BC_SUBSTATE bc7 bc5` by 2619 (FULL_SIMP_TAC std_ss [BC_REFINES_def] 2620 \\ Q.PAT_X_ASSUM `xxx = FDOM fns` (fn th => FULL_SIMP_TAC std_ss [GSYM th]) 2621 \\ FULL_SIMP_TAC std_ss [GSPECIFICATION] 2622 \\ IMP_RES_TAC BC_COMPILE_SUBSTATE) 2623 \\ `BC_SUBSTATE bc bc5` by BC_SUBSTATE_TAC 2624 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 2625 \\ `bc5.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2626 \\ `bc7.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2627 \\ FULL_SIMP_TAC std_ss [BC_return_code_def]) 2628 2629 \\ STRIP_TAC THEN1 2630 (REPEAT STRIP_TAC 2631 \\ Q.PAT_X_ASSUM `BC_ap zzz (Funcall,xxx) szzz` MP_TAC 2632 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2633 \\ ASM_SIMP_TAC std_ss [term_distinct,func_distinct,term_11,func_11,LENGTH_REVERSE,LENGTH] 2634 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND, 2635 LENGTH,LENGTH_APPEND,ADD_ASSOC,SUBMAP_REFL,MAP] 2636 \\ Q.PAT_X_ASSUM `BC_REFINES (fns1,io1) bc8` (fn th => 2637 ASSUME_TAC th THEN MP_TAC th) 2638 \\ SIMP_TAC std_ss [Once BC_FNS_ASSUM_def,Once BC_REFINES_def] 2639 \\ REPEAT STRIP_TAC 2640 \\ Q.PAT_X_ASSUM `!fc params.bbb` (MP_TAC o Q.SPECL [`fname`,`params`,`exp`]) 2641 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2642 \\ `BC_SUBSTATE bc bc7`by BC_SUBSTATE_TAC 2643 \\ `bc7.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2644 \\ FULL_SIMP_TAC std_ss [] 2645 \\ Q.PAT_X_ASSUM `!a code.bbb` (MP_TAC o 2646 Q.SPECL [`MAP ssVAR (REVERSE params)`,`pcode`,`a5`, 2647 `REVERSE args ++ [Sym fname] ++ stack`,`p'`,`(p + 2648 iLENGTH bc.instr_length [iCONST_NUM (LENGTH (args:SExp list)); iLOAD (SUC (LENGTH args)); iCALL_SYM])`,`r::rs`,`T`,`p' + iLENGTH bc.instr_length pcode`,`bc4`,`bc5`,`bc7`]) 2649 \\ ASM_SIMP_TAC std_ss [] 2650 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2651 (SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] 2652 \\ MATCH_MP_TAC STACK_INV_VarBind \\ ASM_SIMP_TAC std_ss []) 2653 \\ REPEAT STRIP_TAC \\ Q.EXISTS_TAC `bc8` \\ ASM_SIMP_TAC std_ss [] 2654 \\ REVERSE STRIP_TAC THEN1 2655 (`LENGTH (ssTEMP::MAP (\x. ssTEMP) (args:SExp list)) = SUC (LENGTH args)` by 2656 FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP] 2657 \\ METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND]) 2658 \\ FULL_SIMP_TAC std_ss [iSTEP_ret_state_def] 2659 \\ `BC_SUBSTATE bc7 bc8` by METIS_TAC [iSTEP_BC_SUBSTATE] 2660 \\ `BC_SUBSTATE bc0 bc8` by BC_SUBSTATE_TAC 2661 \\ `bc8.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2662 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2663 \\ Q.EXISTS_TAC `(Val (LENGTH args) :: (REVERSE (Sym fname::args) ++ stack),p + iLENGTH bc.instr_length [iCONST_NUM ((LENGTH args))],r::rs,bc7)` 2664 \\ STRIP_TAC THEN1 2665 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2666 \\ MATCH_MP_TAC iSTEP_cases_imp 2667 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2668 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2669 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code]) 2670 \\ FULL_SIMP_TAC std_ss [REVERSE_DEF] 2671 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2672 \\ Q.EXISTS_TAC `(Sym fname::(Val (LENGTH args)::(REVERSE args ++ [Sym fname] ++ stack)), 2673 p + iLENGTH bc.instr_length [iCONST_NUM (LENGTH args); iLOAD (SUC(LENGTH args))],r::rs,bc7)` 2674 \\ STRIP_TAC THEN1 2675 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2676 \\ MATCH_MP_TAC iSTEP_cases_imp 2677 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2678 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2679 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code] 2680 \\ FULL_SIMP_TAC std_ss [EL,TL,GSYM APPEND_ASSOC,APPEND,LENGTH_APPEND, 2681 LENGTH_REVERSE,LENGTH] \\ ONCE_REWRITE_TAC [GSYM LENGTH_REVERSE] 2682 \\ SIMP_TAC std_ss [RW [LESS_EQ_REFL] (Q.SPECL [`xs`,`LENGTH xs`] 2683 rich_listTheory.EL_APPEND2),EL,HD] \\ DECIDE_TAC) 2684 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2685 \\ Q.EXISTS_TAC `(REVERSE args ++ [Sym fname] ++ stack,p', 2686 p + iLENGTH bc.instr_length 2687 [iCONST_NUM (LENGTH args); iLOAD (SUC (LENGTH args)); iCALL_SYM]::r::rs,bc7)` 2688 \\ STRIP_TAC THEN1 2689 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2690 \\ MATCH_MP_TAC iSTEP_cases_imp 2691 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2692 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2693 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code] 2694 \\ Q.EXISTS_TAC `fname` \\ FULL_SIMP_TAC (srw_ss()) []) 2695 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2696 \\ Q.EXISTS_TAC `(iSTEP_ret_state (MAP ssVAR (REVERSE params)) 2697 (x,REVERSE args ++ [Sym fname] ++ stack, 2698 p + 2699 iLENGTH bc.instr_length 2700 [iCONST_NUM (LENGTH args); iLOAD (SUC (LENGTH args)); 2701 iCALL_SYM],r::rs,bc8))` \\ ASM_SIMP_TAC std_ss [] 2702 \\ ASM_SIMP_TAC std_ss [iSTEP_ret_state_def] 2703 \\ `DROP (LENGTH (MAP ssVAR (REVERSE params))) 2704 (REVERSE args ++ [Sym fname] ++ stack) = [Sym fname] ++ stack` by 2705 (`(LENGTH (MAP ssVAR (REVERSE params))) = LENGTH (REVERSE args)` by 2706 FULL_SIMP_TAC std_ss [LENGTH_MAP,LENGTH_REVERSE] 2707 \\ METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND,APPEND_ASSOC]) 2708 \\ ASM_SIMP_TAC std_ss [] \\ ASM_SIMP_TAC std_ss [APPEND] 2709 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2710 \\ Q.EXISTS_TAC `(x::stack, 2711 p + iLENGTH bc.instr_length 2712 [iCONST_NUM (LENGTH args); iLOAD (SUC (LENGTH args)); iCALL_SYM; iPOPS 1], 2713 r::rs,bc8)` 2714 \\ STRIP_TAC THEN1 2715 (REPEAT (MATCH_MP_TAC RTC_SINGLE) 2716 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 2717 \\ Q.PAT_X_ASSUM `bc8.instr_length = bc.instr_length` ASSUME_TAC 2718 \\ MATCH_MP_TAC iSTEP_cases_imp 2719 \\ FULL_SIMP_TAC std_ss [bc_inst_type_distinct,bc_inst_type_11,BC_STEP_def, 2720 LENGTH,CONS_11,STACK_INV_lemma,getVal_def,CONTAINS_BYTECODE_def,iLENGTH_def, 2721 iLENGTH_APPEND,iLENGTH_def,AC ADD_ASSOC ADD_COMM,EVAL_DATA_OP_def,BC_PRINT_code] 2722 \\ Q.EXISTS_TAC `[Sym fname]` \\ FULL_SIMP_TAC (srw_ss()) [LENGTH]) 2723 \\ Cases_on `ret` \\ ASM_SIMP_TAC std_ss [BC_return_code_def,RTC_REFL] 2724 \\ MATCH_MP_TAC (SIMP_RULE std_ss [iSTEP_ret_state_def] BC_return_code_thm) 2725 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 2726 \\ Q.PAT_X_ASSUM `bc8.instr_length = bc.instr_length` ASSUME_TAC 2727 \\ `DROP (SUC (LENGTH args)) 2728 (ssTEMP::MAP (\x. ssTEMP) args ++ a') = a'` by 2729 (`LENGTH (ssTEMP::MAP (\x. ssTEMP) (args:SExp list)) = SUC (LENGTH args)` by 2730 FULL_SIMP_TAC std_ss [LENGTH,LENGTH_MAP] 2731 \\ METIS_TAC [rich_listTheory.BUTFIRSTN_LENGTH_APPEND]) 2732 \\ FULL_SIMP_TAC std_ss []) 2733 \\ STRIP_TAC THEN1 2734 (REVERSE (REPEAT STRIP_TAC) 2735 \\ Q.PAT_X_ASSUM `BC_ap zzz xxx szzz` MP_TAC 2736 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2737 \\ ASM_SIMP_TAC std_ss [term_distinct,func_distinct,term_11,func_11,LENGTH_REVERSE,LENGTH]) 2738 \\ STRIP_TAC THEN1 2739 (REVERSE (REPEAT STRIP_TAC) 2740 \\ Q.PAT_X_ASSUM `BC_ap zzz xxx szzz` MP_TAC 2741 \\ ONCE_REWRITE_TAC [BC_ev_cases] \\ SIMP_TAC std_ss [BC_return_def] 2742 \\ ASM_SIMP_TAC std_ss [term_distinct,func_distinct,term_11,func_11,LENGTH_REVERSE,LENGTH] 2743 \\ REPEAT STRIP_TAC 2744 \\ SIMP_TAC std_ss [CONS_11,SUBMAP_REFL, 2745 RW [LENGTH_MAP] (Q.SPEC `MAP f xs` rich_listTheory.BUTFIRSTN_LENGTH_APPEND)] 2746 \\ Q.EXISTS_TAC `bc7` \\ FULL_SIMP_TAC std_ss [iSTEP_ret_state_def] 2747 \\ Cases_on `ret` \\ FULL_SIMP_TAC std_ss [] 2748 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2749 \\ ONCE_REWRITE_TAC [iSTEP_cases] \\ FULL_SIMP_TAC std_ss []) 2750 2751 \\ STRIP_TAC THEN1 2752 (REVERSE (REPEAT STRIP_TAC) 2753 \\ IMP_RES_TAC BC_ev_NOT_RET_LEMMA 2754 \\ FULL_SIMP_TAC std_ss [] \\ Q.EXISTS_TAC `bc7` 2755 \\ ASM_SIMP_TAC std_ss [CONS_11,SUBMAP_REFL] 2756 \\ FULL_SIMP_TAC std_ss [iSTEP_ret_state_def] 2757 \\ Cases_on `ret` \\ FULL_SIMP_TAC std_ss [] 2758 \\ REPEAT (MATCH_MP_TAC RTC_SINGLE) 2759 \\ ONCE_REWRITE_TAC [iSTEP_cases] \\ FULL_SIMP_TAC std_ss []) 2760 2761 \\ STRIP_TAC THEN1 2762 (ONCE_REWRITE_TAC [BC_ev_cases] 2763 \\ SIMP_TAC std_ss [NOT_CONS_NIL,CONS_11,MAP,APPEND,LENGTH, 2764 CONTAINS_BYTECODE_def,RTC_REFL,REVERSE_DEF,iLENGTH_def,SUBMAP_REFL] 2765 \\ METIS_TAC [RTC_REFL]) 2766 \\ STRIP_TAC THEN1 2767 (REPEAT STRIP_TAC 2768 \\ Q.PAT_X_ASSUM `BC_evl (e::el,xxx) yyy` MP_TAC 2769 \\ ONCE_REWRITE_TAC [BC_ev_cases] 2770 \\ SIMP_TAC std_ss [NOT_CONS_NIL,CONS_11,MAP,APPEND,LENGTH, 2771 CONTAINS_BYTECODE_def,RTC_REFL] \\ REPEAT STRIP_TAC 2772 \\ FULL_SIMP_TAC std_ss [CONTAINS_BYTECODE_APPEND] 2773 \\ Q.PAT_X_ASSUM `!env. bbb` MP_TAC 2774 \\ Q.PAT_X_ASSUM `!env. bbb` (MP_TAC o 2775 Q.SPECL [`a'`,`code'`,`a2'`,`stack`,`p`,`r`,`rs`,`F`,`q2`,`bc`,`bc2`,`bc7`]) 2776 \\ `BC_SUBSTATE bc2 bc7` by BC_SUBSTATE_TAC 2777 \\ ASM_SIMP_TAC std_ss [] \\ REPEAT STRIP_TAC 2778 \\ Q.PAT_X_ASSUM `!env. bbb` (MP_TAC o 2779 Q.SPECL [`a2'`,`code2`,`a2`,`s::stack`,`p+iLENGTH bc.instr_length (code')`,`r`,`rs`,`p2`,`bc2`,`bc0`,`bc8`]) 2780 \\ MATCH_MP_TAC IMP_IMP \\ STRIP_TAC THEN1 2781 (IMP_RES_TAC BC_ev_LENGTH \\ FULL_SIMP_TAC std_ss [STACK_INV_lemma] 2782 \\ `BC_SUBSTATE bc7 bc8` by BC_SUBSTATE_TAC 2783 \\ IMP_RES_TAC BC_SUBSTATE_BYTECODE 2784 \\ `bc7.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2785 \\ FULL_SIMP_TAC std_ss [] 2786 \\ IMP_RES_TAC BC_SUBSTATE_TRANS) 2787 \\ REPEAT STRIP_TAC 2788 \\ Q.EXISTS_TAC `bc8'` \\ ASM_SIMP_TAC std_ss [REVERSE_DEF] 2789 \\ SIMP_TAC std_ss [MAP_APPEND,MAP,GSYM APPEND_ASSOC,APPEND] 2790 \\ IMP_RES_TAC SUBMAP_TRANS \\ ASM_SIMP_TAC std_ss [] 2791 \\ `BC_SUBSTATE bc bc2` by IMP_RES_TAC BC_ev_LENGTH 2792 \\ `bc2.instr_length = bc.instr_length` by FULL_SIMP_TAC std_ss [BC_SUBSTATE_def] 2793 \\ ONCE_REWRITE_TAC [RTC_CASES_RTC_TWICE] 2794 \\ Q.EXISTS_TAC `(s::stack,p + iLENGTH bc.instr_length code',r::rs,bc8)` 2795 \\ FULL_SIMP_TAC std_ss [REVERSE_DEF,GSYM APPEND_ASSOC,APPEND, 2796 iLENGTH_APPEND,AC ADD_COMM ADD_ASSOC,MAP_APPEND,MAP]) 2797 (* deal with all macros with a single tactic *) 2798 \\ REPEAT STRIP_TAC THEN 2799 (REPEAT STRIP_TAC 2800 \\ Q.PAT_X_ASSUM `BC_ev ret xxx yyy` MP_TAC 2801 \\ ONCE_REWRITE_TAC [BC_ev_cases] 2802 \\ ASM_SIMP_TAC std_ss [term_distinct,term_11,NOT_CONS_NIL,CONS_11] 2803 \\ METIS_TAC [])); 2804 2805val BC_ev_thm = BC_ev_lemma 2806 |> CONJUNCTS |> el 3 |> SPEC_ALL 2807 |> (fn th => MATCH_MP th (R_ev_IMP_RR_ev |> SPEC_ALL |> UNDISCH_ALL)) |> DISCH_ALL 2808 |> SIMP_RULE std_ss [PULL_FORALL_IMP,AND_IMP_INTRO] |> Q.INST [`ret`|->`T`] 2809 |> GEN_ALL |> SIMP_RULE std_ss [iSTEP_ret_state_def] 2810 2811val _ = save_thm("BC_ev_thm",BC_ev_thm); 2812 2813 2814(* translation: term2sexp *) 2815 2816val prim2sym_def = Define ` 2817 (prim2sym opCONS = "CONS") /\ 2818 (prim2sym opEQUAL = "EQUAL") /\ 2819 (prim2sym opLESS = "<") /\ 2820 (prim2sym opSYMBOL_LESS = "SYMBOL-<") /\ 2821 (prim2sym opADD = "+") /\ 2822 (prim2sym opSUB = "-") /\ 2823 (prim2sym opCONSP = "CONSP") /\ 2824 (prim2sym opNATP = "NATP") /\ 2825 (prim2sym opSYMBOLP = "SYMBOLP") /\ 2826 (prim2sym opCAR = "CAR") /\ 2827 (prim2sym opCDR = "CDR")`; 2828 2829val macro_names_def = Define ` 2830 macro_names = 2831 ["LET";"LET*";"COND";"AND";"FIRST";"SECOND"; 2832 "THIRD";"FOURTH";"FIFTH";"LIST";"DEFUN"]`; 2833 2834val reserved_names_def = Define ` 2835 reserved_names = 2836 ["QUOTE";"IF";"OR";"DEFINE";"PRINT";"ERROR";"FUNCALL"; 2837 "CAR";"CDR";"SYMBOLP";"NATP";"CONSP";"+";"-"; 2838 "SYMBOL-<";"<";"EQUAL";"CONS"] ++ macro_names`; 2839 2840val func2sexp_def = Define ` 2841 (func2sexp (PrimitiveFun p) = [Sym (prim2sym p)]) /\ 2842 (func2sexp (Define) = [Sym "DEFINE"]) /\ 2843 (func2sexp (Print) = [Sym "PRINT"]) /\ 2844 (func2sexp (Error) = [Sym "ERROR"]) /\ 2845 (func2sexp (Funcall) = [Sym "FUNCALL"]) /\ 2846 (func2sexp (Fun f) = 2847 if MEM f reserved_names then [Val 0; Sym f] else [Sym f])`; 2848 2849val term2sexp_def = tDefine "term2sexp" ` 2850 (term2sexp (Const s) = list2sexp [Sym "QUOTE"; s]) /\ 2851 (term2sexp (Var v) = Sym v) /\ 2852 (term2sexp (App fc vs) = list2sexp (func2sexp fc ++ MAP term2sexp vs)) /\ 2853 (term2sexp (If x y z) = list2sexp [Sym "IF"; term2sexp x; term2sexp y; term2sexp z]) /\ 2854 (term2sexp (LamApp xs z ys) = list2sexp (list2sexp [Sym "LAMBDA"; list2sexp (MAP Sym xs); term2sexp z]::MAP term2sexp ys)) /\ 2855 (term2sexp (Let zs x) = list2sexp [Sym "LET"; list2sexp (MAP (\x. list2sexp [Sym (FST x); term2sexp (SND x)]) zs); term2sexp x]) /\ 2856 (term2sexp (LetStar zs x) = list2sexp [Sym "LET*"; list2sexp (MAP (\x. list2sexp [Sym (FST x); term2sexp (SND x)]) zs); term2sexp x]) /\ 2857 (term2sexp (Cond qs) = list2sexp (Sym "COND":: (MAP (\x. list2sexp [term2sexp (FST x); term2sexp (SND x)]) qs))) /\ 2858 (term2sexp (Or ts) = list2sexp (Sym "OR"::MAP term2sexp ts)) /\ 2859 (term2sexp (And ts) = list2sexp (Sym "AND"::MAP term2sexp ts)) /\ 2860 (term2sexp (List ts) = list2sexp (Sym "LIST"::MAP term2sexp ts)) /\ 2861 (term2sexp (First x) = list2sexp [Sym "FIRST"; term2sexp x]) /\ 2862 (term2sexp (Second x) = list2sexp [Sym "SECOND"; term2sexp x]) /\ 2863 (term2sexp (Third x) = list2sexp [Sym "THIRD"; term2sexp x]) /\ 2864 (term2sexp (Fourth x) = list2sexp [Sym "FOURTH"; term2sexp x]) /\ 2865 (term2sexp (Fifth x) = list2sexp [Sym "FIFTH"; term2sexp x]) /\ 2866 (term2sexp (Defun fname ps s) = list2sexp [Sym "DEFUN"; Sym fname; list2sexp (MAP Sym ps); s])` 2867 (WF_REL_TAC `measure (term_size)` \\ SRW_TAC [] [] 2868 THEN1 (Induct_on `vs` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2869 THEN1 DECIDE_TAC 2870 THEN1 DECIDE_TAC 2871 THEN1 (Induct_on `qs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2872 THEN1 (Induct_on `qs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2873 THEN1 DECIDE_TAC 2874 THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2875 THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2876 THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2877 THEN1 (Induct_on `ys` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2878 THEN1 (Induct_on `zs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2879 THEN1 (Induct_on `zs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2880 \\ DECIDE_TAC); 2881 2882val fun_name_ok_def = Define ` 2883 (fun_name_ok (Fun f) = ~MEM f reserved_names) /\ 2884 (fun_name_ok _ = T)`; 2885 2886val no_bad_names_def = tDefine "no_bad_names" ` 2887 (no_bad_names (Const s) = T) /\ 2888 (no_bad_names (Var v) = ~(v = "T") /\ ~(v = "NIL")) /\ 2889 (no_bad_names (App fc vs) = fun_name_ok fc /\ EVERY no_bad_names vs) /\ 2890 (no_bad_names (If x y z) = no_bad_names x /\ no_bad_names y /\ no_bad_names z) /\ 2891 (no_bad_names (LamApp xs z ys) = no_bad_names z /\ EVERY no_bad_names ys) /\ 2892 (no_bad_names (Let zs x) = EVERY (\x. no_bad_names (SND x)) zs /\ no_bad_names x) /\ 2893 (no_bad_names (LetStar zs x) = EVERY (\x. no_bad_names (SND x)) zs /\ no_bad_names x) /\ 2894 (no_bad_names (Cond qs) = EVERY (\x. no_bad_names (FST x) /\ no_bad_names (SND x)) qs) /\ 2895 (no_bad_names (Or ts) = EVERY no_bad_names ts) /\ 2896 (no_bad_names (And ts) = EVERY no_bad_names ts) /\ 2897 (no_bad_names (List ts) = EVERY no_bad_names ts) /\ 2898 (no_bad_names (First x) = no_bad_names x) /\ 2899 (no_bad_names (Second x) = no_bad_names x) /\ 2900 (no_bad_names (Third x) = no_bad_names x) /\ 2901 (no_bad_names (Fourth x) = no_bad_names x) /\ 2902 (no_bad_names (Fifth x) = no_bad_names x) /\ 2903 (no_bad_names (Defun fname ps s) = T)` 2904 (WF_REL_TAC `measure (term_size)` \\ SRW_TAC [] [] 2905 THEN1 (Induct_on `vs` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2906 THEN1 DECIDE_TAC 2907 THEN1 DECIDE_TAC 2908 THEN1 (Induct_on `qs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2909 THEN1 (Induct_on `qs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2910 THEN1 DECIDE_TAC 2911 THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2912 THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2913 THEN1 (Induct_on `ts` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2914 THEN1 (Induct_on `ys` \\ SRW_TAC [] [MEM,term_size_def] \\ RES_TAC \\ DECIDE_TAC) 2915 THEN1 (Induct_on `zs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2916 THEN1 (Induct_on `zs` \\ NTAC 2 (SRW_TAC [] [MEM,term_size_def]) \\ RES_TAC \\ DECIDE_TAC) 2917 \\ DECIDE_TAC); 2918 2919val sexp2list_list2sexp = prove( 2920 ``!x. sexp2list (list2sexp x) = x``, 2921 Induct \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss []); 2922 2923val MAP_EQ_IMP = prove( 2924 ``!xs f. (!x. MEM x xs ==> (f x = x)) ==> (MAP f xs = xs)``, 2925 Induct \\ SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC \\ METIS_TAC []); 2926 2927val sexp2term_term2sexp = store_thm("sexp2term_term2sexp", 2928 ``!t. no_bad_names t ==> (sexp2term (term2sexp t) = t)``, 2929 HO_MATCH_MP_TAC (fetch "-" "term2sexp_ind") \\ REPEAT STRIP_TAC 2930 \\ FULL_SIMP_TAC std_ss [no_bad_names_def] 2931 THEN1 (EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 2932 THEN1 (EVAL_TAC \\ FULL_SIMP_TAC std_ss []) 2933 THEN1 2934 (SIMP_TAC (srw_ss()) [term2sexp_def,LET_DEF] 2935 \\ Cases_on `fc` THEN TRY 2936 (ASM_SIMP_TAC (srw_ss()) [func2sexp_def,list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def] 2937 \\ SIMP_TAC (srw_ss()) [Once sexp2term_def,LET_DEF] \\ TRY (Cases_on `l`) 2938 \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def, 2939 getSym_def,prim2sym_def,sym2prim_def,sexp2list_list2sexp, 2940 MAP_MAP_o,combinTheory.o_DEF,fun_name_ok_def] 2941 \\ MATCH_MP_TAC MAP_EQ_IMP \\ FULL_SIMP_TAC std_ss [EVERY_MEM] \\ NO_TAC) 2942 \\ FULL_SIMP_TAC (srw_ss()) [func2sexp_def,fun_name_ok_def] 2943 \\ FULL_SIMP_TAC (srw_ss()) [reserved_names_def,MEM,APPEND,macro_names_def] 2944 \\ SIMP_TAC (srw_ss()) [Once sexp2term_def,LET_DEF] 2945 \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def, 2946 getSym_def,prim2sym_def,sym2prim_def,sexp2list_list2sexp, 2947 MAP_MAP_o,combinTheory.o_DEF] 2948 \\ MATCH_MP_TAC MAP_EQ_IMP \\ FULL_SIMP_TAC std_ss [EVERY_MEM]) 2949 THEN1 2950 (SIMP_TAC (srw_ss()) [term2sexp_def,Once sexp2term_def,LET_DEF] 2951 \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def]) 2952 THEN 2953 (SIMP_TAC (srw_ss()) [term2sexp_def,Once sexp2term_def,LET_DEF] 2954 \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,CAR_def,CDR_def,isVal_def,isSym_def, 2955 getSym_def,sym2prim_def,sexp2list_list2sexp,MAP_MAP_o,combinTheory.o_DEF] 2956 \\ MATCH_MP_TAC MAP_EQ_IMP \\ FULL_SIMP_TAC std_ss [EVERY_MEM])); 2957 2958val verified_string_def = Define ` 2959 verified_string xs = 2960 if ~ALL_DISTINCT (MAP FST xs) then NONE else 2961 if ~EVERY (\(name,params,body). no_bad_names body) xs then NONE else 2962 SOME (FLAT (MAP ( \ (name,params,body). sexp2string 2963 (list2sexp [Sym "DEFUN"; Sym name; 2964 list2sexp (MAP Sym params); term2sexp body]) ++ "\n") xs))` 2965 2966 2967(* translation sexp2sexp *) 2968 2969val sfix_def = Define `sfix x = Sym (getSym x)`; 2970 2971val IMP_isDot = prove( 2972 ``!x. ~(isVal x) /\ ~(isSym x) ==> isDot x``, 2973 Cases THEN EVAL_TAC); 2974 2975val LSIZE_CAR_LESS = prove( 2976 ``!x. LSIZE x < SUC n ==> LSIZE (CAR x) < SUC n``, 2977 Cases \\ FULL_SIMP_TAC std_ss [LSIZE_def,CAR_def,CDR_def] \\ DECIDE_TAC); 2978 2979val LSIZE_CDR_LESS = prove( 2980 ``!x. LSIZE x < SUC n ==> LSIZE (CDR x) < SUC n``, 2981 Cases \\ FULL_SIMP_TAC std_ss [LSIZE_def,CAR_def,CDR_def] \\ DECIDE_TAC); 2982 2983val MEM_sexp2list = prove( 2984 ``!a x. MEM x (sexp2list a) ==> LSIZE x < LSIZE a``, 2985 Induct \\ SIMP_TAC std_ss [sexp2list_def,MEM] \\ REPEAT STRIP_TAC 2986 \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ RES_TAC \\ DECIDE_TAC); 2987 2988val sexp2sexp_def = tDefine "sexp2sexp" ` 2989 sexp2sexp x = 2990 if x = Sym "T" then list2sexp [Sym "QUOTE"; x] else 2991 if x = Sym "NIL" then list2sexp [Sym "QUOTE"; x] else 2992 if isVal x then list2sexp [Sym "QUOTE"; x] else 2993 if isSym x then x else 2994 let x1 = CAR x in 2995 let x2 = CAR (CDR x) in 2996 let x3 = CAR (CDR (CDR x)) in 2997 let x4 = CAR (CDR (CDR (CDR x))) in 2998 let xs = list2sexp (MAP sexp2sexp (sexp2list (CDR x))) in 2999 if x1 = Sym "QUOTE" then list2sexp [Sym "QUOTE"; x2] else 3000 if x1 = Sym "IF" then 3001 list2sexp [Sym "IF"; sexp2sexp x2; sexp2sexp x3; sexp2sexp x4] else 3002 if x1 = Sym "FIRST" then list2sexp [x1; sexp2sexp x2] else 3003 if x1 = Sym "SECOND" then list2sexp [x1; sexp2sexp x2] else 3004 if x1 = Sym "THIRD" then list2sexp [x1; sexp2sexp x2] else 3005 if x1 = Sym "FOURTH" then list2sexp [x1; sexp2sexp x2] else 3006 if x1 = Sym "FIFTH" then list2sexp [x1; sexp2sexp x2] else 3007 if x1 = Sym "DEFUN" then 3008 list2sexp [Sym "DEFUN"; sfix x2; 3009 list2sexp (MAP sfix (sexp2list x3)); x4] else 3010 if CAR x1 = Sym "LAMBDA" then 3011 let y2 = CAR (CDR x1) in 3012 let y3 = CAR (CDR (CDR x1)) in 3013 Dot (list2sexp [Sym "LAMBDA"; 3014 list2sexp (MAP sfix (sexp2list y2)); 3015 sexp2sexp y3]) xs else 3016 if x1 = Sym "COND" then 3017 Dot (Sym "COND") (list2sexp (MAP 3018 (\x. list2sexp [sexp2sexp (CAR x); sexp2sexp (CAR (CDR x))]) 3019 (sexp2list (CDR x)))) else 3020 if x1 = Sym "LET" then 3021 list2sexp [x1; list2sexp (MAP 3022 (\x. list2sexp [sfix (CAR x); sexp2sexp (CAR (CDR x))]) 3023 (sexp2list x2)); sexp2sexp x3] else 3024 if x1 = Sym "LET*" then 3025 list2sexp [x1; list2sexp (MAP 3026 (\x. list2sexp [sfix (CAR x); sexp2sexp (CAR (CDR x))]) 3027 (sexp2list x2)); sexp2sexp x3] 3028 else 3029 Dot (sfix x1) xs` 3030 (WF_REL_TAC `measure LSIZE` \\ REPEAT STRIP_TAC \\ IMP_RES_TAC IMP_isDot 3031 \\ FULL_SIMP_TAC std_ss [isDot_thm,CAR_def,CDR_def,LSIZE_def] 3032 \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def,LSIZE_def] 3033 \\ IMP_RES_TAC MEM_sexp2list 3034 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3035 \\ REPEAT DECIDE_TAC 3036 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def,LSIZE_def] 3037 \\ DECIDE_TAC); 3038 3039val PULL_FORALL_IMP = METIS_PROVE [] ``(p ==> !x. q x) = !x. p ==> q x``; 3040 3041val list2sexp_11 = prove( 3042 ``!xs ys. (list2sexp xs = list2sexp ys) = (xs = ys)``, 3043 Induct \\ Cases_on `ys` \\ FULL_SIMP_TAC (srw_ss()) [list2sexp_def]); 3044 3045val MAP_sfix = prove( 3046 ``!xs. MAP sfix xs = MAP Sym (MAP getSym xs)``, 3047 Induct \\ FULL_SIMP_TAC std_ss [MAP,sfix_def]); 3048 3049val sexp2sexp_thm = store_thm("sexp2sexp_thm", 3050 ``!x. sexp2sexp x = term2sexp (sexp2term x)``, 3051 REPEAT STRIP_TAC \\ completeInduct_on `LSIZE x` \\ REPEAT STRIP_TAC 3052 \\ FULL_SIMP_TAC std_ss [PULL_FORALL_IMP] 3053 \\ ONCE_REWRITE_TAC [sexp2sexp_def] 3054 \\ Cases_on `x = Sym "T"` \\ ASM_SIMP_TAC std_ss [] THEN1 EVAL_TAC 3055 \\ Cases_on `x = Sym "NIL"` \\ ASM_SIMP_TAC std_ss [] THEN1 EVAL_TAC 3056 \\ Cases_on `isVal x` \\ ASM_SIMP_TAC std_ss [] 3057 THEN1 (ASM_SIMP_TAC std_ss [Once sexp2term_def,term2sexp_def]) 3058 \\ Cases_on `isSym x` \\ ASM_SIMP_TAC std_ss [] 3059 THEN1 (ASM_SIMP_TAC std_ss [Once sexp2term_def,term2sexp_def] 3060 \\ FULL_SIMP_TAC std_ss [isSym_thm,getSym_def]) 3061 \\ ONCE_REWRITE_TAC [sexp2term_def] 3062 \\ FULL_SIMP_TAC std_ss [LET_DEF] \\ IMP_RES_TAC IMP_isDot 3063 \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def,isDot_thm] 3064 \\ FULL_SIMP_TAC std_ss [CAR_def,CDR_def,isDot_thm] 3065 \\ Cases_on `a = Sym "QUOTE"` \\ ASM_SIMP_TAC std_ss [] THEN1 EVAL_TAC 3066 \\ Cases_on `a = Sym "IF"` \\ ASM_SIMP_TAC std_ss [] THEN1 3067 (SIMP_TAC (srw_ss()) [term2sexp_def,list2sexp_11] \\ REPEAT STRIP_TAC 3068 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 3069 \\ FULL_SIMP_TAC std_ss [LSIZE_def] 3070 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3071 \\ DECIDE_TAC) 3072 \\ `MAP (\a. sexp2sexp a) (sexp2list b) = 3073 MAP (\a. term2sexp a) (MAP (\a. sexp2term a) (sexp2list b))` by 3074 (FULL_SIMP_TAC std_ss [LSIZE_def] \\ Q.PAT_X_ASSUM `!x.bb` MP_TAC 3075 \\ Q.SPEC_TAC (`b`,`b`) \\ REVERSE Induct 3076 THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) 3077 THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) 3078 \\ REPEAT STRIP_TAC \\ FULL_SIMP_TAC std_ss [sexp2list_def,MAP,CONS_11] 3079 \\ REPEAT STRIP_TAC THEN1 (POP_ASSUM MATCH_MP_TAC \\ EVAL_TAC \\ DECIDE_TAC) 3080 \\ Q.PAT_X_ASSUM `(!x.bbb) ==> ccc` MATCH_MP_TAC \\ REPEAT STRIP_TAC 3081 \\ Q.PAT_X_ASSUM `(!x.bbb)` MATCH_MP_TAC \\ REPEAT STRIP_TAC 3082 \\ EVAL_TAC \\ DECIDE_TAC) 3083 \\ REVERSE (Cases_on `sym2prim (getSym a) = NONE`) 3084 \\ ASM_SIMP_TAC std_ss [] THEN1 3085 (CCONTR_TAC \\ Q.PAT_X_ASSUM `sym2prim (getSym a) <> NONE` MP_TAC 3086 \\ FULL_SIMP_TAC std_ss [sym2prim_def] \\ SRW_TAC [] [] \\ Cases_on `a` 3087 \\ FULL_SIMP_TAC (srw_ss()) [getSym_def,CAR_def,term2sexp_def,func2sexp_def, 3088 list2sexp_def,prim2sym_def,sfix_def]) 3089 \\ Cases_on `MEM a [Sym "FIRST";Sym "SECOND";Sym "THIRD";Sym "FOURTH";Sym "FIFTH"]` 3090 \\ ASM_SIMP_TAC std_ss [] THEN1 3091 (FULL_SIMP_TAC std_ss [MEM] 3092 \\ SIMP_TAC (srw_ss()) [term2sexp_def,list2sexp_11,CONS_11] 3093 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ SIMP_TAC std_ss [LSIZE_def] 3094 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS) \\ DECIDE_TAC) 3095 \\ FULL_SIMP_TAC std_ss [MEM] 3096 \\ Cases_on `a = Sym "OR"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] 3097 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,getSym_def,sfix_def] 3098 \\ Cases_on `a = Sym "AND"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] 3099 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,getSym_def,sfix_def] 3100 \\ Cases_on `a = Sym "LIST"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] 3101 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,getSym_def,sfix_def] 3102 \\ Cases_on `a = Sym "DEFINE"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def,getSym_def,sfix_def] 3103 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,func2sexp_def,APPEND,getSym_def,sfix_def] 3104 \\ Cases_on `a = Sym "PRINT"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] 3105 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,func2sexp_def,APPEND,getSym_def,sfix_def] 3106 \\ Cases_on `a = Sym "ERROR"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] 3107 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,func2sexp_def,APPEND,getSym_def,sfix_def] 3108 \\ Cases_on `a = Sym "FUNCALL"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] 3109 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,func2sexp_def,APPEND,getSym_def,sfix_def] 3110 \\ Cases_on `a = Sym "DEFUN"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] 3111 \\ FULL_SIMP_TAC std_ss [term2sexp_def,list2sexp_def,func2sexp_def,APPEND,getSym_def,sfix_def] 3112 \\ FULL_SIMP_TAC std_ss [sfix_def,MAP_sfix] 3113 \\ Cases_on `a = Sym "COND"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] THEN1 3114 (FULL_SIMP_TAC (srw_ss()) [term2sexp_def,list2sexp_def,list2sexp_11,LSIZE_def] 3115 \\ Q.PAT_X_ASSUM `!x.bbb` MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 3116 \\ REVERSE (Induct_on `b`) 3117 THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) 3118 \\ SIMP_TAC std_ss [sexp2list_def,MAP,CONS_11] \\ REPEAT STRIP_TAC THEN1 3119 (FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 3120 \\ POP_ASSUM MATCH_MP_TAC 3121 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3122 \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3123 \\ Q.PAT_X_ASSUM `(!x.bbb) ==> ccc` MATCH_MP_TAC \\ REPEAT STRIP_TAC 3124 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ SIMP_TAC std_ss [LSIZE_def] 3125 \\ DECIDE_TAC) 3126 \\ Cases_on `a = Sym "LET"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] THEN1 3127 (FULL_SIMP_TAC (srw_ss()) [term2sexp_def,list2sexp_def,list2sexp_11,LSIZE_def] 3128 \\ REVERSE (REPEAT STRIP_TAC) THEN1 3129 (Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 3130 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3131 \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3132 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [sexp2list_def,CAR_def,MAP,LSIZE_def] 3133 \\ Q.PAT_X_ASSUM `!x.bbb` MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 3134 \\ REVERSE (Induct_on `S'`) 3135 THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) 3136 \\ SIMP_TAC std_ss [sexp2list_def,MAP,CONS_11] \\ REPEAT STRIP_TAC THEN1 3137 (FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 3138 \\ POP_ASSUM MATCH_MP_TAC 3139 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3140 \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3141 \\ Q.PAT_X_ASSUM `(!x.bbb) ==> ccc` MATCH_MP_TAC \\ REPEAT STRIP_TAC 3142 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3143 \\ Cases_on `a = Sym "LET*"` \\ FULL_SIMP_TAC (srw_ss()) [CAR_def] THEN1 3144 (FULL_SIMP_TAC (srw_ss()) [term2sexp_def,list2sexp_def,list2sexp_11,LSIZE_def] 3145 \\ REVERSE (REPEAT STRIP_TAC) THEN1 3146 (Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC 3147 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3148 \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3149 \\ Cases_on `b` \\ FULL_SIMP_TAC std_ss [sexp2list_def,CAR_def,MAP,LSIZE_def] 3150 \\ Q.PAT_X_ASSUM `!x.bbb` MP_TAC \\ REPEAT (POP_ASSUM (K ALL_TAC)) 3151 \\ REVERSE (Induct_on `S'`) 3152 THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) THEN1 (EVAL_TAC \\ SIMP_TAC std_ss []) 3153 \\ SIMP_TAC std_ss [sexp2list_def,MAP,CONS_11] \\ REPEAT STRIP_TAC THEN1 3154 (FULL_SIMP_TAC (srw_ss()) [] \\ REPEAT STRIP_TAC 3155 \\ POP_ASSUM MATCH_MP_TAC 3156 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3157 \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3158 \\ Q.PAT_X_ASSUM `(!x.bbb) ==> ccc` MATCH_MP_TAC \\ REPEAT STRIP_TAC 3159 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3160 \\ Cases_on `CAR a = Sym "LAMBDA"` \\ FULL_SIMP_TAC std_ss [] THEN1 3161 (SIMP_TAC (srw_ss()) [term2sexp_def,list2sexp_def] 3162 \\ Q.PAT_X_ASSUM `!x.bbb` MATCH_MP_TAC \\ SIMP_TAC std_ss [LSIZE_def] 3163 \\ REPEAT (MATCH_MP_TAC LSIZE_CAR_LESS ORELSE MATCH_MP_TAC LSIZE_CDR_LESS) 3164 \\ FULL_SIMP_TAC std_ss [LSIZE_def] \\ DECIDE_TAC) 3165 \\ FULL_SIMP_TAC std_ss [term2sexp_def,func2sexp_def,APPEND,list2sexp_def,sfix_def] 3166 \\ sg `~MEM (getSym a) reserved_names` 3167 \\ FULL_SIMP_TAC std_ss [term2sexp_def,func2sexp_def,APPEND,list2sexp_def,sfix_def] 3168 \\ Cases_on `a` THEN1 EVAL_TAC THEN1 EVAL_TAC 3169 \\ FULL_SIMP_TAC std_ss [getSym_def] 3170 \\ EVAL_TAC \\ FULL_SIMP_TAC (srw_ss()) [] 3171 \\ CCONTR_TAC \\ FULL_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC (srw_ss()) [sym2prim_def]); 3172 3173(* 3174 3175(* bytecode deterministic *) 3176 3177val LENGTH_APPEND_EQ_IMP = prove( 3178 ``!xs1 xs2 ys1 ys2. 3179 (LENGTH xs1 = LENGTH xs2) ==> 3180 ((xs1 ++ ys1 = xs2 ++ ys2) ==> (xs1 = xs2) /\ (ys1 = ys2))``, 3181 Induct \\ Cases_on `xs2` 3182 \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,APPEND,CONS_11] \\ METIS_TAC []); 3183 3184val LENGTH_REVERSE_APPEND_EQ_IMP = prove( 3185 ``!xs1 xs2 ys1 ys2. 3186 (LENGTH xs1 = LENGTH xs2) /\ (REVERSE xs1 ++ ys1 = REVERSE xs2 ++ ys2) ==> 3187 (xs1 = xs2) /\ (ys1 = ys2)``, 3188 Induct \\ Cases_on `xs2` 3189 \\ ASM_SIMP_TAC std_ss [LENGTH,ADD1,APPEND,CONS_11,REVERSE_DEF] 3190 \\ ASM_SIMP_TAC std_ss [GSYM APPEND_ASSOC,APPEND] \\ NTAC 4 STRIP_TAC 3191 \\ RES_TAC \\ FULL_SIMP_TAC std_ss [CONS_11]); 3192 3193val list2sexp_MAP_Sym_11 = prove( 3194 ``!xs ys. (list2sexp (MAP Sym xs) = list2sexp (MAP Sym ys)) ==> (xs = ys)``, 3195 Induct \\ Cases_on `ys` \\ ASM_SIMP_TAC (srw_ss()) [list2sexp_def,MAP]); 3196 3197val iSTEP_DETERMINISTIC = store_thm("iSTEP_DETERMINISTIC", 3198 ``!x y1 y2. iSTEP x y1 /\ iSTEP x y2 ==> (y1 = y2)``, 3199 ONCVE_REWRITE_TAC [iSTEP_cases] \\ REPEAT STRIP_TAC 3200 \\ REPEAT (Q.PAT_X_ASSUM `CONTAINS_BYTECODE xx yy zz` MP_TAC) 3201 \\ FULL_SIMP_TAC (srw_ss()) [CONS_11,CONTAINS_BYTECODE_def] 3202 \\ REPEAT STRIP_TAC THEN1 METIS_TAC [LENGTH_APPEND_EQ_IMP] 3203 \\ FULL_SIMP_TAC std_ss [] 3204 \\ IMP_RES_TAC LENGTH_REVERSE_APPEND_EQ_IMP \\ FULL_SIMP_TAC std_ss [] 3205 \\ Q.PAT_X_ASSUM `fc' = fc` (fn th => FULL_SIMP_TAC std_ss [th]) 3206 \\ Q.PAT_X_ASSUM `bc' = bc` (fn th => FULL_SIMP_TAC std_ss [th]) 3207 \\ REPEAT (Q.PAT_X_ASSUM `BC_COMPILE xxx = yyy` MP_TAC) 3208 \\ IMP_RES_TAC list2sexp_MAP_Sym_11 \\ FULL_SIMP_TAC std_ss []); 3209 3210*) 3211 3212val _ = export_theory(); 3213