--- a/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 15:28:17 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Tactic.thy Thu Jan 26 15:29:11 2012 +0100
@@ -470,7 +470,7 @@
always fails.
\item @{ML_op "THEN'"} is the lifted version of @{ML_op "THEN"}, for
- tactics with explicit subgoal addressing. Thus @{text
+ tactics with explicit subgoal addressing. So @{text
"(tac\<^sub>1"}~@{ML_op THEN'}~@{text "tac\<^sub>2) i"} is the same as @{text
"(tac\<^sub>1 i"}~@{ML_op THEN}~@{text "tac\<^sub>2 i)"}.
@@ -489,11 +489,10 @@
text %mlref {*
\begin{mldecls}
@{index_ML "TRY": "tactic -> tactic"} \\
+ @{index_ML "REPEAT": "tactic -> tactic"} \\
+ @{index_ML "REPEAT1": "tactic -> tactic"} \\
@{index_ML "REPEAT_DETERM": "tactic -> tactic"} \\
@{index_ML "REPEAT_DETERM_N": "int -> tactic -> tactic"} \\
- @{index_ML "REPEAT": "tactic -> tactic"} \\
- @{index_ML "REPEAT1": "tactic -> tactic"} \\
- @{index_ML "DETERM_UNTIL": "(thm -> bool) -> tactic -> tactic"} \\
\end{mldecls}
\begin{description}
@@ -503,14 +502,9 @@
returns the original state. Thus, it applies @{text "tac"} at most
once.
- \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
- proof state and, recursively, to the head of the resulting sequence.
- It returns the first state to make @{text "tac"} fail. It is
- deterministic, discarding alternative outcomes.
-
- \item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML
- REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound
- by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).
+ Note that for tactics with subgoal addressing, the combinator can be
+ applied via functional composition: @{ML "TRY"}~@{ML_op o}~@{text
+ "tac"}. There is no need for @{verbatim TRY'}.
\item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the proof
state and, recursively, to each element of the resulting sequence.
@@ -524,12 +518,14 @@
but it always applies @{text "tac"} at least once, failing if this
is impossible.
- \item @{ML DETERM_UNTIL}~@{text "P tac"} applies @{text "tac"} to
- the proof state and, recursively, to the head of the resulting
- sequence, until the predicate @{text "P"} (applied on the proof
- state) yields @{ML true}. It fails if @{text "tac"} fails on any of
- the intermediate states. It is deterministic, discarding alternative
- outcomes.
+ \item @{ML REPEAT_DETERM}~@{text "tac"} applies @{text "tac"} to the
+ proof state and, recursively, to the head of the resulting sequence.
+ It returns the first state to make @{text "tac"} fail. It is
+ deterministic, discarding alternative outcomes.
+
+ \item @{ML REPEAT_DETERM_N}~@{text "n tac"} is like @{ML
+ REPEAT_DETERM}~@{text "tac"} but the number of repetitions is bound
+ by @{text "n"} (where @{ML "~1"} means @{text "\<infinity>"}).
\end{description}
*}
@@ -592,18 +588,15 @@
@{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. *}
+ where a different order is desired. *}
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}
@@ -612,10 +605,6 @@
n"}~@{ML_op THEN}~@{text "\<dots>"}~@{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 "\<dots>"}~@{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 "\<dots>"}~@{ML_op ORELSE}~@{text "tac 1"}. It
applies @{text "tac"} to one subgoal, counting downwards.
@@ -630,13 +619,6 @@
\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}
*}
--- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 15:28:17 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Thu Jan 26 15:29:11 2012 +0100
@@ -553,7 +553,7 @@
always fails.
\item \verb|THEN'| is the lifted version of \verb|THEN|, for
- tactics with explicit subgoal addressing. Thus \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}}.
+ tactics with explicit subgoal addressing. So \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}}~\verb|THEN'|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ i} is the same as \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ i}~\verb|THEN|~\isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}}.
The other primed tacticals work analogously.
@@ -588,11 +588,10 @@
\begin{isamarkuptext}%
\begin{mldecls}
\indexdef{}{ML}{TRY}\verb|TRY: tactic -> tactic| \\
+ \indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\
+ \indexdef{}{ML}{REPEAT1}\verb|REPEAT1: tactic -> tactic| \\
\indexdef{}{ML}{REPEAT\_DETERM}\verb|REPEAT_DETERM: tactic -> tactic| \\
\indexdef{}{ML}{REPEAT\_DETERM\_N}\verb|REPEAT_DETERM_N: int -> tactic -> tactic| \\
- \indexdef{}{ML}{REPEAT}\verb|REPEAT: tactic -> tactic| \\
- \indexdef{}{ML}{REPEAT1}\verb|REPEAT1: tactic -> tactic| \\
- \indexdef{}{ML}{DETERM\_UNTIL}\verb|DETERM_UNTIL: (thm -> bool) -> tactic -> tactic| \\
\end{mldecls}
\begin{description}
@@ -602,13 +601,8 @@
returns the original state. Thus, it applies \isa{tac} at most
once.
- \item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the
- proof state and, recursively, to the head of the resulting sequence.
- It returns the first state to make \isa{tac} fail. It is
- deterministic, discarding alternative outcomes.
-
- \item \verb|REPEAT_DETERM_N|~\isa{n\ tac} is like \verb|REPEAT_DETERM|~\isa{tac} but the number of repetitions is bound
- by \isa{n} (where \verb|~1| means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}).
+ Note that for tactics with subgoal addressing, the combinator can be
+ applied via functional composition: \verb|TRY|~\verb|o|~\isa{tac}. There is no need for \verb|TRY'|.
\item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the proof
state and, recursively, to each element of the resulting sequence.
@@ -620,12 +614,13 @@
but it always applies \isa{tac} at least once, failing if this
is impossible.
- \item \verb|DETERM_UNTIL|~\isa{P\ tac} applies \isa{tac} to
- the proof state and, recursively, to the head of the resulting
- sequence, until the predicate \isa{P} (applied on the proof
- state) yields \verb|true|. It fails if \isa{tac} fails on any of
- the intermediate states. It is deterministic, discarding alternative
- outcomes.
+ \item \verb|REPEAT_DETERM|~\isa{tac} applies \isa{tac} to the
+ proof state and, recursively, to the head of the resulting sequence.
+ It returns the first state to make \isa{tac} fail. It is
+ deterministic, discarding alternative outcomes.
+
+ \item \verb|REPEAT_DETERM_N|~\isa{n\ tac} is like \verb|REPEAT_DETERM|~\isa{tac} but the number of repetitions is bound
+ by \isa{n} (where \verb|~1| means \isa{{\isaliteral{5C3C696E66696E6974793E}{\isasyminfinity}}}).
\end{description}%
\end{isamarkuptext}%
@@ -736,8 +731,7 @@
\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.%
+ where a different order is desired.%
\end{isamarkuptext}%
\isamarkuptrue%
%
@@ -750,12 +744,10 @@
\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}
@@ -763,8 +755,6 @@
\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.
@@ -777,12 +767,6 @@
\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%