1 2open HolKernel boolLib bossLib Parse; 3open pred_setTheory set_sepTheory progTheory listTheory pairTheory 4open combinTheory addressTheory sexpTheory imported_acl2Theory; 5open complex_rationalTheory hol_defaxiomsTheory arithmeticTheory; 6 7val _ = new_theory "m1_prog"; 8 9 10infix \\ 11val op \\ = op THEN; 12 13val RW = REWRITE_RULE; 14val RW1 = ONCE_REWRITE_RULE; 15 16 17 18(* ----------------------------------------------------------------------------- *) 19(* The M1_ set *) 20(* ----------------------------------------------------------------------------- *) 21 22val _ = Hol_datatype ` 23 m1_el = tPC of sexp 24 | tLocal of num => sexp 25 | tStack of sexp 26 | tInstr of sexp => sexp 27 | tOK of bool`; 28 29val m1_el_11 = DB.fetch "-" "m1_el_11"; 30val m1_el_distinct = DB.fetch "-" "m1_el_distinct"; 31 32val _ = Parse.type_abbrev("m1_set",``:m1_el set``); 33 34 35(* ----------------------------------------------------------------------------- *) 36(* Converting from m1_state to m1_set *) 37(* ----------------------------------------------------------------------------- *) 38 39val instr_def = Define `instr a s = nth a (program s)`; 40val nth_local_def = Define `nth_local a s = nth (nat a) (locals s)`; 41val m1_ok_def = Define `m1_ok s = ?x1 x2 x3 x4. s = make_state x1 x2 x3 x4`; 42 43val m1_2set'_def = Define ` 44 m1_2set' (ps:unit set, ls: num set, ss: unit set, is: sexp set, os: unit set) (s:sexp) = 45 IMAGE (\a. tPC (pc s)) ps UNION 46 IMAGE (\a. tLocal a (nth_local a s)) ls UNION 47 IMAGE (\a. tStack (stack s)) ss UNION 48 IMAGE (\a. tInstr a (instr a s)) is UNION 49 IMAGE (\a. tOK (m1_ok s)) os`; 50 51val m1_2set_def = Define `m1_2set s = m1_2set' (UNIV,UNIV,UNIV,UNIV,UNIV) s`; 52val m1_2set''_def = Define `m1_2set'' x s = m1_2set s DIFF m1_2set' x s`; 53 54(* theorems *) 55 56val m1_2set'_SUBSET_m1_2set = prove( 57 ``!y s. m1_2set' y s SUBSET m1_2set s``, 58 SIMP_TAC std_ss [pairTheory.FORALL_PROD] 59 \\ SIMP_TAC std_ss [SUBSET_DEF,m1_2set'_def,m1_2set_def,IN_IMAGE,IN_UNION,IN_UNIV] 60 \\ METIS_TAC [NOT_IN_EMPTY]); 61 62val SPLIT_m1_2set = prove( 63 ``!x s. SPLIT (m1_2set s) (m1_2set' x s, m1_2set'' x s)``, 64 REPEAT STRIP_TAC 65 \\ ASM_SIMP_TAC std_ss [SPLIT_def,EXTENSION,IN_UNION,IN_DIFF,m1_2set''_def] 66 \\ `m1_2set' x s SUBSET m1_2set s` by METIS_TAC [m1_2set'_SUBSET_m1_2set] 67 \\ SIMP_TAC bool_ss [DISJOINT_DEF,EXTENSION,IN_INTER,NOT_IN_EMPTY,IN_DIFF] 68 \\ METIS_TAC [SUBSET_DEF]); 69 70val SUBSET_m1_2set = prove( 71 ``!u s. u SUBSET m1_2set s = ?y. u = m1_2set' y s``, 72 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC 73 \\ ASM_REWRITE_TAC [m1_2set'_SUBSET_m1_2set] 74 \\ Q.EXISTS_TAC `( 75 { a |a| ?x. tPC x IN u }, 76 { a |a| ?x. tLocal a x IN u }, 77 { a |a| ?x. tStack x IN u }, 78 { a |a| ?x. tInstr a x IN u }, 79 { a |a| ?x. tOK x IN u })` 80 \\ FULL_SIMP_TAC std_ss [m1_2set'_def,m1_2set_def,EXTENSION,SUBSET_DEF,IN_IMAGE, 81 IN_UNION,GSPECIFICATION,IN_INSERT,NOT_IN_EMPTY,IN_UNIV] 82 \\ STRIP_TAC \\ ASM_REWRITE_TAC [] \\ EQ_TAC \\ REPEAT STRIP_TAC THEN1 METIS_TAC [] 83 \\ PAT_ASSUM ``!x:'a. b:bool`` IMP_RES_TAC \\ FULL_SIMP_TAC std_ss [m1_el_11,m1_el_distinct]); 84 85val SPLIT_m1_2set_EXISTS = prove( 86 ``!s u v. SPLIT (m1_2set s) (u,v) = ?y. (u = m1_2set' y s) /\ (v = m1_2set'' y s)``, 87 REPEAT STRIP_TAC \\ EQ_TAC \\ REPEAT STRIP_TAC \\ ASM_REWRITE_TAC [SPLIT_m1_2set] 88 \\ FULL_SIMP_TAC bool_ss [SPLIT_def,m1_2set'_def,m1_2set''_def] 89 \\ `u SUBSET (m1_2set s)` by 90 (FULL_SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_UNION] \\ METIS_TAC []) 91 \\ FULL_SIMP_TAC std_ss [SUBSET_m1_2set] \\ Q.EXISTS_TAC `y` \\ REWRITE_TAC [] 92 \\ FULL_SIMP_TAC std_ss [EXTENSION,IN_DIFF,IN_UNION,DISJOINT_DEF,NOT_IN_EMPTY,IN_INTER] 93 \\ METIS_TAC []); 94 95 96 97val IN_m1_2set = (SIMP_RULE std_ss [oneTheory.one] o prove)(`` 98 (!a x s. tPC x IN (m1_2set s) = (x = pc s)) /\ 99 (!a x s. tPC x IN (m1_2set' (ps,ls,ss,is,os) s) = (x = pc s) /\ a IN ps) /\ 100 (!a x s. tPC x IN (m1_2set'' (ps,ls,ss,is,os) s) = (x = pc s) /\ ~(a IN ps)) /\ 101 (!a x s. tLocal a x IN (m1_2set s) = (x = nth_local a s)) /\ 102 (!a x s. tLocal a x IN (m1_2set' (ps,ls,ss,is,os) s) = (x = nth_local a s) /\ a IN ls) /\ 103 (!a x s. tLocal a x IN (m1_2set'' (ps,ls,ss,is,os) s) = (x = nth_local a s) /\ ~(a IN ls)) /\ 104 (!a x s. tStack x IN (m1_2set s) = (x = stack s)) /\ 105 (!a x s. tStack x IN (m1_2set' (ps,ls,ss,is,os) s) = (x = stack s) /\ a IN ss) /\ 106 (!a x s. tStack x IN (m1_2set'' (ps,ls,ss,is,os) s) = (x = stack s) /\ ~(a IN ss)) /\ 107 (!a x s. tInstr a x IN (m1_2set s) = (x = instr a s)) /\ 108 (!a x s. tInstr a x IN (m1_2set' (ps,ls,ss,is,os) s) = (x = instr a s) /\ a IN is) /\ 109 (!a x s. tInstr a x IN (m1_2set'' (ps,ls,ss,is,os) s) = (x = instr a s) /\ ~(a IN is)) /\ 110 (!a x s. tOK x IN (m1_2set s) = (x = m1_ok s)) /\ 111 (!a x s. tOK x IN (m1_2set' (ps,ls,ss,is,os) s) = (x = m1_ok s) /\ a IN os) /\ 112 (!a x s. tOK x IN (m1_2set'' (ps,ls,ss,is,os) s) = (x = m1_ok s) /\ ~(a IN os))``, 113 SRW_TAC [] [m1_2set'_def,m1_2set''_def,m1_2set_def,IN_UNION,IN_DIFF,oneTheory.one] 114 \\ METIS_TAC []); 115 116val SET_NOT_EQ = prove( 117 ``!x y. ~(x = y:'a set) = ?a. ~(a IN x = a IN y)``, 118 FULL_SIMP_TAC std_ss [EXTENSION]) 119 120val m1_2set''_11 = prove( 121 ``!y y' s s'. (m1_2set'' y' s' = m1_2set'' y s) ==> (y = y')``, 122 REPEAT STRIP_TAC 123 \\ `?ps ls ss is os. y = (ps,ls,ss,is,os)` by METIS_TAC [PAIR] 124 \\ `?ps2 ls2 ss2 is2 os2. y' = (ps2,ls2,ss2,is2,os2)` by METIS_TAC [PAIR] 125 \\ FULL_SIMP_TAC std_ss [] \\ CCONTR_TAC 126 \\ FULL_SIMP_TAC std_ss [EXTENSION] 127 THEN1 (`~((?y. tPC y IN m1_2set'' (ps,ls,ss,is,os) s) = 128 (?y. tPC y IN m1_2set'' (ps2,ls2,ss2,is2,os2) s'))` by 129 FULL_SIMP_TAC std_ss [IN_m1_2set,oneTheory.one] THEN1 METIS_TAC []) 130 THEN1 (`~((?y. tLocal x y IN m1_2set'' (ps,ls,ss,is,os) s) = 131 (?y. tLocal x y IN m1_2set'' (ps2,ls2,ss2,is2,os2) s'))` by 132 FULL_SIMP_TAC std_ss [IN_m1_2set,oneTheory.one] THEN1 METIS_TAC []) 133 THEN1 (`~((?y. tStack y IN m1_2set'' (ps,ls,ss,is,os) s) = 134 (?y. tStack y IN m1_2set'' (ps2,ls2,ss2,is2,os2) s'))` by 135 FULL_SIMP_TAC std_ss [IN_m1_2set,oneTheory.one] THEN1 METIS_TAC []) 136 THEN1 (`~((?y. tInstr x y IN m1_2set'' (ps,ls,ss,is,os) s) = 137 (?y. tInstr x y IN m1_2set'' (ps2,ls2,ss2,is2,os2) s'))` by 138 FULL_SIMP_TAC std_ss [IN_m1_2set,oneTheory.one] THEN1 METIS_TAC []) 139 THEN1 (`~((?y. tOK y IN m1_2set'' (ps,ls,ss,is,os) s) = 140 (?y. tOK y IN m1_2set'' (ps2,ls2,ss2,is2,os2) s'))` by 141 FULL_SIMP_TAC std_ss [IN_m1_2set,oneTheory.one] THEN1 METIS_TAC [])); 142 143val DELETE_m1_2set = (SIMP_RULE std_ss [oneTheory.one] o prove)(`` 144 (!a s. (m1_2set' (ps,ls,ss,is,os) s) DELETE tPC (pc s) = 145 (m1_2set' (ps DELETE a,ls,ss,is,os) s)) /\ 146 (!a s. (m1_2set' (ps,ls,ss,is,os) s) DELETE tLocal a (nth_local a s) = 147 (m1_2set' (ps,ls DELETE a,ss,is,os) s)) /\ 148 (!a s. (m1_2set' (ps,ls,ss,is,os) s) DELETE tStack (stack s) = 149 (m1_2set' (ps,ls,ss DELETE a,is,os) s)) /\ 150 (!a s. (m1_2set' (ps,ls,ss,is,os) s) DELETE tInstr a (instr a s) = 151 (m1_2set' (ps,ls,ss,is DELETE a,os) s)) /\ 152 (!a s. (m1_2set' (ps,ls,ss,is,os) s) DELETE tOK (m1_ok s) = 153 (m1_2set' (ps,ls,ss,is,os DELETE a) s))``, 154 SRW_TAC [] [m1_2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR, 155 EXISTS_OR_THM,IN_DELETE,IN_INSERT,NOT_IN_EMPTY,oneTheory.one] 156 \\ Cases_on `x` \\ SRW_TAC [] [] \\ METIS_TAC []); 157 158val EMPTY_m1_2set = prove(`` 159 (m1_2set' (ps,ls,ss,is,os) s = {}) = 160 (ps = {}) /\ (ls = {}) /\ (ss = {}) /\ (is = {}) /\ (os = {})``, 161 SRW_TAC [] [m1_2set'_def,EXTENSION,IN_UNION,GSPECIFICATION,LEFT_AND_OVER_OR,EXISTS_OR_THM] 162 \\ METIS_TAC []); 163 164 165(* ----------------------------------------------------------------------------- *) 166(* Defining the M1_MODEL *) 167(* ----------------------------------------------------------------------------- *) 168 169val tP_def = Define `tP x = SEP_EQ {tPC x}`; 170val tS_def = Define `tS x = SEP_EQ {tStack x}`; 171val tL_def = Define `tL a x = SEP_EQ {tLocal a x}`; 172val tO_def = Define `tO x = SEP_EQ {tOK x}`; 173val tI_def = Define `tI a x = SEP_EQ {tInstr a x}`; 174 175val PC_def = Define `PC x = tP x * tO T`; 176 177val M1_INSTR_def = Define `M1_INSTR (a,w) = { tInstr a w }`; 178val M1_NEXT_def = Define `M1_NEXT s1 s2 = (step s1 = s2)`; 179 180val M1_MODEL_def = Define ` 181 M1_MODEL = (m1_2set, M1_NEXT, M1_INSTR, (\x y. (x:sexp) = y))`; 182 183 184(* theorems *) 185 186val lemma = 187 METIS_PROVE [SPLIT_m1_2set] 188 ``p (m1_2set' y s) ==> (?u v. SPLIT (m1_2set s) (u,v) /\ p u /\ (\v. v = m1_2set'' y s) v)``; 189 190val M1_SPEC_SEMANTICS = prove( 191 ``SPEC M1_MODEL p {} q = 192 !y s seq. p (m1_2set' y s) /\ rel_sequence M1_NEXT seq s ==> 193 ?k. q (m1_2set' y (seq k)) /\ (m1_2set'' y s = m1_2set'' y (seq k))``, 194 SIMP_TAC bool_ss [GSYM RUN_EQ_SPEC,RUN_def,M1_MODEL_def,STAR_def,SEP_REFINE_def] 195 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC 196 THEN1 (FULL_SIMP_TAC bool_ss [SPLIT_m1_2set_EXISTS] \\ METIS_TAC []) 197 \\ Q.PAT_ASSUM `!s r. b` (STRIP_ASSUME_TAC o UNDISCH o SPEC_ALL o 198 (fn th => MATCH_MP th (UNDISCH lemma)) o Q.SPECL [`s`,`(\v. v = m1_2set'' y s)`]) 199 \\ FULL_SIMP_TAC bool_ss [SPLIT_m1_2set_EXISTS] 200 \\ IMP_RES_TAC m1_2set''_11 \\ Q.EXISTS_TAC `i` \\ METIS_TAC []); 201 202 203(* ----------------------------------------------------------------------------- *) 204(* Theorems for construction of |- SPEC M1_MODEL ... *) 205(* ----------------------------------------------------------------------------- *) 206 207val SEP_EQ_STAR_LEMMA = prove( 208 ``!p s t. (SEP_EQ t * p) s <=> t SUBSET s /\ (t SUBSET s ==> p (s DIFF t))``, 209 METIS_TAC [EQ_STAR]); 210 211val FLIP_CONJ = prove(``!b c. b /\ (b ==> c) = b /\ c``,METIS_TAC []); 212 213val EXPAND_STAR = 214 GEN_ALL o (SIMP_CONV std_ss [tP_def, tS_def, tL_def, tO_def, tI_def, 215 SEP_EQ_STAR_LEMMA,INSERT_SUBSET,IN_m1_2set,DELETE_m1_2set, 216 DIFF_INSERT,DIFF_EMPTY,EMPTY_SUBSET] THENC SIMP_CONV std_ss [FLIP_CONJ] 217 THENC REWRITE_CONV [GSYM CONJ_ASSOC]) 218 219val STAR_m1_2set = LIST_CONJ (map EXPAND_STAR 220 [``(tP x * p) (m1_2set' (ps,ls,ss,is,os) s)``, 221 ``(tL a x * p) (m1_2set' (ps,ls,ss,is,os) s)``, 222 ``(tS x * p) (m1_2set' (ps,ls,ss,is,os) s)``, 223 ``(tI a x * p) (m1_2set' (ps,ls,ss,is,os) s)``, 224 ``(tO x * p) (m1_2set' (ps,ls,ss,is,os) s)``]); 225 226val CODE_POOL_m1_2set_LEMMA = prove( 227 ``!x y z. (x = z INSERT y) = (z INSERT y) SUBSET x /\ (x DIFF (z INSERT y) = {})``, 228 SIMP_TAC std_ss [EXTENSION,SUBSET_DEF,IN_INSERT,NOT_IN_EMPTY,IN_DIFF] \\ METIS_TAC []); 229 230val CODE_POOL_m1_2set = prove( 231 ``CODE_POOL M1_INSTR {(p,c)} (m1_2set' (ps,ls,ss,is,os) s) = 232 ({p} = is) /\ (ls = {}) /\ (ss = {}) /\ (ps = {}) /\ (os = {}) /\ 233 (instr p s = c)``, 234 SIMP_TAC bool_ss [CODE_POOL_def,IMAGE_INSERT,IMAGE_EMPTY,BIGUNION_INSERT, 235 BIGUNION_EMPTY,UNION_EMPTY,M1_INSTR_def,CODE_POOL_m1_2set_LEMMA, 236 GSYM DELETE_DEF, INSERT_SUBSET, EMPTY_SUBSET,IN_m1_2set] 237 \\ REPEAT STRIP_TAC \\ EQ_TAC \\ ASM_SIMP_TAC std_ss [] 238 \\ ASM_SIMP_TAC std_ss [DELETE_m1_2set,EMPTY_m1_2set,DIFF_INSERT] 239 \\ ASM_SIMP_TAC std_ss [GSYM AND_IMP_INTRO,DELETE_m1_2set,EMPTY_m1_2set,DIFF_EMPTY] 240 \\ ONCE_REWRITE_TAC [EQ_SYM_EQ] 241 \\ ASM_SIMP_TAC std_ss [DELETE_m1_2set,EMPTY_m1_2set]); 242 243val M1_SPEC_CODE = (RW [GSYM M1_MODEL_def] o SIMP_RULE std_ss [M1_MODEL_def] o prove) 244 (``SPEC M1_MODEL (CODE_POOL (FST (SND (SND M1_MODEL))) c * p) {} 245 (CODE_POOL (FST (SND (SND M1_MODEL))) c * q) = 246 SPEC M1_MODEL p c q``, 247 REWRITE_TAC [SPEC_CODE]); 248 249val IMP_M1_SPEC_LEMMA = prove( 250 ``!p q. 251 (!s s2 y. 252 p (m1_2set' y s) ==> 253 (?s1. M1_NEXT s s1) /\ 254 (M1_NEXT s s2 ==> q (m1_2set' y s2) /\ (m1_2set'' y s = m1_2set'' y s2))) ==> 255 SPEC M1_MODEL p {} q``, 256 REWRITE_TAC [M1_SPEC_SEMANTICS] \\ REPEAT STRIP_TAC \\ RES_TAC 257 \\ FULL_SIMP_TAC bool_ss [rel_sequence_def] 258 \\ Q.EXISTS_TAC `SUC 0` \\ METIS_TAC []); 259 260val IMP_M1_SPEC = 261 (RW1 [STAR_COMM] o RW [M1_SPEC_CODE] o 262 SPECL [``CODE_POOL M1_INSTR {(p,c)} * p1``, 263 ``CODE_POOL M1_INSTR {(p,c)} * q1``]) IMP_M1_SPEC_LEMMA; 264 265val m1_2set''_thm = prove( 266 ``(m1_2set'' (ps,ls,ss,is,os) s1 = m1_2set'' (ps,ls,ss,is,os) s2) = 267 (!a. ~(a IN ps) ==> (pc s1 = pc s2)) /\ 268 (!a. ~(a IN ls) ==> (nth_local a s1 = nth_local a s2)) /\ 269 (!a. ~(a IN ss) ==> (stack s1 = stack s2)) /\ 270 (!a. ~(a IN is) ==> (instr a s1 = instr a s2)) /\ 271 (!a. ~(a IN os) ==> (m1_ok s1 = m1_ok s2))``, 272 SIMP_TAC std_ss [oneTheory.one] 273 \\ REPEAT STRIP_TAC \\ REVERSE EQ_TAC \\ REPEAT STRIP_TAC 274 \\ FULL_SIMP_TAC std_ss [EXTENSION] 275 THEN1 (Cases \\ ASM_SIMP_TAC std_ss [IN_m1_2set] \\ METIS_TAC []) 276 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tPC (pc s1)`) 277 \\ METIS_TAC [IN_m1_2set]) 278 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tLocal a (nth_local a s1)`) 279 \\ METIS_TAC [IN_m1_2set]) 280 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tStack (stack s1)`) 281 \\ METIS_TAC [IN_m1_2set]) 282 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tInstr a (instr a s1)`) 283 \\ FULL_SIMP_TAC std_ss [IN_m1_2set,oneTheory.one] \\ METIS_TAC []) 284 THEN1 (Q.PAT_ASSUM `!x.bb` (ASSUME_TAC o Q.SPEC `tOK (m1_ok s1)`) 285 \\ METIS_TAC [IN_m1_2set])); 286 287 288(* ----------------------------------------------------------------------------- *) 289(* Proving a SPEC theorem for each M1 instruction *) 290(* ----------------------------------------------------------------------------- *) 291 292val acl2_simp = 293 SIMP_RULE std_ss [itel_def] o 294 SIMP_RULE list_ss 295 ([let_simp,andl_fold,itel_fold,itel_append,forall2_thm,exists2_thm,forall_fold, 296 exists_fold,implies,andl_simp,not_simp,t_nil] @ 297 (map GSYM [int_def,nat_def,List_def,asym_def,csym_def,ksym_def,osym_def])); 298 299val defs = map acl2_simp [actual_defun, app_defun, arg1_defun, 300 arg2_defun, arg3_defun, bind_defun, binding_defun, boundp_defun, 301 collect_at_end_defun, collect_vars_in_expr_defun, compile_defun, 302 concat_symbols_defun, do_inst_defun, even_sched_defun, 303 exclaim_defun, execute_goto_defun, execute_iadd_defun, 304 execute_iconst_defun, execute_ifle_defun, execute_iload_defun, 305 execute_imul_defun, execute_istore_defun, execute_isub_defun, 306 expr_exclaim_defun, frev_defun, goto_exclaim_defun, 307 iconst_exclaim_defun, ifact_defun, ifact_loop_sched_defun, 308 ifact_sched_defun, ifle_exclaim_defun, iload_exclaim_defun, 309 index_defun, istore_exclaim_defun, locals_defun, m1_len_defun, 310 m1_member_defun, make_defun_defun, make_state_defun, 311 next_inst_defun, nextn_defun, nth_defun, op_code_defun, 312 op_exclaim_defun, pattern_bindings_defun, pc_defun, pop_defun, 313 popn_defun, program_defun, push_defun, repeat_defun, rev1_defun, 314 rev_defun, run_defun, s_big_defun, s_fix_defun, skipn_defun, 315 stack_defun, step_defun, suppliedp_defun, test_even_defun, 316 test_exclaim_defun, test_ifact_defun, top_defun, u_big1_defun, 317 u_big_defun, u_fix_defun, update_nth_defun, while_exclaim_defun]; 318 319val defs2 = map acl2_simp [actual_defun, app_defun, arg1_defun, 320 arg2_defun, arg3_defun, bind_defun, binding_defun, boundp_defun, 321 collect_at_end_defun, collect_vars_in_expr_defun, compile_defun, 322 concat_symbols_defun, do_inst_defun, even_sched_defun, 323 exclaim_defun, execute_goto_defun, execute_iadd_defun, 324 execute_iconst_defun, execute_ifle_defun, execute_iload_defun, 325 execute_imul_defun, execute_istore_defun, execute_isub_defun, 326 expr_exclaim_defun, frev_defun, goto_exclaim_defun, 327 iconst_exclaim_defun, ifact_defun, ifact_loop_sched_defun, 328 ifact_sched_defun, ifle_exclaim_defun, iload_exclaim_defun, 329 index_defun, istore_exclaim_defun, m1_len_defun, m1_member_defun, 330 make_defun_defun, next_inst_defun, nextn_defun, op_code_defun, 331 op_exclaim_defun, pattern_bindings_defun, pop_defun, popn_defun, 332 push_defun, repeat_defun, rev1_defun, rev_defun, run_defun, 333 s_big_defun, s_fix_defun, skipn_defun, step_defun, suppliedp_defun, 334 test_even_defun, test_exclaim_defun, test_ifact_defun, top_defun, 335 u_big1_defun, u_big_defun, u_fix_defun, while_exclaim_defun]; 336 337 338val CODE_POOL_THM = prove( 339 ``!p x. CODE_POOL M1_INSTR {(p,x)} = tI p x``, 340 SIMP_TAC std_ss [CODE_POOL_def,IMAGE_INSERT,IMAGE_EMPTY,SEP_EQ_def, 341 BIGUNION_INSERT,BIGUNION_EMPTY,UNION_EMPTY,M1_INSTR_def,tI_def]); 342 343val UNIT_IN_SET = prove( 344 ``!x. () IN x = (x = {()})``, 345 SIMP_TAC std_ss [EXTENSION,IN_INSERT,NOT_IN_EMPTY] \\ METIS_TAC [oneTheory.one]); 346 347val ite_intro = store_thm("ite_intro", 348 ``!p x y. (if |= p then x else y) = ite p x y``, 349 ASM_SIMP_TAC std_ss [hol_defaxiomsTheory.ACL2_SIMPS] THEN METIS_TAC []); 350 351val add_COMM = store_thm("add_COMM", 352 ``!x y. add x y = add y x``, 353 Cases \\ Cases \\ SIMP_TAC std_ss [add_def] \\ Cases_on `c` \\ Cases_on `c'` 354 \\ SIMP_TAC std_ss [complex_rationalTheory.COMPLEX_ADD_def] 355 \\ METIS_TAC [ratTheory.RAT_ADD_COMM]); 356 357val add_ASSOC = store_thm("add_ASSOC", 358 ``!x y z. add (add x y) z = add x (add y z)``, 359 Cases \\ Cases \\ Cases \\ SIMP_TAC std_ss [add_def,int_def,cpx_def] 360 \\ Q.SPEC_TAC (`c`,`c`) \\ Q.SPEC_TAC (`c'`,`c2`) 361 \\ SIMP_TAC std_ss [] \\ REPEAT Cases 362 \\ Q.SPEC_TAC (`r`,`m`) \\ Q.SPEC_TAC (`r0`,`n`) \\ Q.SPEC_TAC (`c''`,`d`) 363 \\ SIMP_TAC std_ss [complex_rationalTheory.COMPLEX_ADD_def,rat_def] 364 \\ REPEAT Cases \\ SIMP_TAC std_ss [GSYM (EVAL ``0:rat``),ratTheory.RAT_ADD_LID, 365 RW1[ratTheory.RAT_ADD_COMM]ratTheory.RAT_ADD_LID, 366 complex_rationalTheory.COMPLEX_ADD_def,ratTheory.RAT_ADD_ASSOC]); 367 368val add_nat = store_thm("add_nat", 369 ``!m n. add (nat m) (nat n) = nat (m + n)``, 370 SIMP_TAC (srw_ss()) [add_def,int_def,nat_def,cpx_def, 371 complex_rationalTheory.COMPLEX_ADD_def,rat_def, 372 ratTheory.RAT_ADD_CALCULATE,fracTheory.FRAC_ADD_CALCULATE] 373 \\ `!m n. &(m + n) = &m + (&(n:num)):int` by intLib.COOPER_TAC 374 \\ ASM_SIMP_TAC std_ss []); 375 376val less_nat = store_thm("less_nat", 377 ``!m n. (|= (less (nat m) (nat n))) = m < n``, 378 SIMP_TAC (srw_ss()) [less_def,int_def,nat_def,cpx_def, 379 complex_rationalTheory.COMPLEX_LT_def,rat_def, 380 ratTheory.RAT_LES_CALCULATE,fracTheory.NMR,fracTheory.DNM] 381 \\ SRW_TAC [] [] \\ EVAL_TAC); 382 383val sexp_not = store_thm("sexp_not", 384 ``!s. (|= not s) = ~(|= s)``, 385 REPEAT STRIP_TAC \\ Cases_on `s = nil` \\ POP_ASSUM MP_TAC 386 \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC); 387 388val mult_nat = store_thm("mult_nat", 389 ``!m n. mult (nat m) (nat n) = nat (m * n)``, 390 SIMP_TAC (srw_ss()) [mult_def,int_def,nat_def,cpx_def, 391 complex_rationalTheory.COMPLEX_MULT_def,rat_def, 392 ratTheory.RAT_MUL_CALCULATE,fracTheory.FRAC_MULT_CALCULATE, 393 complex_rationalTheory.COMPLEX_ADD_def,rat_def, 394 ratTheory.RAT_ADD_CALCULATE,fracTheory.FRAC_ADD_CALCULATE, 395 ratTheory.RAT_SUB_CALCULATE,fracTheory.FRAC_SUB_CALCULATE]); 396 397val add_nat_int = store_thm("add_nat_int", 398 ``!m n. n <= m ==> (add (nat m) (int (-&n)) = nat (m - n))``, 399 SIMP_TAC (srw_ss()) [add_def,int_def,nat_def,cpx_def, 400 complex_rationalTheory.COMPLEX_ADD_def,rat_def, 401 ratTheory.RAT_ADD_CALCULATE,fracTheory.FRAC_ADD_CALCULATE, 402 integerTheory.INT_SUB,GSYM integerTheory.int_sub]); 403 404val unary_minus_int = store_thm("unary_minus_int", 405 ``!i. unary_minus (int i) = int (-i)``, 406 SIMP_TAC (srw_ss()) [unary_minus_def,int_def,nat_def,cpx_def, 407 complex_rationalTheory.COMPLEX_SUB_def,rat_def, 408 complex_rationalTheory.com_0_def,ratTheory.rat_0_def,fracTheory.frac_0_def, 409 ratTheory.RAT_SUB_CALCULATE,fracTheory.FRAC_SUB_CALCULATE, 410 integerTheory.INT_SUB,GSYM integerTheory.int_sub]); 411 412val rat_lemma = prove( 413 ``!x. ?y. (rep_rat (abs_rat x) = y) /\ rat_equiv x y``, 414 SIMP_TAC std_ss [] \\ ONCE_REWRITE_TAC [RW[quotientTheory.QUOTIENT_def]ratTheory.rat_def] 415 \\ SIMP_TAC std_ss [ratTheory.rat_equiv_def,ratTheory.RAT]); 416 417val DIVIDES_lemma = prove( 418 ``!n m. 0 < n ==> DIVIDES n (m * n)``, 419 EVAL_TAC \\ SIMP_TAC std_ss [GSYM integerTheory.INT_ABS_MUL] \\ REPEAT STRIP_TAC 420 \\ `?nn mm. (ABS n = &nn) /\ (ABS m = &mm)` by 421 METIS_TAC [integerTheory.INT_ABS_POS,integerTheory.NUM_POSINT_EXISTS] 422 \\ ASM_SIMP_TAC std_ss [integerTheory.INT_MUL,integerTheory.NUM_OF_INT] 423 \\ REPEAT STRIP_TAC \\ `0 < nn` by intLib.COOPER_TAC 424 \\ ASM_SIMP_TAC std_ss [arithmeticTheory.MOD_EQ_0]); 425 426val INTEGERP_INT = prove( 427 ``integerp (int n) = t``, 428 SIMP_TAC std_ss [int_def,integerp_def,cpx_def,IS_INT_def, 429 EVAL ``rat 0 1 = rat_0``] 430 \\ SIMP_TAC std_ss [ratTheory.rat_dnm_def,ratTheory.rat_nmr_def,rat_def] 431 \\ STRIP_ASSUME_TAC (Q.SPEC `abs_frac (n,1)` rat_lemma) 432 \\ ASM_SIMP_TAC std_ss [] \\ FULL_SIMP_TAC std_ss [ratTheory.rat_equiv_def] 433 \\ FULL_SIMP_TAC (srw_ss()) [fracTheory.NMR,fracTheory.DNM] 434 \\ POP_ASSUM (ASSUME_TAC o GSYM) 435 \\ Cases_on `DIVIDES (frac_dnm y) (n * frac_dnm y)` 436 \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC \\ POP_ASSUM MP_TAC 437 \\ METIS_TAC [fracTheory.FRAC_DNMPOS,DIVIDES_lemma]); 438 439val nth_lemma = store_thm("nth_lemma", 440 ``(nth (nat 0) x = car x) /\ 441 (nth (nat (SUC n)) x = nth (nat n) (cdr x))``, 442 SIMP_TAC std_ss [arithmeticTheory.ADD1] \\ REPEAT STRIP_TAC 443 \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [acl2_simp nth_defun])) 444 \\ SIMP_TAC (srw_ss()) [ACL2_SIMPS,nat_def,INTEGERP_INT,less_def, 445 cpx_def,EVAL ``int 0``,rat_def,ratTheory.RAT_LES_CALCULATE] 446 \\ ONCE_REWRITE_TAC [add_COMM] \\ SIMP_TAC std_ss [GSYM nat_def] 447 \\ SIMP_TAC std_ss [add_nat_int] \\ SIMP_TAC std_ss [nat_def] 448 \\ SIMP_TAC (srw_ss()) [ACL2_SIMPS,nat_def,INTEGERP_INT,less_def,int_def, 449 cpx_def,EVAL ``int 0``,rat_def,ratTheory.RAT_LES_CALCULATE, 450 fracTheory.NMR,fracTheory.DNM,DECIDE ``0<n+1:num``]); 451 452val update_nth_lemma = store_thm("update_nth_lemma", 453 ``(update_nth (nat 0) v list = cons v (cdr list)) /\ 454 (update_nth (nat (SUC n)) v list = cons (car list) (update_nth (nat n) v (cdr list)))``, 455 SIMP_TAC std_ss [arithmeticTheory.ADD1] \\ REPEAT STRIP_TAC 456 \\ CONV_TAC (RATOR_CONV (ONCE_REWRITE_CONV [acl2_simp update_nth_defun])) 457 \\ SIMP_TAC (srw_ss()) [ACL2_SIMPS,nat_def,INTEGERP_INT,less_def, 458 cpx_def,EVAL ``int 0``,rat_def,ratTheory.RAT_LES_CALCULATE] 459 \\ ONCE_REWRITE_TAC [add_COMM] \\ SIMP_TAC std_ss [GSYM nat_def] 460 \\ SIMP_TAC std_ss [add_nat_int] \\ SIMP_TAC std_ss [nat_def] 461 \\ SIMP_TAC (srw_ss()) [ACL2_SIMPS,nat_def,INTEGERP_INT,less_def,int_def, 462 cpx_def,EVAL ``int 0``,rat_def,ratTheory.RAT_LES_CALCULATE, 463 fracTheory.NMR,fracTheory.DNM,DECIDE ``0<n+1:num``]); 464 465val nth_thm = prove( 466 ``(nth (nat 0) (cons x0 x1) = x0) /\ 467 (nth (nat 1) (cons x0 (cons x1 x2)) = x1) /\ 468 (nth (nat 2) (cons x0 (cons x1 (cons x2 x3))) = x2) /\ 469 (nth (nat 3) (cons x0 (cons x1 (cons x2 (cons x3 x4)))) = x3)``, 470 SIMP_TAC bool_ss [nth_lemma,car_def,cdr_def, 471 DECIDE ``(1 = SUC 0) /\ (2 = SUC 1) /\ (3 = SUC 2) /\ (4 = SUC 3)``]); 472 473val nth_1 = save_thm("nth_1", 474 SIMP_CONV bool_ss [GSYM (EVAL ``SUC 0``),nth_lemma] ``nth (nat 1) x``); 475 476val update_nth_1 = save_thm("update_nth_1", 477 SIMP_CONV bool_ss [GSYM (EVAL ``SUC 0``),update_nth_lemma] ``update_nth (nat 1) v list``); 478 479val not_eq_nil = store_thm("not_eq_nil", 480 ``!x. (not x = nil) = (|= x)``, 481 REPEAT STRIP_TAC \\ Cases_on `x = nil` \\ POP_ASSUM MP_TAC 482 \\ ASM_SIMP_TAC std_ss [] \\ EVAL_TAC \\ ASM_SIMP_TAC std_ss []); 483 484val sexp_reduce_SUC = store_thm("sexp_reduce_SUC", 485 ``!n. add (nat (SUC n)) (unary_minus (nat 1)) = nat n``, 486 SIMP_TAC std_ss [ADD1,GSYM add_nat,add_ASSOC] 487 \\ `add (nat 1) (unary_minus (nat 1)) = nat 0` by ALL_TAC 488 \\ ASM_SIMP_TAC std_ss [add_nat] \\ SIMP_TAC std_ss [nat_def,unary_minus_int] 489 \\ SIMP_TAC std_ss [GSYM nat_def,add_nat_int]); 490 491val make_state_thm = prove( 492 ``(pc (make_state x y z p) = x) /\ 493 (locals (make_state x y z p) = y) /\ 494 (stack (make_state x y z p) = z) /\ 495 (program (make_state x y z p) = p)``, 496 ONCE_REWRITE_TAC defs \\ SIMP_TAC std_ss [make_state_defun,nth_thm]); 497 498val instr_step = prove( 499 ``!a s. instr a (step s) = instr a s``, 500 NTAC 2 (ONCE_REWRITE_TAC defs) \\ SIMP_TAC std_ss [ite_def] 501 \\ SRW_TAC [] [] \\ ONCE_REWRITE_TAC defs 502 \\ SIMP_TAC std_ss [instr_def,make_state_thm]); 503 504val m1_ok_step = prove( 505 ``!s. m1_ok s ==> m1_ok (step s)``, 506 NTAC 2 (ONCE_REWRITE_TAC defs) \\ SIMP_TAC std_ss [ite_def] 507 \\ SRW_TAC [] [] \\ ONCE_REWRITE_TAC defs 508 \\ SIMP_TAC std_ss [m1_ok_def] \\ METIS_TAC []); 509 510val IMP_SPEC_M1_MODEL = prove( 511 ``(!cs l1. (nth p1 cs = c) ==> 512 (step (make_state p1 l1 s1 cs) = make_state p2 l1 s2 cs)) ==> 513 SPEC M1_MODEL (tS s1 * PC p1) 514 {(p1,c)} (tS s2 * PC p2)``, 515 REPEAT STRIP_TAC 516 \\ MATCH_MP_TAC IMP_M1_SPEC \\ SIMP_TAC std_ss [M1_NEXT_def] 517 \\ SIMP_TAC std_ss [PC_def,GSYM STAR_ASSOC] 518 \\ SIMP_TAC std_ss [pairTheory.FORALL_PROD,STAR_m1_2set,CODE_POOL_m1_2set, 519 UNIT_IN_SET,m1_2set''_thm,IN_INSERT,NOT_IN_EMPTY,oneTheory.one,instr_step] 520 \\ STRIP_TAC \\ Cases_on `m1_ok s` \\ ASM_SIMP_TAC std_ss [m1_ok_step] 521 \\ FULL_SIMP_TAC std_ss [m1_ok_def,make_state_thm,instr_def] 522 \\ STRIP_TAC \\ RES_TAC \\ POP_ASSUM MP_TAC 523 \\ Q.PAT_ASSUM `!cs.bb` (K ALL_TAC) 524 \\ ASM_SIMP_TAC std_ss [make_state_thm,nth_local_def]); 525 526val IMP_SPEC_M1_MODEL_2 = prove( 527 ``(!cs l1. (nth p1 cs = c) /\ (v = nth (nat n) l1) ==> 528 (step (make_state p1 l1 s1 cs) = make_state p2 l1 s2 cs)) ==> 529 SPEC M1_MODEL (tS s1 * tL n v * PC p1) 530 {(p1,c)} (tS s2 * tL n v * PC p2)``, 531 REPEAT STRIP_TAC 532 \\ MATCH_MP_TAC IMP_M1_SPEC \\ SIMP_TAC std_ss [M1_NEXT_def] 533 \\ SIMP_TAC std_ss [PC_def,GSYM STAR_ASSOC] 534 \\ SIMP_TAC std_ss [pairTheory.FORALL_PROD,STAR_m1_2set,CODE_POOL_m1_2set, 535 UNIT_IN_SET,m1_2set''_thm,IN_INSERT,NOT_IN_EMPTY,oneTheory.one,instr_step] 536 \\ STRIP_TAC \\ Cases_on `m1_ok s` \\ ASM_SIMP_TAC std_ss [m1_ok_step] 537 \\ FULL_SIMP_TAC std_ss [m1_ok_def,make_state_thm,instr_def,nth_local_def] 538 \\ STRIP_TAC \\ STRIP_TAC \\ RES_TAC \\ POP_ASSUM MP_TAC 539 \\ Q.PAT_ASSUM `!cs.bb` (K ALL_TAC) 540 \\ ASM_SIMP_TAC std_ss [make_state_thm,nth_local_def]); 541 542val nth_update_nth = prove( 543 ``!n w l. (nth (nat n) (update_nth (nat n) w l) = w)``, 544 Induct \\ ASM_SIMP_TAC std_ss [nth_lemma,update_nth_lemma,car_def,cdr_def]); 545 546val nth_update_nth_NEQ = prove( 547 ``!n a w l. ~(n = a) ==> (nth (nat n) (update_nth (nat a) w l) = nth (nat n) l)``, 548 Induct \\ ASM_SIMP_TAC std_ss [nth_lemma,update_nth_lemma,car_def,cdr_def] 549 \\ Cases_on `a` \\ ASM_SIMP_TAC std_ss [] 550 \\ ASM_SIMP_TAC std_ss [nth_lemma,update_nth_lemma,car_def,cdr_def]); 551 552val IMP_SPEC_M1_MODEL_3 = prove( 553 ``(!cs l1. (nth p1 cs = c) /\ (v = nth (nat n) l1) ==> 554 (step (make_state p1 l1 s1 cs) = 555 make_state p2 (update_nth (nat n) w l1) s2 cs)) ==> 556 SPEC M1_MODEL (tS s1 * tL n v * PC p1) 557 {(p1,c)} (tS s2 * tL n w * PC p2)``, 558 REPEAT STRIP_TAC 559 \\ MATCH_MP_TAC IMP_M1_SPEC \\ SIMP_TAC std_ss [M1_NEXT_def] 560 \\ SIMP_TAC std_ss [PC_def,GSYM STAR_ASSOC] 561 \\ SIMP_TAC std_ss [pairTheory.FORALL_PROD,STAR_m1_2set,CODE_POOL_m1_2set, 562 UNIT_IN_SET,m1_2set''_thm,IN_INSERT,NOT_IN_EMPTY,oneTheory.one,instr_step] 563 \\ STRIP_TAC \\ Cases_on `m1_ok s` \\ ASM_SIMP_TAC std_ss [m1_ok_step] 564 \\ FULL_SIMP_TAC std_ss [m1_ok_def,make_state_thm,instr_def,nth_local_def] 565 \\ STRIP_TAC \\ STRIP_TAC \\ RES_TAC \\ POP_ASSUM MP_TAC 566 \\ Q.PAT_ASSUM `!cs.bb` (K ALL_TAC) 567 \\ ASM_SIMP_TAC std_ss [make_state_thm,nth_local_def,nth_update_nth] 568 \\ REPEAT STRIP_TAC \\ Cases_on `a = n` 569 \\ FULL_SIMP_TAC std_ss [nth_update_nth_NEQ]); 570 571val acl2_ss = std_ss ++ rewrites [hol_defaxiomsTheory.ACL2_SIMPS, 572 make_state_thm,nth_thm,CONS_11,NOT_CONS_NIL,stringTheory.CHR_11] 573 574fun M1_TAC thm = 575 SIMP_TAC std_ss [SPEC_MOVE_COND,precond_def] \\ SIMP_TAC std_ss [ACL2_TRUE] 576 \\ REPEAT STRIP_TAC 577 \\ MATCH_MP_TAC thm \\ ONCE_REWRITE_TAC defs2 578 \\ ASM_SIMP_TAC std_ss [make_state_thm,next_inst_defun] 579 \\ REPEAT STRIP_TAC \\ POP_ASSUM (K ALL_TAC) \\ REPEAT (POP_ASSUM MP_TAC) 580 \\ ONCE_REWRITE_TAC defs2 \\ SIMP_TAC acl2_ss [op_code_defun,List_def] 581 \\ ONCE_REWRITE_TAC defs2 \\ SIMP_TAC acl2_ss [op_code_defun,List_def] 582 \\ ONCE_REWRITE_TAC defs2 \\ SIMP_TAC acl2_ss [op_code_defun,List_def] 583 \\ ONCE_REWRITE_TAC defs2 \\ SIMP_TAC acl2_ss [op_code_defun,List_def] 584 \\ ONCE_REWRITE_TAC defs2 \\ SIMP_TAC acl2_ss [op_code_defun,List_def] 585 \\ METIS_TAC [add_COMM] 586 587 588val M1_ICONST = store_thm("M1_ICONST", 589 ``SPEC M1_MODEL 590 (tS s * PC p) 591 {(p, List [sym "M1" "ICONST"; x])} 592 (tS (push x s) * PC (add p (nat 1)))``, 593 M1_TAC IMP_SPEC_M1_MODEL); 594 595val M1_IADD = store_thm("M1_IADD", 596 ``SPEC M1_MODEL 597 (tS s * PC p) 598 {(p, List [sym "M1" "IADD"])} 599 (tS (push (add (top (pop s)) (top s)) (pop (pop s))) * PC (add p (nat 1)))``, 600 M1_TAC IMP_SPEC_M1_MODEL); 601 602val M1_ISUB = store_thm("M1_ISUB", 603 ``SPEC M1_MODEL 604 (tS s * PC p) 605 {(p, List [sym "M1" "ISUB"])} 606 (tS (push (add (top (pop s)) (unary_minus (top s))) (pop (pop s))) * PC (add p (nat 1)))``, 607 M1_TAC IMP_SPEC_M1_MODEL); 608 609val M1_IMUL = store_thm("M1_IMUL", 610 ``SPEC M1_MODEL 611 (tS s * PC p) 612 {(p, List [sym "M1" "IMUL"])} 613 (tS (push (mult (top (pop s)) (top s)) (pop (pop s))) * PC (add p (nat 1)))``, 614 M1_TAC IMP_SPEC_M1_MODEL); 615 616val M1_GOTO = store_thm("M1_GOTO", 617 ``SPEC M1_MODEL 618 (tS s * PC p) 619 {(p, List [sym "M1" "GOTO"; x])} 620 (tS s * PC (add p x))``, 621 M1_TAC IMP_SPEC_M1_MODEL); 622 623val M1_IFLE = store_thm("M1_IFLE", 624 ``SPEC M1_MODEL 625 (tS s * PC p * precond ((|= (not (less (nat 0) (top s)))))) 626 {(p, List [sym "M1" "IFLE"; x])} 627 (tS (pop s) * PC (add p x))``, 628 M1_TAC IMP_SPEC_M1_MODEL); 629 630val M1_IFLE_NOP = store_thm("M1_IFLE_NOP", 631 ``SPEC M1_MODEL 632 (tS s * PC p * precond (~(|= (not (less (nat 0) (top s)))))) 633 {(p, List [sym "M1" "IFLE"; x])} 634 (tS (pop s) * PC (add p (nat 1)))``, 635 M1_TAC IMP_SPEC_M1_MODEL); 636 637val M1_ILOAD = store_thm("M1_ILOAD", 638 ``SPEC M1_MODEL 639 (tS s * tL n v * PC p) 640 {(p, List [sym "M1" "ILOAD"; (nat n)])} 641 (tS (push v s) * tL n v * PC (add p (nat 1)))``, 642 M1_TAC IMP_SPEC_M1_MODEL_2); 643 644val M1_ISTORE = store_thm("M1_ISTORE", 645 ``SPEC M1_MODEL 646 (tS s * tL n v * PC p) 647 {(p, List [sym "M1" "ISTORE"; (nat n)])} 648 (tS (pop s) * tL n (top s) * PC (add p (nat 1)))``, 649 M1_TAC IMP_SPEC_M1_MODEL_3); 650 651 652val _ = export_theory(); 653