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

author | wenzelm |

Wed, 25 Jan 2012 16:16:20 +0100 | |

changeset 46257 | 3ba3681d8930 |

parent 46256 | bc874d2ee55a |

child 46258 | 89ee3bc580a8 |

removed obscure/outdated material;

--- a/doc-src/Ref/tactic.tex Wed Jan 25 15:39:08 2012 +0100 +++ b/doc-src/Ref/tactic.tex Wed Jan 25 16:16:20 2012 +0100 @@ -38,22 +38,6 @@ \end{ttdescription} -\subsection{``Putting off'' a subgoal} -\begin{ttbox} -defer_tac : int -> tactic -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{defer_tac} {\it i}] - moves subgoal~$i$ to the last position in the proof state. It can be - useful when correcting a proof script: if the tactic given for subgoal~$i$ - fails, calling {\tt defer_tac} instead will let you continue with the rest - of the script. - - The tactic fails if subgoal~$i$ does not exist or if the proof state - contains type unknowns. -\end{ttdescription} - - \subsection{Definitions and meta-level rewriting} \label{sec:rewrite_goals} \index{tactics!meta-rewriting|bold}\index{meta-rewriting|bold} \index{definitions} @@ -68,13 +52,10 @@ There are rules for unfolding and folding definitions; Isabelle does not do this automatically. The corresponding tactics rewrite the proof state, -yielding a single next state. See also the {\tt goalw} command, which is the -easiest way of handling definitions. +yielding a single next state. \begin{ttbox} rewrite_goals_tac : thm list -> tactic -rewrite_tac : thm list -> tactic fold_goals_tac : thm list -> tactic -fold_tac : thm list -> tactic \end{ttbox} \begin{ttdescription} \item[\ttindexbold{rewrite_goals_tac} {\it defs}] @@ -82,16 +63,9 @@ leaving the main goal unchanged. Use \ttindex{SELECT_GOAL} to restrict it to a particular subgoal. -\item[\ttindexbold{rewrite_tac} {\it defs}] -unfolds the {\it defs} throughout the proof state, including the main goal ---- not normally desirable! - \item[\ttindexbold{fold_goals_tac} {\it defs}] folds the {\it defs} throughout the subgoals of the proof state, while leaving the main goal unchanged. - -\item[\ttindexbold{fold_tac} {\it defs}] -folds the {\it defs} throughout the proof state. \end{ttdescription} \begin{warn}

--- a/doc-src/Ref/tctical.tex Wed Jan 25 15:39:08 2012 +0100 +++ b/doc-src/Ref/tctical.tex Wed Jan 25 16:16:20 2012 +0100 @@ -344,16 +344,15 @@ \index{tacticals!for restriction to a subgoal} \begin{ttbox} SELECT_GOAL : tactic -> int -> tactic -METAHYPS : (thm list -> tactic) -> int -> tactic \end{ttbox} \begin{ttdescription} \item[\ttindexbold{SELECT_GOAL} {\it tac} $i$] restricts the effect of {\it tac\/} to subgoal~$i$ of the proof state. It -fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal -(do not use {\tt rewrite_tac}). It applies {\it tac\/} to a dummy proof -state and uses the result to refine the original proof state at -subgoal~$i$. If {\it tac\/} returns multiple results then so does -\hbox{\tt SELECT_GOAL {\it tac} $i$}. +fails if there is no subgoal~$i$, or if {\it tac\/} changes the main goal. +It applies {\it tac\/} to a dummy proof state and uses the result to +refine the original proof state at subgoal~$i$. If {\it tac\/} +returns multiple results then so does \hbox{\tt SELECT_GOAL {\it tac} + $i$}. {\tt SELECT_GOAL} works by creating a state of the form $\phi\Imp\phi$, with the one subgoal~$\phi$. If subgoal~$i$ has the form $\psi\Imp\theta$ @@ -363,40 +362,8 @@ SELECT_GOAL} inserts a quantifier to create the state \[ (\Forall x.\psi\Imp\theta)\Imp(\Forall x.\psi\Imp\theta). \] -\item[\ttindexbold{METAHYPS} {\it tacf} $i$]\index{meta-assumptions} -takes subgoal~$i$, of the form -\[ \Forall x@1 \ldots x@l. \List{\theta@1; \ldots; \theta@k}\Imp\theta, \] -and creates the list $\theta'@1$, \ldots, $\theta'@k$ of meta-level -assumptions. In these theorems, the subgoal's parameters ($x@1$, -\ldots,~$x@l$) become free variables. It supplies the assumptions to -$tacf$ and applies the resulting tactic to the proof state -$\theta\Imp\theta$. - -If the resulting proof state is $\List{\phi@1; \ldots; \phi@n} \Imp \phi$, -possibly containing $\theta'@1,\ldots,\theta'@k$ as assumptions, then it is -lifted back into the original context, yielding $n$ subgoals. - -Meta-level assumptions may not contain unknowns. Unknowns in the -hypotheses $\theta@1,\ldots,\theta@k$ become free variables in $\theta'@1$, -\ldots, $\theta'@k$, and are restored afterwards; the {\tt METAHYPS} call -cannot instantiate them. Unknowns in $\theta$ may be instantiated. New -unknowns in $\phi@1$, \ldots, $\phi@n$ are lifted over the parameters. - -Here is a typical application. Calling {\tt hyp_res_tac}~$i$ resolves -subgoal~$i$ with one of its own assumptions, which may itself have the form -of an inference rule (these are called {\bf higher-level assumptions}). -\begin{ttbox} -val hyp_res_tac = METAHYPS (fn prems => resolve_tac prems 1); -\end{ttbox} -The function \ttindex{gethyps} is useful for debugging applications of {\tt - METAHYPS}. \end{ttdescription} -\begin{warn} -{\tt METAHYPS} fails if the context or new subgoals contain type unknowns. -In principle, the tactical could treat these like ordinary unknowns. -\end{warn} - \subsection{Scanning for a subgoal by number} \index{tacticals!scanning for subgoals}

--- a/doc-src/Ref/thm.tex Wed Jan 25 15:39:08 2012 +0100 +++ b/doc-src/Ref/thm.tex Wed Jan 25 16:16:20 2012 +0100 @@ -143,7 +143,6 @@ nprems_of : thm -> int tpairs_of : thm -> (term*term) list theory_of_thm : thm -> theory -dest_state : thm * int -> (term*term) list * term list * term * term \end{ttbox} \begin{ttdescription} \item[\ttindexbold{cprop_of} $thm$] returns the statement of $thm$ as @@ -169,11 +168,6 @@ with $thm$. Note that this does a lookup in Isabelle's global database of loaded theories. -\item[\ttindexbold{dest_state} $(thm,i)$] -decomposes $thm$ as a tuple containing a list of flex-flex constraints, a -list of the subgoals~1 to~$i-1$, subgoal~$i$, and the rest of the theorem -(this will be an implication if there are more than $i$ subgoals). - \end{ttdescription}