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