1structure armLib :> armLib = 2struct 3 4(* interactive use: 5 app load ["fcpLib", "armTheory"]; 6*) 7 8open HolKernel boolLib bossLib Parse; 9open Q pairTheory armTheory; 10 11(* ------------------------------------------------------------------------- *) 12 13local 14 val ICLASS_CONV = (REWRITE_CONV [iclass_EQ_iclass,iclass2num_thm] 15 THENC numLib.REDUCE_CONV); 16 fun conv_rec t = {name = "ICLASS_CONV",trace = 3,conv = K (K ICLASS_CONV), 17 key = SOME([t],mk_eq(t,``x:iclass``))}; 18in 19 val ICLASS_ss = simpLib.SSFRAG 20 {name = SOME"ICLASS", 21 convs = map conv_rec [``swp``,``mrs``,``msr``,``data_proc``, 22 ``mla_mul``, ``ldr_str``,``ldrh_strh``, ``ldm_stm``, 23 ``br``,``swi_ex``, ``cdp_und``, ``mcr``,``mrc``,``ldc_stc``, 24 ``unexec``], 25 rewrs = [], congs = [], filter = NONE, ac = [], dprocs = []}; 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 35 fun rstrip_comb l = 36 if is_comb l then 37 List.concat (map rstrip_comb (snd (boolSyntax.strip_comb l))) 38 else 39 [l]; 40in 41 fun combCases M = 42 let val vlist = rstrip_comb M 43 val X = variant vlist (mk_var("x",type_of M)) 44 val tm = list_mk_exists(vlist, mk_eq(X,M)) 45 in 46 GEN_ALL (METIS_PROVE (map (fn (a,(b,c)) => b) (find "nchotomy")) tm) 47 end 48end; 49 50fun tupleCases M = 51 let val vlist = pairSyntax.strip_pair M 52 val X = variant vlist (mk_var("x",type_of M)) 53 val tm = list_mk_exists(vlist, mk_eq(X,M)) 54 in 55 GEN_ALL (METIS_PROVE [pairTheory.ABS_PAIR_THM] tm) 56 end; 57 58val PBETA_ss = simpLib.SSFRAG 59 {name = SOME "PBETA", 60 convs = [{name="PBETA",trace = 3,conv=K (K PairRules.PBETA_CONV), 61 key = SOME([],``(\(x:'a,y:'b). s1) s2:'c``)}], rewrs = [], congs = [], 62 filter = NONE, ac = [], dprocs = []}; 63 64fun RES_MP1_TAC s t = 65 let val a = (fst o dest_imp o concl o INST s o SPEC_ALL) t 66 in 67 Tactical.SUBGOAL_THEN a (fn th => STRIP_ASSUME_TAC (MATCH_MP t th)) 68 end; 69 70fun RES_MP_TAC s t = RES_MP1_TAC s t THEN1 METIS_TAC []; 71 72fun mk_abbrev v = mk_comb(``Abbrev``,mk_eq(v,genvar (type_of v))); 73 74val dest_abbrev = dest_eq o snd o dest_comb; 75 76fun is_abbrev_match m t = 77let val v = fst (dest_abbrev m) 78 val rrl = match_term m t 79in 80 null (snd rrl) andalso 81 not (isSome (List.find (fn x => term_eq (#redex x) v) (fst rrl))) 82end; 83 84fun total_is_abbrev_match m t = 85 case total (is_abbrev_match m) t of 86 SOME b => b 87 | _ => false; 88 89fun get_abbrev_match m t = find_term (total_is_abbrev_match m) t; 90 91fun UNABBREV_RULE q thm = 92let val t = concl thm 93 val m = mk_abbrev (parse_in_context (free_vars t) q) 94 val mt = get_abbrev_match m t 95 val (l,r) = dest_abbrev mt 96in 97 PURE_REWRITE_RULE [METIS_PROVE [] ``Abbrev (x = x)``, 98 AND_CLAUSES,OR_CLAUSES,IMP_CLAUSES] (Thm.INST [l |-> r] thm) 99end; 100 101end 102