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

author | oheimb |

Fri, 27 Oct 2000 15:53:47 +0200 | |

changeset 10347 | c0cfc4ac12e2 |

parent 10346 | 4dce06387aea |

child 10348 | a5653826379e |

added instantiate_tac

doc-src/Ref/tactic.tex | file | annotate | diff | comparison | revisions | |

src/Pure/tactic.ML | file | annotate | diff | comparison | revisions |

--- a/doc-src/Ref/tactic.tex Fri Oct 27 15:23:39 2000 +0200 +++ b/doc-src/Ref/tactic.tex Fri Oct 27 15:53:47 2000 +0200 @@ -105,20 +105,24 @@ \end{ttdescription} -\subsection{Resolution with instantiation} \label{res_inst_tac} +\subsection{Explicit instantiation} \label{res_inst_tac} \index{tactics!instantiation}\index{instantiation} \begin{ttbox} -res_inst_tac : (string*string)list -> thm -> int -> tactic -eres_inst_tac : (string*string)list -> thm -> int -> tactic -dres_inst_tac : (string*string)list -> thm -> int -> tactic -forw_inst_tac : (string*string)list -> thm -> int -> tactic +res_inst_tac : (string*string)list -> thm -> int -> tactic +eres_inst_tac : (string*string)list -> thm -> int -> tactic +dres_inst_tac : (string*string)list -> thm -> int -> tactic +forw_inst_tac : (string*string)list -> thm -> int -> tactic +instantiate_tac : (string*string)list -> tactic \end{ttbox} -These tactics are designed for applying rules such as substitution and -induction, which cause difficulties for higher-order unification. The -tactics accept explicit instantiations for unknowns in the rule --- -typically, in the rule's conclusion. Each instantiation is a pair -{\tt($v$,$e$)}, where $v$ is an unknown \emph{without} its leading -question mark! +The first four of these tactics are designed for applying rules by resolution +such as substitution and induction, which cause difficulties for higher-order +unification. The tactics accept explicit instantiations for unknowns +in the rule ---typically, in the rule's conclusion. The last one, +{\tt instantiate_tac}, may be used to instantiate unknowns in the proof state, +independently of rule application. + +Each instantiation is a pair {\tt($v$,$e$)}, +where $v$ is an unknown \emph{without} its leading question mark! \begin{itemize} \item If $v$ is the type unknown {\tt'a}, then the rule must contain a type unknown \verb$?'a$ of some @@ -138,7 +142,7 @@ \texttt{[("t","True")]}. Type unknowns in the proof state may cause failure because the tactics cannot instantiate them. -The instantiation tactics act on a given subgoal. Terms in the +The first four instantiation tactics act on a given subgoal. Terms in the instantiations are type-checked in the context of that subgoal --- in particular, they may refer to that subgoal's parameters. Any unknowns in the terms receive subscripts and are lifted over the parameters; thus, you @@ -161,6 +165,10 @@ is like {\tt dres_inst_tac} except that the selected assumption is not deleted. It applies the instantiated rule to an assumption, adding the result as a new assumption. + +\item[\ttindexbold{instantiate_tac} {\it insts}] +instantiates unknowns in the proof state. This affects the main goal as +well as all subgoals. \end{ttdescription}

--- a/src/Pure/tactic.ML Fri Oct 27 15:23:39 2000 +0200 +++ b/src/Pure/tactic.ML Fri Oct 27 15:53:47 2000 +0200 @@ -96,6 +96,7 @@ val term_lift_inst_rule : thm * int * (indexname*typ)list * ((indexname*typ)*term)list * thm -> thm + val instantiate_tac : (string * string) list -> tactic val thin_tac : string -> int -> tactic val trace_goalno_tac : (int -> tactic) -> int -> tactic end; @@ -305,6 +306,9 @@ (*dresolve tactic applies a RULE to replace an assumption*) fun dres_inst_tac sinsts rule = eres_inst_tac sinsts (make_elim_preserve rule); +(*instantiate variables in the whole state*) +val instantiate_tac = PRIMITIVE o read_instantiate; + (*Deletion of an assumption*) fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;