1structure graph_specsLib :> graph_specsLib = 2struct 3 4open HolKernel boolLib bossLib Parse; 5open wordsTheory listTheory combinTheory progTheory; 6open helperLib backgroundLib file_readerLib derive_specsLib stack_introLib 7open writerLib; 8 9open GraphLangTheory 10 11val code_case_of = TypeBase.case_def_of ``:code``; 12 13val emp_pat = ``emp:'a set set`` 14val s_var = mk_var("s",``:state``) 15 16fun get_pc_pat () = let 17 val (_,_,_,pc) = get_tools () 18 in ``^pc w`` end 19 20local 21 val var_bool_pat = ``var_bool n s`` 22 val var_nat_pat = ``var_nat n s`` 23 val var_word8_pat = ``var_word8 n s`` 24 val var_word32_pat = ``var_word32 n s`` 25 val var_mem_pat = ``var_mem n s`` 26in 27 fun var_lookup tm = 28 can (match_term var_bool_pat) tm orelse 29 can (match_term var_nat_pat) tm orelse 30 can (match_term var_word8_pat) tm orelse 31 can (match_term var_word32_pat) tm orelse 32 can (match_term var_mem_pat) tm 33 fun mk_update (x,y) = 34 if can (match_term var_bool_pat) x then 35 pairSyntax.mk_pair(x |> rator |> rand,mk_abs(s_var,mk_comb(``VarBool``,y))) 36 else if can (match_term var_nat_pat) x then 37 pairSyntax.mk_pair(x |> rator |> rand,mk_abs(s_var,mk_comb(``VarNat``,y))) 38 else if can (match_term var_word8_pat) x then 39 pairSyntax.mk_pair(x |> rator |> rand,mk_abs(s_var,mk_comb(``VarWord8``,y))) 40 else if can (match_term var_word32_pat) x then 41 pairSyntax.mk_pair(x |> rator |> rand,mk_abs(s_var,mk_comb(``VarWord32``,y))) 42 else if can (match_term var_mem_pat) x then 43 pairSyntax.mk_pair(x |> rator |> rand,mk_abs(s_var,mk_comb(``VarMem``,y))) 44 else failwith "should not happen (mk_update)" 45end 46 47local 48 val arm_state_inst = arm_STATE_thm |> concl |> find_terms var_lookup 49 |> map (fn tm => 50 let 51 val str = tm |> rator |> rand |> stringSyntax.fromHOLstring 52 val ty = type_of tm 53 in mk_var(str,ty) |-> tm end) 54 |> (fn x => (``dmem:word32 set`` |-> 55 ``(var_dom "dom" s):word32 set``):: 56 (``dom_stack:word32 set`` |-> 57 ``(var_dom "dom_stack" s):word32 set``):: 58 (``mode:word5`` |-> 59 ``w2w (var_word8 "mode" s):word5``)::x) |> INST 60 val arm_state = arm_STATE_thm |> concl |> rator |> rand 61 val arm_state_parts = arm_STATE_thm |> concl |> rand |> list_dest dest_star 62 val arm_state_type = arm_state_parts |> hd |> type_of 63 val arm_state_combs = map (fn tm => (rator tm,rand tm)) arm_state_parts 64 val arm_state_thm = arm_STATE_thm 65 val m0_state_inst = m0_STATE_thm |> concl |> find_terms var_lookup 66 |> map (fn tm => 67 let 68 val str = tm |> rator |> rand |> stringSyntax.fromHOLstring 69 val ty = type_of tm 70 in mk_var(str,ty) |-> tm end) 71 |> (fn x => (``dmem:word32 set`` |-> 72 ``(var_dom "dom" s):word32 set``):: 73 (``dom_stack:word32 set`` |-> 74 ``(var_dom "dom_stack" s):word32 set``):: 75 (mk_var("count",``:num``) |-> 76 ``(var_nat "clock" s):num``):: 77 (``mode:Mode`` |-> 78 ``Mode_Thread:Mode``)::x) |> INST 79 val m0_state = m0_STATE_thm |> concl |> rator |> rand 80 val m0_state_parts = m0_STATE_thm |> concl |> rand |> list_dest dest_star 81 val m0_state_type = m0_state_parts |> hd |> type_of 82 val m0_state_combs = map (fn tm => (rator tm,rand tm)) m0_state_parts 83 val m0_state_thm = m0_STATE_thm 84in 85 fun state_tools () = 86 case (!arch_name) of 87 ARM => (arm_state_inst, arm_state, arm_state_parts, 88 arm_state_type, arm_state_combs, arm_state_thm) 89 | M0 => (m0_state_inst, m0_state, m0_state_parts, m0_state_type, 90 m0_state_combs, m0_state_thm) 91end 92 93val STATE_INTRO_RULE_input = ref TRUTH 94(* 95 val th = !STATE_INTRO_RULE_input 96*) 97fun STATE_INTRO_RULE th = let 98 val (state_inst, state, state_parts, 99 state_type, state_combs, state_thm) = state_tools () 100 val pc_pat = get_pc_pat () 101 val th = th |> SIMP_RULE (std_ss++sep_cond_ss) [] 102 |> REWRITE_RULE [SPEC_MOVE_COND] |> UNDISCH_ALL 103 |> Q.INST [`curr`|->`stack`] 104 (* make pre into just ``STATE s`` *) 105 val th = state_inst th 106 val (_,pre,_,_) = dest_spec (concl th) 107 val ps = list_dest dest_star pre 108 val pc = first (can (match_term pc_pat)) ps 109 val missing_parts = diff state_parts ps 110 val frame = list_mk_star missing_parts state_type 111 val th = SPEC_FRAME_RULE th frame 112 val (_,pre,_,_) = dest_spec (concl th) 113 val goal = mk_eq(pre,mk_star(state,pc)) 114 val conv = PURE_REWRITE_CONV [state_thm,emp_STAR] THENC 115 BINOP_CONV STAR_AC_CONV THENC REWRITE_CONV [] 116 val lemma = auto_conv_prove "STATE_INTRO_RULE - 1" goal conv 117 val th = th |> CONV_RULE (PRE_CONV (REWR_CONV lemma)) 118 (* make post into just state *) 119 val th = PURE_REWRITE_RULE [STAR_IF] th 120 val (_,_,_,post) = dest_spec (concl th) 121 fun fix_post_conv post = let 122 val ps = list_dest dest_star post 123 val pc = first (can (match_term pc_pat)) ps 124 val ps = filter (not o can (match_term pc_pat)) ps 125 val ps = filter (not o can (match_term emp_pat)) ps 126 fun find_match x [] = fail () 127 | find_match x ((n,y)::xs) = 128 if x = n then y else find_match x xs 129 fun find_all_matches tm = 130 [(find_match (rator tm) state_combs,rand tm)] 131 handle HOL_ERR _ => let 132 val x = repeat rator tm 133 val y = first (fn tm => x = repeat rator tm) state_parts 134 fun dest_app tm = let 135 val (x,y) = dest_comb tm 136 val (f,xs) = dest_app x 137 in (f,xs @ [y]) end handle HOL_ERR _ => (tm,[]) 138 val xs = zip (dest_app y |> snd) (dest_app tm |> snd) 139 in xs end 140 val qs = ps |> map find_all_matches |> flatten 141 |> filter (fn (x,y) => x <> y) |> all_distinct 142 val new_s = listSyntax.mk_list( 143 foldl (fn ((x,y),s) => mk_update(x,y)::s) [] qs, 144 ``:string # (state -> variable)``) 145 val new_s = ``apply_update ^new_s ^s_var`` 146 val goal = mk_eq(post,mk_star(mk_comb(rator state,new_s),pc)) 147 val conv = (REWRITE_CONV [state_thm,var_update_thm, 148 apply_update_def, 149 CONS_11,NOT_CONS_NIL,GSYM NOT_CONS_NIL] 150 THENC (DEPTH_CONV stringLib.string_EQ_CONV) 151 THENC REWRITE_CONV [] THENC SIMP_CONV (srw_ss()) [] 152 THENC PURE_REWRITE_CONV [state_thm,emp_STAR] 153 THENC BINOP_CONV STAR_AC_CONV THENC REWRITE_CONV []) 154 val lemma = auto_conv_prove "STATE_INTRO_RULE - 2" goal conv 155 in lemma end 156 fun fix_if_post_conv post = 157 if is_cond post then BINOP_CONV fix_if_post_conv post 158 else fix_post_conv post 159 val th = th |> CONV_RULE (POST_CONV fix_if_post_conv) 160 in th end 161 handle HOL_ERR e => 162 (STATE_INTRO_RULE_input := th; 163 report_error "STATE_INTRO_RULE" (HOL_ERR e)) 164 165fun write_transform th1 th2_opt th_res = let 166 val clean_th = REWRITE_RULE [] o DISCH_ALL 167 val _ = write_line "Proved:" 168 val _ = write_thm (clean_th th_res) 169 val _ = write_line "Using:" 170 val _ = write_thm (clean_th th1) 171 val _ = (case th2_opt of NONE => () | SOME th => write_thm (clean_th th)) 172 in th_res end 173 174fun mk_code_term c = 175 case (!arch_name) of ARM => ``ARM ^c`` | M0 => ``M0 ^c``; 176 177val make_ASM_input = ref TRUTH; 178val make_CALL_input = ref TRUTH; 179val make_SWITCH_input = ref TRUTH; 180 181local 182 fun read_pc_assum hs = let 183 val h = first (can (match_term ``var_word32 "pc" s = w``)) hs 184 in (h |> rand,filter (fn tm => tm <> h) hs) end 185 fun read_pc_update th = let 186 val tm = find_term (can (match_term ``("pc" =+ VarWord32 (n2w n))``)) 187 (concl th) |> rand |> rand 188 in (mk_comb(``Jump``,tm),th) end 189 handle HOL_ERR _ => let 190 val tm = find_term (can (match_term ``("pc" =+ pat)``)) (concl th) 191 val x = ``var_word32 "ret" s`` 192 val assum = mk_eq(tm |> rand,``^s_var "ret"``) 193 val rw = RAND_CONV (fn tm => ASSUME assum) tm 194 val th = RW1 [rw] th 195 in (``Return``,th) end 196 fun read_state_update th = let 197 val (_,_,_,q) = dest_spec (concl th) 198 in q |> rand end 199 val simp = SIMP_CONV std_ss [IMPL_INST_def,exec_next_def,CONS_11,NOT_CONS_NIL, 200 check_jump_def,get_assert_def,APPLY_UPDATE_THM, 201 stringTheory.CHR_11,code_case_of] 202 fun has_call_tag th = 203 can (find_term (can dest_call_tag)) (concl (DISCH_ALL th)) 204 val ret_and_all_names = 205 ret_and_all_names_def |> concl |> rand 206 |> REWRITE_CONV [all_names_def,APPEND] |> concl |> rand 207 |> listSyntax.dest_list |> fst 208 fun dest_supdate tm = 209 listSyntax.dest_list tm |> fst |> map pairSyntax.dest_pair 210 fun prepare_supdate_for_call th = let 211 val (_,pre,_,post) = dest_spec (concl th) 212 val pc1 = pre |> rand |> rand 213 val tm = post |> rator |> rand |> rand |> rator |> rand 214 val supdate = dest_supdate tm 215 val r0 = ``"r0"`` 216 val r14 = ``"r14"`` 217 val ret_str = ``"ret"`` 218 val r0_input_str = ``"r0_input"`` 219 val (is_tail_call,ret) = let 220 val u = first (fn (t,x) => t = r14) supdate |> snd 221 val res = EVAL ``(^u s = VarWord32 (^pc1+4w)) \/ (^u s = VarWord32 (^pc1+2w))`` 222 |> concl |> rand 223 in if res = T then 224 (false,mk_comb(``Jump``,u |> dest_abs |> snd |> rand)) 225 else (true,``Return``) end handle HOL_ERR _ => (true,``Return``) 226 fun get_assign tm = 227 if tm = r0_input_str then 228 pairSyntax.mk_pair(r0_input_str,``var_acc ^r0``) 229 else let 230 val tm2 = if is_tail_call then tm else 231 if tm = ret_str then r14 else tm 232 val rhs = first (fn (t,x) => (t = tm2)) supdate |> snd 233 handle HOL_ERR _ => ``var_acc ^tm`` 234 in pairSyntax.mk_pair(tm,rhs) end 235 val new_supdate = map get_assign ret_and_all_names 236 val new_supdate = listSyntax.mk_list(new_supdate,type_of (hd new_supdate)) 237 val x = post |> rator |> rand |> rator 238 val goal = ``^x (apply_update ^tm s) = ^x (apply_update ^new_supdate s)`` 239 val lemma = auto_prove "prepare_supdate_for_call" (goal, 240 TRY (MATCH_MP_TAC arm_STATE_all_names) 241 \\ TRY (MATCH_MP_TAC m0_STATE_all_names) 242 \\ REWRITE_TAC [all_names_def,EVERY_DEF,apply_update_def, 243 combinTheory.APPLY_UPDATE_THM,var_acc_def] 244 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 245 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 246 \\ REWRITE_TAC [all_names_def,EVERY_DEF,apply_update_def, 247 combinTheory.APPLY_UPDATE_THM,var_acc_def]) 248 val th = CONV_RULE ((RAND_CONV o RATOR_CONV o RAND_CONV) 249 (REWR_CONV lemma)) th 250 in (th,ret) end 251(* 252 val th = !make_CALL_input 253*) 254 fun make_CALL th = let 255 val th = STATE_INTRO_RULE th 256 val hs = filter (fn tm => tm <> T) (hyp th) 257 val tag = first (can dest_call_tag) hs 258 val fname = fst (dest_call_tag tag) 259 val th = th |> DISCH_ALL |> PURE_REWRITE_RULE [CALL_TAG_def] |> UNDISCH_ALL 260 val (_,pre,_,post) = dest_spec (concl th) 261 val pc1 = pre |> rand |> rand 262 val pc2 = post |> rand |> rand 263 val supdate = post |> rator |> rand |> rand |> rator |> rand 264 val hs = filter (fn tm => tm <> T) (hyp th) 265 val side = if length hs = 0 then ``NONE:(state->bool) option`` 266 else ``SOME ^(mk_abs(s_var,list_mk_conj hs))`` 267 val (th,ret) = prepare_supdate_for_call th 268 val (_,pre,_,post) = dest_spec (concl th) 269 val supdate = post |> rator |> rand |> rand |> rator |> rand 270 val name = stringSyntax.fromMLstring fname 271 val i = ``Inst ^pc1 (K T) (CALL ^side ^supdate ^name ^ret)`` 272 val (m,_,c,_) = dest_spec (concl th) 273 val goal = ``(locs ^name = SOME ^pc2) ==> IMPL_INST ^(mk_code_term c) locs ^i`` 274(* 275 set_goal([],goal) 276*) 277 val lemma = auto_prove "make_CALL" (goal, 278 CONV_TAC simp \\ REPEAT STRIP_TAC \\ IMP_RES_TAC ret_lemma 279 \\ ASM_SIMP_TAC std_ss [code_case_of] 280 \\ NTAC 20 (ONCE_REWRITE_TAC [var_word32_apply_update]) 281 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 282 \\ ASM_REWRITE_TAC [apply_update_NIL] 283 \\ SIMP_TAC std_ss [next_ok_def,check_ret_def] 284 \\ TRY (REWRITE_TAC [ret_and_all_names_def,all_names_def,MAP,APPEND] 285 \\ REWRITE_TAC [all_names_def,EVERY_DEF,apply_update_def, 286 combinTheory.APPLY_UPDATE_THM,var_acc_def,var_word32_def] 287 \\ EVAL_TAC \\ NO_TAC) 288 \\ (DISCH_ALL th |> DISCH T 289 |> PURE_REWRITE_RULE [AND_IMP_INTRO] |> MATCH_MP_TAC) 290 \\ ASM_REWRITE_TAC [] \\ FULL_SIMP_TAC (srw_ss()) []) 291 val th = lemma |> UNDISCH_ALL |> SIMP_RULE std_ss [word_add_n2w] 292 in th end 293 handle HOL_ERR e => 294 (make_CALL_input := th; 295 report_error "make_CALL" (HOL_ERR e)) 296(* 297 val th = !make_ASM_input 298*) 299 fun make_ASM th = 300 if has_call_tag th then make_CALL th else let 301 val th = STATE_INTRO_RULE th 302 val (_,pre,_,post) = dest_spec (concl th) 303 val pc1 = pre |> rand |> rand 304 val pc2 = post |> rand |> rand 305 val supdate = post |> rator |> rand |> rand |> rator |> rand 306 val (jmp,th) = if wordsSyntax.is_n2w pc2 then (``Jump ^pc2``,th) else 307 (``Return``,let 308 val lemma = ASSUME (mk_eq(pc2,``var_word32 "ret" s``)) 309 in CONV_RULE (RAND_CONV (RAND_CONV (RAND_CONV (fn tm => lemma)))) th end) 310 val hs = filter (fn tm => tm <> T) (hyp th) 311 val side = if length hs = 0 then ``NONE:(state->bool) option`` 312 else ``SOME ^(mk_abs(s_var,list_mk_conj hs))`` 313 val i = ``Inst ^pc1 (K T) (ASM ^side ^supdate ^jmp)`` 314 val th = RW [apply_update_NIL] th 315 val (m,_,c,_) = dest_spec (concl th) 316 val goal = ``IMPL_INST ^(mk_code_term c) locs ^i`` 317(* 318 set_goal([],goal) 319*) 320 val lemma = auto_prove "make_ASM" (goal, 321 CONV_TAC simp \\ REPEAT STRIP_TAC \\ IMP_RES_TAC ret_lemma 322 \\ ASM_SIMP_TAC std_ss [code_case_of] 323 \\ NTAC 20 (ONCE_REWRITE_TAC [var_word32_apply_update]) 324 \\ CONV_TAC (DEPTH_CONV stringLib.string_EQ_CONV) 325 \\ ASM_REWRITE_TAC [apply_update_NIL] THEN1 EVAL_TAC THEN1 EVAL_TAC 326 \\ (DISCH_ALL th |> DISCH T 327 |> PURE_REWRITE_RULE [AND_IMP_INTRO] |> MATCH_MP_TAC) 328 \\ ASM_REWRITE_TAC [] \\ FULL_SIMP_TAC (srw_ss()) []) 329 in lemma end 330 handle HOL_ERR e => 331 (make_ASM_input := th; 332 report_error "make_ASM" (HOL_ERR e)) 333(* 334 val th = !make_SWITCH_input 335*) 336 fun make_SWITCH th = let 337 val th = STATE_INTRO_RULE th 338 (* val th = SIMP_RULE std_ss [Once EQ_SYM_EQ] th *) 339 val post = th |> concl |> rand 340 val pre = 341 th |> DISCH_ALL |> DISCH T |> PURE_REWRITE_RULE [AND_IMP_INTRO] 342 |> CONV_RULE ((RATOR_CONV o RAND_CONV) (REWRITE_CONV [])) 343 |> concl |> dest_imp |> fst 344 val pre = mk_abs(s_var,pre) 345 fun get_simp_asm x1 = let 346 val upd = x1 |> rator |> rand |> rand |> rator |> rand 347 val pc = x1 |> rand |> rand 348 in ``ASM (SOME ^pre) ^upd (Jump ^pc)`` end 349 fun dest_ifs post = let 350 val (g,x1,x2) = dest_cond post 351 val next1 = get_simp_asm x1 352 val next2 = dest_ifs x2 353 in ``IF (\s. ^g) ^next1 ^next2`` end 354 handle HOL_ERR _ => get_simp_asm post 355 val next = dest_ifs post 356 val pc1 = th |> concl |> rator |> rator |> rand |> rand |> rand 357 val i = ``Inst ^pc1 (K T) ^next`` 358 val (m,_,c,_) = dest_spec (concl th) 359 val goal = ``IMPL_INST ^(mk_code_term c) locs ^i`` 360 val lemma = auto_prove "make_SWITCH" (goal, 361 REWRITE_TAC [IMPL_INST_IF_SPLIT] 362 \\ CONV_TAC (DEPTH_CONV BETA_CONV) 363 \\ REPEAT STRIP_TAC 364 \\ CONV_TAC simp \\ REPEAT STRIP_TAC 365 \\ TRY (EVAL_TAC \\ NO_TAC) 366 \\ MP_TAC (DISCH_ALL th) 367 \\ ASM_REWRITE_TAC [] 368 \\ STRIP_TAC 369 \\ TRY (POP_ASSUM MATCH_MP_TAC) 370 \\ ASM_REWRITE_TAC [var_word32_def,var_acc_def] 371 \\ EVAL_TAC) 372 in lemma end 373 handle HOL_ERR e => 374 (make_SWITCH_input := th; 375 report_error "make_SWITCH" (HOL_ERR e)) 376in 377 fun make_INST (i:int,(th,l:int,j:int option),NONE) = 378 write_transform th NONE 379 (if not (is_cond (rand (concl th))) 380 then make_ASM th else make_SWITCH th) 381 | make_INST (i,(th1',l',j'),SOME (th2',l:int,j:int option)) = let 382 val th1 = make_INST (i,(th1',l',j'),NONE) 383 val th2 = th2' |> make_ASM 384 val not_guard = th2 |> concl |> find_term (can (match_term ``ASM (SOME k)``)) 385 |> rand |> rand |> dest_abs |> snd 386 val guard = dest_neg not_guard handle HOL_ERR _ => mk_neg not_guard 387 val c = (RAND_CONV o RATOR_CONV o RAND_CONV) (SIMP_CONV std_ss []) 388 val th = MATCH_MP IMPL_INST_IF (CONJ th1 th2) 389 |> CONV_RULE (BINOP1_CONV (SIMP_CONV std_ss [])) 390 |> MATCH_MP T_IMP |> SPEC (mk_abs(s_var,guard)) 391 val th = RW1 [IMPL_INST_SIMP_IF] th 392 |> SIMP_RULE std_ss [IMPL_INST_IF_RW] 393 in write_transform th1' (SOME th2') th end 394end 395 396(* 397val (i:int,(th,l:int,j:int option),NONE) = 398 first (fn (i,(th,_,_),_) => i = 52) thms 399 400val (i:int,(th,l:int,j:int option),NONE) = thms |> el 2 401 402val (_,(th1,_,_),SOME (th2,l:int,j:int option)) = first (not o can make_INST) thms 403 404*) 405 406fun try_map g f [] = [] 407 | try_map g f (x::xs) = let 408 val y = f x 409 in y :: try_map g f xs end 410 handle HOL_ERR _ => 411 (g x; try_map g f xs) 412 413val graph_spec_fails = ref ([] : (int * string) list); 414 415fun print_graph_spec_fail (pos,sec_name) = let 416 val str = ("Graph spec failed in " ^ sec_name ^ " for pos " ^ 417 (int_to_hex pos) ^ ".") 418 in (write_line str; print (str ^ "\n")) end 419 420fun add_graph_spec_fail pos sec_name = 421 (print_graph_spec_fail (pos,sec_name); 422 graph_spec_fails := (pos, sec_name) :: (!graph_spec_fails)); 423 424fun clear_graph_spec_fails () = (graph_spec_fails := []); 425 426fun print_graph_spec_report () = 427 (if length (!graph_spec_fails) = 0 then 428 (write_line "No graph spec failures."; []) 429 else (map print_graph_spec_fail (!graph_spec_fails))) 430 431fun get_pc_val th = let 432 val pc_pat = get_pc_pat () 433 val (_,p,_,_) = dest_spec (concl th) 434 in find_term (can (match_term pc_pat)) p 435 |> rand |> rand |> numSyntax.int_of_term end 436 437local 438 val r = ref [""]; 439 fun get_index_name name i = let 440 val str = name ^ "_" ^ int_to_string i 441 in if mem str (!r) then get_index_name name (i+1) 442 else(r := str::(!r); str) end 443in 444 fun get_name name = 445 if mem name (!r) then get_index_name name 0 446 else (r := name::(!r); name) 447end 448 449fun derive_insts_for sec_name = let 450 val thms = derive_specs_for sec_name 451 val _ = write_subsection "Proving inst theorems" 452 val _ = (writer_prints := false) 453 val insts = try_map (fn (_,(th,_,_),_) => 454 add_graph_spec_fail (get_pc_val th) sec_name) make_INST thms 455 val _ = (writer_prints := true) 456 val all_ok_chars = explode 457 ("abcdefghijklmonpqrstuvwxyz" ^ 458 "ABCDEFGHIJKLMNOPQRSTUVWXYZ" ^ 459 "0123456789_") 460 fun remove_SKIP_TAG th = let 461 val pos = th |> concl |> rand |> rator |> rator |> rand |> rand 462 |> numSyntax.dest_numeral 463 |> Arbnumcore.toHexString 464 val th = MATCH_MP SKIP_TAG_IMP_CALL th 465 val name = find_term (can stringLib.dest_string) (concl th) 466 fun join [] = "" 467 | join [x] = x 468 | join (x::ys) = x ^ "_" ^ join ys 469 fun prefix_instr str = "instruction'" ^ str ^ "_" ^ pos 470 val new_name = stringLib.fromHOLstring name 471 |> String.tokens (fn c => not (mem c all_ok_chars)) 472 |> join |> prefix_instr |> get_name 473 in th |> SIMP_RULE std_ss [] 474 |> SPEC (stringLib.fromMLstring new_name) 475 |> UNDISCH end 476 handle HOL_ERR _ => th 477 val insts = map remove_SKIP_TAG insts 478 val inst_count = int_to_string (length insts) 479 val _ = write_line (inst_count ^ " inst theorems describe instructions.") 480 in insts end; 481 482end 483