137 necessary. |
137 necessary. |
138 \end{warn} |
138 \end{warn} |
139 |
139 |
140 |
140 |
141 \section{Simplification sets}\index{simplification sets} |
141 \section{Simplification sets}\index{simplification sets} |
142 The simplification tactics are controlled by {\bf simpsets}. These consist |
142 The simplification tactics are controlled by {\bf simpsets}. These |
143 of five components: rewrite rules, congruence rules, the subgoaler, the |
143 consist of several components, including rewrite rules, congruence |
144 solver and the looper. The simplifier should be set up with sensible |
144 rules, the subgoaler, the solver and the looper. The simplifier |
145 defaults so that most simplifier calls specify only rewrite rules. |
145 should be set up with sensible defaults so that most simplifier calls |
146 Experienced users can exploit the other components to streamline proofs. |
146 specify only rewrite rules. Experienced users can exploit the other |
|
147 components to streamline proofs. |
147 |
148 |
148 Logics like \HOL, which support a current |
149 Logics like \HOL, which support a current |
149 simpset\index{simpset!current}, store its value in an ML reference |
150 simpset\index{simpset!current}, store its value in an ML reference |
150 variable called {\tt simpset}\index{simpset@{\tt simpset} ML value}. |
151 variable called {\tt simpset}\index{simpset@{\tt simpset} ML value}. |
151 |
152 |
372 |
373 |
373 signature SIMPLIFIER = |
374 signature SIMPLIFIER = |
374 sig |
375 sig |
375 type simpset |
376 type simpset |
376 val empty_ss: simpset |
377 val empty_ss: simpset |
377 val rep_ss: simpset -> {simps: thm list, procs: string list, |
378 val rep_ss: simpset -> {\ttlbrace}simps: thm list, procs: string list, |
378 congs: thm list, |
379 congs: thm list, |
379 subgoal_tac: simpset -> int -> tactic, |
380 subgoal_tac: simpset -> int -> tactic, |
380 loop_tac: int -> tactic, |
381 loop_tac: int -> tactic, |
381 finish_tac: thm list -> int -> tactic, |
382 finish_tac: thm list -> int -> tactic, |
382 unsafe_finish_tac: thm list -> int -> tactic} |
383 unsafe_finish_tac: thm list -> int -> tactic{\ttrbrace} |
383 val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
384 val setsubgoaler: simpset * (simpset -> int -> tactic) -> simpset |
384 val setloop: simpset * (int -> tactic) -> simpset |
385 val setloop: simpset * (int -> tactic) -> simpset |
385 val addloop: simpset * (int -> tactic) -> simpset |
386 val addloop: simpset * (int -> tactic) -> simpset |
386 val setSSolver: simpset * (thm list -> int -> tactic) -> simpset |
387 val setSSolver: simpset * (thm list -> int -> tactic) -> simpset |
387 val addSSolver: simpset * (thm list -> int -> tactic) -> simpset |
388 val addSSolver: simpset * (thm list -> int -> tactic) -> simpset |