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