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 convdata = { name: string,
46                     key: (term list * term) option,
47                   trace: int,
48                    conv: (term list -> term -> thm) -> term list -> conv}
49
50  type stdconvdata = { name: string,
51                       pats: term list,
52                       conv: conv}
53
54  type relsimpdata = {refl: thm,
55                      trans:thm,
56                      weakenings:thm list,
57                      subsets : thm list,
58                      rewrs : thm list}
59
60  type controlled_thm = BoundedRewrites.controlled_thm
61
62  type ssfrag
63
64  val SSFRAG :
65    {name : string option,
66     convs: convdata list,
67     rewrs: thm list,
68        ac: (thm * thm) list,
69    filter: (controlled_thm -> controlled_thm list) option,
70    dprocs: Traverse.reducer list,
71     congs: thm list} -> ssfrag
72
73  val frag_rewrites : ssfrag -> thm list
74
75  (*------------------------------------------------------------------------*)
76  (* Easy building of common kinds of ssfrag objects                        *)
77  (*------------------------------------------------------------------------*)
78
79  val Cong        : thm -> thm
80  val AC          : thm -> thm -> thm
81
82  val rewrites       : thm list -> ssfrag
83  val dproc_ss       : Traverse.reducer -> ssfrag
84  val ac_ss          : (thm * thm) list -> ssfrag
85  val conv_ss        : convdata -> ssfrag
86  val relsimp_ss     : relsimpdata -> ssfrag
87  val std_conv_ss    : stdconvdata -> ssfrag
88  val merge_ss       : ssfrag list -> ssfrag
89  val name_ss        : string -> ssfrag -> ssfrag
90  val named_rewrites : string -> thm list -> ssfrag
91  val named_merge_ss : string -> ssfrag list -> ssfrag
92  val type_ssfrag    : hol_type -> ssfrag
93
94  val partition_ssfrags : string list -> ssfrag list ->
95                          (ssfrag list * ssfrag list)
96
97   (* ---------------------------------------------------------------------
98    * mk_simpset: Joins several ssfrag fragments to make a simpset.
99    * This is a "runtime" object - the ssfrag can be thought of as the
100    * static, data objects.
101    * Beware of duplicating information - you should only
102    * merge distinct ssfrag fragments! (like BOOL_ss and PURE_ss).
103    * You cannot merge simpsets with lower-case names (like bool_ss).
104    *
105    * The order of the merge is significant w.r.t. congruence rules
106    * and rewrite makers.
107    * ---------------------------------------------------------------------*)
108
109  type simpset
110
111  val empty_ss        : simpset
112  val ssfrags_of      : simpset -> ssfrag list
113  val mk_simpset      : ssfrag list -> simpset
114  val remove_ssfrags  : simpset -> string list -> simpset
115  val remove_theorems : term list -> simpset -> simpset
116  val ssfrag_names_of : simpset -> string list
117  val ++              : simpset * ssfrag -> simpset  (* infix *)
118  val &&              : simpset * thm list -> simpset  (* infix *)
119  val limit           : int -> simpset -> simpset
120  val unlimit         : simpset -> simpset
121
122  val add_weakener : (Travrules.preorder list * thm list * Traverse.reducer) ->
123                     simpset -> simpset
124
125  val add_relsimp  : relsimpdata -> simpset -> simpset
126
127  val traversedata_for_ss: simpset -> Traverse.traverse_data
128
129
130   (* ---------------------------------------------------------------------
131    * SIMP_CONV : simpset -> conv
132    *
133    * SIMP_CONV makes a simplification conversion from the given simpset.  The
134    * conversion uses a top-depth strategy for rewriting.  It sets both
135    * the solver and the depther to be SIMP_CONV itself.
136    *
137    * FAILURE CONDITIONS
138    *
139    * SIMP_CONV never fails, though it may diverge.  Beware of
140    * divergence when trying to solve conditions to conditional rewrites.
141    * ---------------------------------------------------------------------*)
142
143   val SIMP_PROVE : simpset -> thm list -> term -> thm
144   val SIMP_CONV  : simpset -> thm list -> conv
145
146   (* ---------------------------------------------------------------------
147    * SIMP_TAC : simpset -> tactic
148    * ASM_SIMP_TAC : simpset -> tactic
149    * FULL_SIMP_TAC : simpset -> tactic
150    *
151    * SIMP_TAC makes a simplification tactic from the given simpset.  The
152    * tactic uses a top-depth strategy for rewriting, and will be recursively
153    * reapplied when a simplification step makes a change to a term.
154    * This is done in the same way as similar to TOP_DEPTH_CONV.
155    *
156    * ASM_SIMP_TAC draws extra rewrites (conditional and unconditional)
157    * from the assumption list.  These are also added to the context that
158    * will be passed to conversions.
159    *
160    * FULL_SIMP_TAC simplifies the assumptions one by one, before
161    * simplifying the goal.  The assumptions are simplified in the order
162    * that they are found in the assumption list, and the simplification
163    * of each assumption is used when simplifying the next assumption.
164    *
165    * FAILURE CONDITIONS
166    *
167    * These tactics never fail, though they may diverge.
168    * ---------------------------------------------------------------------*)
169
170   val SIMP_TAC      : simpset -> thm list -> tactic
171   val simp_tac      : simpset -> thm list -> tactic
172   val ASM_SIMP_TAC  : simpset -> thm list -> tactic
173   val asm_simp_tac  : simpset -> thm list -> tactic
174   val FULL_SIMP_TAC : simpset -> thm list -> tactic
175   val full_simp_tac : simpset -> thm list -> tactic
176
177   val REV_FULL_SIMP_TAC          : simpset -> thm list -> tactic
178   val rev_full_simp_tac          : simpset -> thm list -> tactic
179   val NO_STRIP_FULL_SIMP_TAC     : simpset -> thm list -> tactic
180   val NO_STRIP_REV_FULL_SIMP_TAC : simpset -> thm list -> tactic
181
182   (* ---------------------------------------------------------------------
183    * SIMP_RULE : simpset -> tactic
184    * ASM_SIMP_RULE : simpset -> tactic
185    *
186    * Make a simplification rule from the given simpset.  The
187    * rule uses a top-depth strategy for rewriting.
188    *
189    * FAILURE CONDITIONS
190    *
191    * These rules never fail, though they may diverge.
192    * ---------------------------------------------------------------------*)
193
194   val SIMP_RULE     : simpset -> thm list -> thm -> thm
195   val ASM_SIMP_RULE : simpset -> thm list -> thm -> thm
196
197   (* ---------------------------------------------------------------------*)
198   (* Accumulating the rewrite rules that are actually used.               *)
199   (* ---------------------------------------------------------------------*)
200
201   val used_rewrites : thm list ref
202   val track_rewrites : bool ref
203
204   val track : ('a -> 'b) -> 'a -> 'b
205
206   (* ---------------------------------------------------------------------*)
207   (* Prettyprinters for ssfrags and simpsets.                             *)
208   (* ---------------------------------------------------------------------*)
209
210   val pp_ssfrag : ssfrag Parse.pprinter
211   val pp_simpset : simpset Parse.pprinter
212
213end
214