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