1structure armLib :> armLib = 2struct 3 4(* interactive use: 5 app load ["fcpLib", "armTheory", "coreTheory"]; 6*) 7 8open HolKernel boolLib bossLib Parse; 9open Q pairTheory; 10open onestepTheory armTheory coreTheory; 11 12(* ------------------------------------------------------------------------- *) 13 14local 15 val ICLASS_CONV = (REWRITE_CONV [iclass_EQ_iclass,iclass2num_thm] 16 THENC numLib.REDUCE_CONV); 17 fun conv_rec t = {name = "ICLASS_CONV",trace = 3,conv = K (K ICLASS_CONV), 18 key = SOME([t],mk_eq(t,``x:iclass``))}; 19in 20 val ICLASS_ss = simpLib.SSFRAG 21 {convs = map conv_rec [``swp``,``mrs_msr``,``data_proc``,``reg_shift``, 22 ``mla_mul``, ``ldr``,``str``,``ldm``,``stm``,``br``,``swi_ex``, 23 ``cdp_und``, ``mcr``,``mrc``,``ldc``,``stc``,``unexec``], 24 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = [], 25 name = SOME "ICLASS"}; 26end; 27 28local open fcpTheory in 29 val fcp_ss = std_ss ++ fcpLib.FCP_ss; 30end; 31 32val std_ss = std_ss ++ boolSimps.LET_ss; 33 34local open io_onestepTheory in 35 val stdi_ss = std_ss ++ ICLASS_ss ++ rewrites [iseq_distinct] ++ 36 (rewrites [state_out_accessors, state_out_updates_eq_literal, 37 state_out_accfupds, state_out_fupdfupds, state_out_literal_11, 38 state_out_fupdfupds_comp, state_out_fupdcanon, 39 state_out_fupdcanon_comp]) ; 40 val STATE_INP_ss = 41 rewrites [state_inp_accessors, state_inp_updates_eq_literal, 42 state_inp_accfupds, state_inp_fupdfupds, state_inp_literal_11, 43 state_inp_fupdfupds_comp, state_inp_fupdcanon, 44 state_inp_fupdcanon_comp]; 45end; 46 47local 48 fun rstrip_comb l = 49 if is_comb l then 50 List.concat (map rstrip_comb (snd (boolSyntax.strip_comb l))) 51 else 52 [l]; 53in 54 fun combCases M = 55 let val vlist = rstrip_comb M 56 val X = variant vlist (mk_var("x",type_of M)) 57 val tm = list_mk_exists(vlist, mk_eq(X,M)) 58 in 59 GEN_ALL (METIS_PROVE (map (fn (a,(b,c)) => b) (find "nchotomy")) tm) 60 end 61end; 62 63fun tupleCases M = 64 let val vlist = pairSyntax.strip_pair M 65 val X = variant vlist (mk_var("x",type_of M)) 66 val tm = list_mk_exists(vlist, mk_eq(X,M)) 67 in 68 GEN_ALL (METIS_PROVE [pairTheory.ABS_PAIR_THM] tm) 69 end; 70 71fun PBETA_CONV t = 72let val _ = (pairSyntax.dest_pabs o fst o dest_comb) t in 73 PairRules.PBETA_CONV t 74end; 75 76val PBETA_ss = 77 simpLib.conv_ss {name="PBETA", trace = 3, conv=K (K PBETA_CONV), key = NONE}; 78 79fun RES_MP1_TAC s t = 80 let val a = (fst o dest_imp o concl o INST s o SPEC_ALL) t 81 in 82 Tactical.SUBGOAL_THEN a (fn th => STRIP_ASSUME_TAC (MATCH_MP t th)) 83 end; 84 85fun RES_MP_TAC s t = RES_MP1_TAC s t THEN1 METIS_TAC []; 86 87fun mk_abbrev v = mk_comb(``Abbrev``,mk_eq(v,genvar (type_of v))); 88 89val dest_abbrev = dest_eq o snd o dest_comb; 90 91fun is_abbrev_match m t = 92let val v = fst (dest_abbrev m) 93 val rrl = match_term m t 94in 95 null (snd rrl) andalso 96 not (isSome (List.find (fn x => term_eq (#redex x) v) (fst rrl))) 97end; 98 99fun total_is_abbrev_match m t = 100 case total (is_abbrev_match m) t of 101 SOME b => b 102 | _ => false; 103 104fun get_abbrev_match m t = find_term (total_is_abbrev_match m) t; 105 106fun UNABBREV_RULE q thm = 107let val t = concl thm 108 val m = mk_abbrev (parse_in_context (free_vars t) q) 109 val mt = get_abbrev_match m t 110 val (l,r) = dest_abbrev mt 111in 112 PURE_REWRITE_RULE [METIS_PROVE [] ``Abbrev (x = x)``, 113 AND_CLAUSES,OR_CLAUSES,IMP_CLAUSES] (Thm.INST [l |-> r] thm) 114end; 115 116end 117