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