--- a/doc-src/IsarImplementation/Thy/Isar.thy Thu Jan 26 15:29:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Isar.thy Thu Jan 26 21:16:11 2012 +0100
@@ -311,7 +311,6 @@
@{index_ML METHOD: "(thm list -> tactic) -> Proof.method"} \\
@{index_ML SIMPLE_METHOD: "tactic -> Proof.method"} \\
@{index_ML SIMPLE_METHOD': "(int -> tactic) -> Proof.method"} \\
- @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
@{index_ML Method.insert_tac: "thm list -> int -> tactic"} \\
@{index_ML Method.setup: "binding -> (Proof.context -> Proof.method) context_parser ->
string -> theory -> theory"} \\
@@ -336,13 +335,9 @@
applied.
\item @{ML SIMPLE_METHOD'}~@{text "tactic"} wraps a tactic that
- addresses a specific subgoal as simple proof method. Goal facts are
- already inserted into the first subgoal before @{text "tactic"} is
- applied to the same.
-
- \item @{ML HEADGOAL}~@{text "tactic"} applies @{text "tactic"} to
- the first subgoal. This is convenient to reproduce part the @{ML
- SIMPLE_METHOD'} wrapping within regular @{ML METHOD}, for example.
+ addresses a specific subgoal as simple proof method that operates on
+ subgoal 1. Goal facts are inserted into the subgoal then the @{text
+ "tactic"} is applied.
\item @{ML Method.insert_tac}~@{text "facts i"} inserts @{text
"facts"} into subgoal @{text "i"}. This is convenient to reproduce
--- a/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 15:29:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 21:16:11 2012 +0100
@@ -575,13 +575,13 @@
*}
-subsection {* Scanning for a subgoal by number *}
+subsection {* Applying tactics to subgoal ranges *}
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.
+ is applied to \emph{all} subgoals, \emph{some} subgoal etc.
Suppose that the goal state has @{text "n \<ge> 0"} subgoals. Many of
these tacticals address subgoal ranges counting downwards from
@@ -595,8 +595,10 @@
@{index_ML ALLGOALS: "(int -> tactic) -> tactic"} \\
@{index_ML SOMEGOAL: "(int -> tactic) -> tactic"} \\
@{index_ML FIRSTGOAL: "(int -> tactic) -> tactic"} \\
+ @{index_ML HEADGOAL: "(int -> tactic) -> tactic"} \\
@{index_ML REPEAT_SOME: "(int -> tactic) -> tactic"} \\
@{index_ML REPEAT_FIRST: "(int -> tactic) -> tactic"} \\
+ @{index_ML RANGE: "(int -> tactic) list -> int -> tactic"} \\
\end{mldecls}
\begin{description}
@@ -613,12 +615,20 @@
1"}~@{ML_op ORELSE}~@{text "\<dots>"}~@{ML_op ORELSE}~@{text "tac n"}. It
applies @{text "tac"} to one subgoal, counting upwards.
+ \item @{ML HEADGOAL}~@{text "tac"} is equivalent to @{text "tac 1"}.
+ It applies @{text "tac"} unconditionally to the first subgoal.
+
\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 RANGE}~@{text "[tac\<^sub>1, \<dots>, tac\<^sub>k] i"} is equivalent to
+ @{text "tac\<^sub>k (i + k - 1)"}~@{ML_op THEN}~@{text "\<dots>"}~@{ML_op
+ THEN}~@{text "tac\<^sub>1 i"}. It applies the given list of tactics to the
+ corresponding range of subgoals, counting downwards.
+
\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/document/Isar.tex Thu Jan 26 15:29:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Isar.tex Thu Jan 26 21:16:11 2012 +0100
@@ -428,7 +428,6 @@
\indexdef{}{ML}{METHOD}\verb|METHOD: (thm list -> tactic) -> Proof.method| \\
\indexdef{}{ML}{SIMPLE\_METHOD}\verb|SIMPLE_METHOD: tactic -> Proof.method| \\
\indexdef{}{ML}{SIMPLE\_METHOD'}\verb|SIMPLE_METHOD': (int -> tactic) -> Proof.method| \\
- \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{Method.insert\_tac}\verb|Method.insert_tac: thm list -> int -> tactic| \\
\indexdef{}{ML}{Method.setup}\verb|Method.setup: binding -> (Proof.context -> Proof.method) context_parser ->|\isasep\isanewline%
\verb| string -> theory -> theory| \\
@@ -452,12 +451,8 @@
applied.
\item \verb|SIMPLE_METHOD'|~\isa{tactic} wraps a tactic that
- addresses a specific subgoal as simple proof method. Goal facts are
- already inserted into the first subgoal before \isa{tactic} is
- applied to the same.
-
- \item \verb|HEADGOAL|~\isa{tactic} applies \isa{tactic} to
- the first subgoal. This is convenient to reproduce part the \verb|SIMPLE_METHOD'| wrapping within regular \verb|METHOD|, for example.
+ addresses a specific subgoal as simple proof method that operates on
+ subgoal 1. Goal facts are inserted into the subgoal then the \isa{tactic} is applied.
\item \verb|Method.insert_tac|~\isa{facts\ i} inserts \isa{facts} into subgoal \isa{i}. This is convenient to reproduce
part of the \verb|SIMPLE_METHOD| or \verb|SIMPLE_METHOD'| wrapping
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 15:29:11 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 21:16:11 2012 +0100
@@ -715,7 +715,7 @@
%
\endisadelimML
%
-\isamarkupsubsection{Scanning for a subgoal by number%
+\isamarkupsubsection{Applying tactics to subgoal ranges%
}
\isamarkuptrue%
%
@@ -724,7 +724,7 @@
\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.
+ is applied to \emph{all} subgoals, \emph{some} subgoal etc.
Suppose that the goal state has \isa{n\ {\isaliteral{5C3C67653E}{\isasymge}}\ {\isadigit{0}}} subgoals. Many of
these tacticals address subgoal ranges counting downwards from
@@ -746,8 +746,10 @@
\indexdef{}{ML}{ALLGOALS}\verb|ALLGOALS: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{SOMEGOAL}\verb|SOMEGOAL: (int -> tactic) -> tactic| \\
\indexdef{}{ML}{FIRSTGOAL}\verb|FIRSTGOAL: (int -> tactic) -> tactic| \\
+ \indexdef{}{ML}{HEADGOAL}\verb|HEADGOAL: (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}{RANGE}\verb|RANGE: (int -> tactic) list -> int -> tactic| \\
\end{mldecls}
\begin{description}
@@ -761,12 +763,19 @@
\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|HEADGOAL|~\isa{tac} is equivalent to \isa{tac\ {\isadigit{1}}}.
+ It applies \isa{tac} unconditionally to the first subgoal.
+
\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|RANGE|~\isa{{\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k{\isaliteral{5D}{\isacharbrackright}}\ i} is equivalent to
+ \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub k\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}}~\verb|THEN|~\isa{{\isaliteral{5C3C646F74733E}{\isasymdots}}}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}. It applies the given list of tactics to the
+ corresponding range of subgoals, counting downwards.
+
\end{description}%
\end{isamarkuptext}%
\isamarkuptrue%