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