# HG changeset patch # User wenzelm # Date 1327525275 -3600 # Node ID a87e06a18a5c46d12b1d9fb83f47050ce04c874e # Parent 912b42e64fdefd403c194369e9f83ea9cbb1b9f0 updated "subgoal quantifiers"; diff -r 912b42e64fde -r a87e06a18a5c doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 21:14:00 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 22:01:15 2012 +0100 @@ -586,4 +586,66 @@ fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; *} + +subsection {* Scanning for a subgoal by number *} + +text {* Tactics with explicit subgoal addressing + @{ML_type "int -> tactic"} can be used together with tacticals that + act like ``subgoal quantifiers'': guided by success of the body + tactic a certain range of subgoals is covered. Thus the body tactic + is applied to all subgoals, for example. + + Suppose that the goal state has @{text "n \ 0"} subgoals. Many of + these tacticals address subgoal ranges counting downwards from + @{text "n"} towards @{text "1"}. This has the fortunate effect that + newly emerging subgoals are concatenated in the result, without + interfering each other. Nonetheless, there might be situations + where a different order is desired, but it has to be achieved by + other means. *} + +text %mlref {* + \begin{mldecls} + @{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\ + @{index_ML TRYALL: "(int -> tactic) -> tactic"} \\ + @{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\ + @{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\ + @{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\ + @{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\ + @{index_ML trace_goalno_tac: "(int -> tactic) -> int -> tactic"} \\ + \end{mldecls} + + \begin{description} + + \item @{ML ALLGOALS}~@{text "tac"} is equivalent to @{text "tac + n"}~@{ML_op THEN}~@{text "\"}~@{ML_op THEN}~@{text "tac 1"}. It + applies the @{text tac} to all the subgoals, counting downwards. + + \item @{ML TRYALL}~@{text "tac"} is equivalent to @{ML TRY}~@{text + "(tac n)"}~@{ML_op THEN}~@{text "\"}~@{ML_op THEN}~@{ML TRY}~@{text + "(tac 1)"}. It attempts to apply @{text "tac"} to all the subgoals. + + \item @{ML SOMEGOAL}~@{text "tac"} is equivalent to @{text "tac + n"}~@{ML_op ORELSE}~@{text "\"}~@{ML_op ORELSE}~@{text "tac 1"}. It + applies @{text "tac"} to one subgoal, counting downwards. + + \item @{ML FIRSTGOAL}~@{text "tac"} is equivalent to @{text "tac + 1"}~@{ML_op ORELSE}~@{text "\"}~@{ML_op ORELSE}~@{text "tac n"}. It + applies @{text "tac"} to one subgoal, counting upwards. + + \item @{ML REPEAT_SOME}~@{text "tac"} applies @{text "tac"} once or + more to a subgoal, counting downwards. + + \item @{ML REPEAT_FIRST}~@{text "tac"} applies @{text "tac"} once or + more to a subgoal, counting upwards. + + \item @{ML trace_goalno_tac}~@{text "tac i"} applies @{text "tac i"} + to the proof state. If the resulting sequence is non-empty, then it + is returned, with the side-effect of printing the selected subgoal. + Otherwise, it fails and prints nothing. It indicates that ``the + tactic worked for subgoal @{text "i"}'' and is mainly used with @{ML + SOMEGOAL} and @{ML FIRSTGOAL}. + + \end{description} +*} + end diff -r 912b42e64fde -r a87e06a18a5c doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 21:14:00 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 22:01:15 2012 +0100 @@ -728,10 +728,82 @@ \isadelimML % \endisadelimML -\isanewline +% +\isamarkupsubsection{Scanning for a subgoal by number% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Tactics with explicit subgoal addressing + \verb|int -> tactic| can be used together with tacticals that + act like ``subgoal quantifiers'': guided by success of the body + tactic a certain range of subgoals is covered. Thus the body tactic + is applied to all subgoals, for example. + + Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals. Many of + these tacticals address subgoal ranges counting downwards from + \isa{n} towards \isa{{\isadigit{1}}}. This has the fortunate effect that + newly emerging subgoals are concatenated in the result, without + interfering each other. Nonetheless, there might be situations + where a different order is desired, but it has to be achieved by + other means.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{TRYALL}\verb|TRYALL: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{REPEAT\_SOME}\verb|REPEAT_SOME: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{REPEAT\_FIRST}\verb|REPEAT_FIRST: (int -> tactic) -> tactic| \\ + \indexdef{}{ML}{trace\_goalno\_tac}\verb|trace_goalno_tac: (int -> tactic) -> int -> tactic| \\ + \end{mldecls} + + \begin{description} + + \item \verb|ALLGOALS|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\ {\isadigit{1}}}. It + applies the \isa{tac} to all the subgoals, counting downwards. + + \item \verb|TRYALL|~\isa{tac} is equivalent to \verb|TRY|~\isa{{\isaliteral{28}{\isacharparenleft}}tac\ n{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\verb|TRY|~\isa{{\isaliteral{28}{\isacharparenleft}}tac\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}. It attempts to apply \isa{tac} to all the subgoals. + + \item \verb|SOMEGOAL|~\isa{tac} is equivalent to \isa{tac\ n}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ {\isadigit{1}}}. It + applies \isa{tac} to one subgoal, counting downwards. + + \item \verb|FIRSTGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}~\verb|ORELSE|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|ORELSE|~\isa{tac\ n}. It + applies \isa{tac} to one subgoal, counting upwards. + + \item \verb|REPEAT_SOME|~\isa{tac} applies \isa{tac} once or + more to a subgoal, counting downwards. + + \item \verb|REPEAT_FIRST|~\isa{tac} applies \isa{tac} once or + more to a subgoal, counting upwards. + + \item \verb|trace_goalno_tac|~\isa{tac\ i} applies \isa{tac\ i} + to the proof state. If the resulting sequence is non-empty, then it + is returned, with the side-effect of printing the selected subgoal. + Otherwise, it fails and prints nothing. It indicates that ``the + tactic worked for subgoal \isa{i}'' and is mainly used with \verb|SOMEGOAL| and \verb|FIRSTGOAL|. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref % \isadelimtheory -\isanewline % \endisadelimtheory % diff -r 912b42e64fde -r a87e06a18a5c doc-src/Ref/tctical.tex --- a/doc-src/Ref/tctical.tex Wed Jan 25 21:14:00 2012 +0100 +++ b/doc-src/Ref/tctical.tex Wed Jan 25 22:01:15 2012 +0100 @@ -204,71 +204,6 @@ \end{ttdescription} - -\subsection{Scanning for a subgoal by number} -\index{tacticals!scanning for subgoals} -\begin{ttbox} -ALLGOALS : (int -> tactic) -> tactic -TRYALL : (int -> tactic) -> tactic -SOMEGOAL : (int -> tactic) -> tactic -FIRSTGOAL : (int -> tactic) -> tactic -REPEAT_SOME : (int -> tactic) -> tactic -REPEAT_FIRST : (int -> tactic) -> tactic -trace_goalno_tac : (int -> tactic) -> int -> tactic -\end{ttbox} -These apply a tactic function of type {\tt int -> tactic} to all the -subgoal numbers of a proof state, and join the resulting tactics using -\ttindex{THEN} or \ttindex{ORELSE}\@. Thus, they apply the tactic to all the -subgoals, or to one subgoal. - -Suppose that the original proof state has $n$ subgoals. - -\begin{ttdescription} -\item[\ttindexbold{ALLGOALS} {\it tacf}] -is equivalent to -\hbox{\tt$tacf(n)$ THEN \ldots{} THEN $tacf(1)$}. - -It applies {\it tacf} to all the subgoals, counting downwards (to -avoid problems when subgoals are added or deleted). - -\item[\ttindexbold{TRYALL} {\it tacf}] -is equivalent to -\hbox{\tt TRY$(tacf(n))$ THEN \ldots{} THEN TRY$(tacf(1))$}. - -It attempts to apply {\it tacf} to all the subgoals. For instance, -the tactic \hbox{\tt TRYALL assume_tac} attempts to solve all the subgoals by -assumption. - -\item[\ttindexbold{SOMEGOAL} {\it tacf}] -is equivalent to -\hbox{\tt$tacf(n)$ ORELSE \ldots{} ORELSE $tacf(1)$}. - -It applies {\it tacf} to one subgoal, counting downwards. For instance, -the tactic \hbox{\tt SOMEGOAL assume_tac} solves one subgoal by assumption, -failing if this is impossible. - -\item[\ttindexbold{FIRSTGOAL} {\it tacf}] -is equivalent to -\hbox{\tt$tacf(1)$ ORELSE \ldots{} ORELSE $tacf(n)$}. - -It applies {\it tacf} to one subgoal, counting upwards. - -\item[\ttindexbold{REPEAT_SOME} {\it tacf}] -applies {\it tacf} once or more to a subgoal, counting downwards. - -\item[\ttindexbold{REPEAT_FIRST} {\it tacf}] -applies {\it tacf} once or more to a subgoal, counting upwards. - -\item[\ttindexbold{trace_goalno_tac} {\it tac} {\it i}] -applies \hbox{\it tac i\/} to the proof state. If the resulting sequence -is non-empty, then it is returned, with the side-effect of printing {\tt -Subgoal~$i$ selected}. Otherwise, {\tt trace_goalno_tac} returns the empty -sequence and prints nothing. - -It indicates that `the tactic worked for subgoal~$i$' and is mainly used -with {\tt SOMEGOAL} and {\tt FIRSTGOAL}. -\end{ttdescription} - \index{tacticals|)}