summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Tue, 28 Sep 1999 14:15:57 +0200 | |

changeset 7620 | 8d721c3f4acb |

parent 7619 | d78b8b103fd9 |

child 7621 | 4074bc1e380d |

documented type solver

--- a/doc-src/Ref/simplifier.tex Tue Sep 28 13:57:33 1999 +0200 +++ b/doc-src/Ref/simplifier.tex Tue Sep 28 14:15:57 1999 +0200 @@ -222,9 +222,9 @@ print_ss : simpset -> unit rep_ss : simpset -> \{mss : meta_simpset, subgoal_tac: simpset -> int -> tactic, - loop_tac : int -> tactic, - finish_tac : thm list -> int -> tactic, - unsafe_finish_tac : thm list -> int -> tactic\} + loop_tacs : (string * (int -> tactic))list, + finish_tac : solver list, + unsafe_finish_tac : solver list\} \end{ttbox} \begin{ttdescription} @@ -536,16 +536,19 @@ \subsection{*The solver}\label{sec:simp-solver} \begin{ttbox} -setSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} -addSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} -setSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} -addSSolver : simpset * (thm list -> int -> tactic) -> simpset \hfill{\bf infix 4} +mk_solver : string -> (thm list -> int -> tactic) -> solver +setSolver : simpset * solver -> simpset \hfill{\bf infix 4} +addSolver : simpset * solver -> simpset \hfill{\bf infix 4} +setSSolver : simpset * solver -> simpset \hfill{\bf infix 4} +addSSolver : simpset * solver -> simpset \hfill{\bf infix 4} \end{ttbox} -The solver is a pair of tactics that attempt to solve a subgoal after +A solver is a tactic that attempts to solve a subgoal after simplification. Typically it just proves trivial subgoals such as \texttt{True} and $t=t$. It could use sophisticated means such as {\tt blast_tac}, though that could make simplification expensive. +To keep things more abstract, solvers are packaged up in type +\texttt{solver}. The only way to create a solver is via \texttt{mk_solver}. Rewriting does not instantiate unknowns. For example, rewriting cannot prove $a\in \Var{A}$ since this requires @@ -555,7 +558,7 @@ contains extra variables. When a simplification tactic is to be combined with other provers, especially with the classical reasoner, it is important whether it can be considered safe or not. For this -reason the solver is split into a safe and an unsafe part. +reason a simpset contains two solvers, a safe and an unsafe one. The standard simplification strategy solely uses the unsafe solver, which is appropriate in most cases. For special applications where @@ -565,7 +568,9 @@ conditional rules or congruences. \begin{ttdescription} - +\item[\ttindexbold{mk_solver} $s$ $tacf$] converts $tacf$ into a new solver; + the string $s$ is only attached as a comment and has no other significance. + \item[$ss$ \ttindexbold{setSSolver} $tacf$] installs $tacf$ as the \emph{safe} solver of $ss$.