1(* =====================================================================
2 * FILE        : simpLib.sig
3 * DESCRIPTION : A programmable, contextual, conditional simplifier
4 *
5 * AUTHOR      : Donald Syme
6 *               Based loosely on original HOL rewriting by
7 *               Larry Paulson et al, and on the Isabelle simplifier.
8 * =====================================================================*)
9
10
11signature simpLib =
12sig
13 include Abbrev
14
15   (* ---------------------------------------------------------------------
16    * type simpset
17    *
18    * A simpset contains:
19    *    - a collection of rewrite rules
20    *    - a collection of equational conversions
21    *    - a traversal strategy for applying them
22    *
23    * The traversal strategy may include other actions, especially
24    * decision procedures, which can work cooperatively with
25    * rewriting during simplification.
26    *
27    * REWRITE RULES
28    *
29    * Simpsets are foremost a collection of rewrite theorems stored
30    * efficiently in a termnet.  These are made into conversions
31    * by using COND_REWR_CONV.
32    *
33    * CONVERSIONS IN SIMPSETS
34    *
35    * Simpsets can contain arbitrary user conversions, as well as
36    * rewrites and contextual-rewrites.  These conversions should
37    * be thought of as infinite families of rewrites.
38    *
39    * Conversions can be keyed by term patterns (implemented
40    * using termnets).  Thus a conversion won't even be called if
41    * the target term doesn't match (in the termnet sense of matching)
42    * its key.
43    * ---------------------------------------------------------------------*)
44
45 type thname = KernelSig.kernelname
46 type convdata = { name: string,
47                    key: (term list * term) option,
48                  trace: int,
49                   conv: (term list -> term -> thm) -> term list -> conv}
50
51  type stdconvdata = { name: string,
52                       pats: term list,
53                       conv: conv}
54
55  type relsimpdata = {refl: thm,
56                      trans:thm,
57                      weakenings:thm list,
58                      subsets : thm list,
59                      rewrs : thm list}
60
61  type controlled_thm = BoundedRewrites.controlled_thm
62
63  type ssfrag
64
65  val SSFRAG :
66    {name : string option,
67     convs: convdata list,
68     rewrs: (thname option * thm) list,
69        ac: (thm * thm) list,
70    filter: (controlled_thm -> controlled_thm list) option,
71    dprocs: Traverse.reducer list,
72     congs: thm list} -> ssfrag
73
74  val empty_ssfrag : ssfrag
75  val ssf_upd_rewrs : ((thname option * thm) list -> (thname option * thm) list)
76                      ->
77                      ssfrag -> ssfrag
78  val frag_rewrites : ssfrag -> thm list
79  val frag_name : ssfrag -> string option
80
81  (*------------------------------------------------------------------------*)
82  (* Easy building of common kinds of ssfrag objects                        *)
83  (*------------------------------------------------------------------------*)
84
85  val Cong        : thm -> thm
86  val AC          : thm -> thm -> thm
87  val Excl        : string -> thm
88  val Req0        : thm -> thm
89  val ReqD        : thm -> thm
90
91  val rewrites       : thm list -> ssfrag
92  val rewrites_with_names : (thname * thm) list -> ssfrag
93  val dproc_ss       : Traverse.reducer -> ssfrag
94  val ac_ss          : (thm * thm) list -> ssfrag
95  val conv_ss        : convdata -> ssfrag
96  val relsimp_ss     : relsimpdata -> ssfrag
97  val std_conv_ss    : stdconvdata -> ssfrag
98  val merge_ss       : ssfrag list -> ssfrag
99  val name_ss        : string -> ssfrag -> ssfrag
100  val named_rewrites : string -> thm list -> ssfrag
101  val named_rewrites_with_names : string -> (thname * thm) list -> ssfrag
102  val named_merge_ss : string -> ssfrag list -> ssfrag
103  val type_ssfrag    : hol_type -> ssfrag
104  val tyi_to_ssdata  : TypeBasePure.tyinfo -> ssfrag
105
106  val partition_ssfrags : string list -> ssfrag list ->
107                          (ssfrag list * ssfrag list)
108
109   (* ---------------------------------------------------------------------
110    * mk_simpset: Joins several ssfrag fragments to make a simpset.
111    * This is a "runtime" object - the ssfrag can be thought of as the
112    * static, data objects.
113    * Beware of duplicating information - you should only
114    * merge distinct ssfrag fragments! (like BOOL_ss and PURE_ss).
115    * You cannot merge simpsets with lower-case names (like bool_ss).
116    *
117    * The order of the merge is significant w.r.t. congruence rules
118    * and rewrite makers.
119    * ---------------------------------------------------------------------*)
120
121  type simpset
122  type weakener_data = Travrules.preorder list * thm list * Traverse.reducer
123
124  val empty_ss        : simpset
125  val ssfrags_of      : simpset -> ssfrag list
126  val mk_simpset      : ssfrag list -> simpset
127  val remove_ssfrags  : string list -> simpset -> simpset
128  val ssfrag_names_of : simpset -> string list
129  val ++              : simpset * ssfrag -> simpset  (* infix *)
130  val -*              : simpset * string list -> simpset (* infix *)
131  val &&              : simpset * thm list -> simpset  (* infix *)
132  val limit           : int -> simpset -> simpset
133  val unlimit         : simpset -> simpset
134  val add_named_rwt   : (thname * thm) -> ssfrag -> ssfrag
135
136  val add_weakener : weakener_data -> simpset -> simpset
137
138  val add_relsimp  : relsimpdata -> simpset -> simpset
139
140  val traversedata_for_ss: simpset -> Traverse.traverse_data
141
142
143   (* ---------------------------------------------------------------------
144    * SIMP_CONV : simpset -> conv
145    *
146    * SIMP_CONV makes a simplification conversion from the given simpset.  The
147    * conversion uses a top-depth strategy for rewriting.  It sets both
148    * the solver and the depther to be SIMP_CONV itself.
149    *
150    * FAILURE CONDITIONS
151    *
152    * SIMP_CONV never fails, though it may diverge.  Beware of
153    * divergence when trying to solve conditions to conditional rewrites.
154    * ---------------------------------------------------------------------*)
155
156   val SIMP_PROVE : simpset -> thm list -> term -> thm
157   val SIMP_CONV  : simpset -> thm list -> conv
158
159   (* ---------------------------------------------------------------------
160    * SIMP_TAC : simpset -> tactic
161    * ASM_SIMP_TAC : simpset -> tactic
162    * FULL_SIMP_TAC : simpset -> tactic
163    *
164    * SIMP_TAC makes a simplification tactic from the given simpset.  The
165    * tactic uses a top-depth strategy for rewriting, and will be recursively
166    * reapplied when a simplification step makes a change to a term.
167    * This is done in the same way as similar to TOP_DEPTH_CONV.
168    *
169    * ASM_SIMP_TAC draws extra rewrites (conditional and unconditional)
170    * from the assumption list.  These are also added to the context that
171    * will be passed to conversions.
172    *
173    * FULL_SIMP_TAC simplifies the assumptions one by one, before
174    * simplifying the goal.  The assumptions are simplified in the order
175    * that they are found in the assumption list, and the simplification
176    * of each assumption is used when simplifying the next assumption.
177    *
178    * FAILURE CONDITIONS
179    *
180    * These tactics never fail, though they may diverge.
181    * ---------------------------------------------------------------------*)
182
183   val SIMP_TAC      : simpset -> thm list -> tactic
184   val simp_tac      : simpset -> thm list -> tactic
185   val ASM_SIMP_TAC  : simpset -> thm list -> tactic
186   val asm_simp_tac  : simpset -> thm list -> tactic
187   val FULL_SIMP_TAC : simpset -> thm list -> tactic
188   val full_simp_tac : simpset -> thm list -> tactic
189
190   val REV_FULL_SIMP_TAC          : simpset -> thm list -> tactic
191   val rev_full_simp_tac          : simpset -> thm list -> tactic
192   val NO_STRIP_FULL_SIMP_TAC     : simpset -> thm list -> tactic
193   val NO_STRIP_REV_FULL_SIMP_TAC : simpset -> thm list -> tactic
194
195   type simptac_config = {strip : bool, elimvars : bool, droptrues : bool}
196   val psr : simptac_config -> simpset -> tactic
197     (* Pop, Simp, Rotate to back *)
198   val allasms : simptac_config -> simpset -> tactic
199     (* do the above to all the assumptions in turn *)
200   val global_simp_tac : simptac_config -> simpset -> thm list -> tactic
201     (* do allasms until quiescence, then simp in the goal as well *)
202
203   (* ---------------------------------------------------------------------
204    * SIMP_RULE : simpset -> tactic
205    * ASM_SIMP_RULE : simpset -> tactic
206    *
207    * Make a simplification rule from the given simpset.  The
208    * rule uses a top-depth strategy for rewriting.
209    *
210    * FAILURE CONDITIONS
211    *
212    * These rules never fail, though they may diverge.
213    * ---------------------------------------------------------------------*)
214
215   val SIMP_RULE     : simpset -> thm list -> thm -> thm
216   val ASM_SIMP_RULE : simpset -> thm list -> thm -> thm
217
218   (* ---------------------------------------------------------------------*)
219   (* Accumulating the rewrite rules that are actually used.               *)
220   (* ---------------------------------------------------------------------*)
221
222   val used_rewrites : thm list ref
223   val track_rewrites : bool ref
224
225   val track : ('a -> 'b) -> 'a -> 'b
226
227   (* ---------------------------------------------------------------------*)
228   (* Prettyprinters for ssfrags and simpsets.                             *)
229   (* ---------------------------------------------------------------------*)
230
231   val pp_ssfrag : ssfrag Parse.pprinter
232   val pp_simpset : simpset Parse.pprinter
233
234end
235