# HG changeset patch # User wenzelm # Date 1327514678 -3600 # Node ID 6fab37137dcba447745ac092d68a695592671395 # Parent 89ee3bc580a8ed449b5bc5f2c727e3ef525fb480 updated repetition tacticals; discontinued odd trace_REPEAT (assumes sequential TTY loop); diff -r 89ee3bc580a8 -r 6fab37137dcb doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 18:18:59 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 19:04:38 2012 +0100 @@ -483,4 +483,111 @@ \end{description} *} + +subsection {* Repetition tacticals *} + +text {* These tacticals provide further control over repetition of + tactics, beyond the stylized forms of ``@{verbatim "?"}'' and + ``@{verbatim "+"}'' in Isar method expressions. *} + +text %mlref {* + \begin{mldecls} + @{index_ML "TRY": "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} + + \item @{ML TRY}~@{text "tac"} applies @{text "tac"} to the proof + state and returns the resulting sequence, if non-empty; otherwise it + 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 "\"}). + + \item @{ML REPEAT}~@{text "tac"} applies @{text "tac"} to the proof + state and, recursively, to each element of the resulting sequence. + The resulting sequence consists of those states that make @{text + "tac"} fail. Thus, it applies @{text "tac"} as many times as + possible (including zero times), and allows backtracking over each + invocation of @{text "tac"}. @{ML REPEAT} is more general than @{ML + REPEAT_DETERM}, but requires more space. + + \item @{ML REPEAT1}~@{text "tac"} is like @{ML REPEAT}~@{text "tac"} + 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. + + \end{description} +*} + + +subsection {* Identities for tacticals *} + +text %mlref {* + \begin{mldecls} + @{index_ML all_tac: tactic} \\ + @{index_ML no_tac: tactic} \\ + \end{mldecls} + + \begin{description} + + \item @{ML all_tac} maps any proof state to the one-element sequence + containing that state. Thus, it succeeds for all states. It is the + identity element of the tactical @{ML "op THEN"}. + + \item @{ML no_tac} maps any proof state to the empty sequence. Thus + it succeeds for no state. It is the identity element of + @{ML "op ORELSE"} and @{ML "op APPEND"}. Also, it is a zero element + for @{ML "op THEN"}, which means that @{text "tac THEN"}~@{ML + no_tac} is equivalent to @{ML no_tac}. + + \end{description} +*} + +text %mlex {* The following examples illustrate how these primitive + tactics can be used to imitate existing combinators like @{ML TRY} + or @{ML REPEAT} (ignoring some further implementation tricks): +*} + +ML {* + fun TRY tac = tac ORELSE all_tac; + fun REPEAT tac st = ((tac THEN REPEAT tac) ORELSE all_tac) st; +*} + +text {* If @{text "tac"} can return multiple outcomes then so can @{ML + REPEAT}~@{text "tac"}. @{ML REPEAT} uses @{ML "op ORELSE"} and not + @{ML "op APPEND"}, it applies @{text "tac"} as many times as + possible in each outcome. + + \begin{warn} + Note @{ML REPEAT}'s explicit abstraction over the proof state. + Recursive tacticals must be coded in this awkward fashion to avoid + infinite recursion. With the following definition, @{ML + REPEAT}~@{text "tac"} would loop due to the eager evaluation + strategy of ML: + \end{warn} +*} + +ML {* + fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; (*BAD!*) +*} + end diff -r 89ee3bc580a8 -r 6fab37137dcb doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 18:18:59 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 19:04:38 2012 +0100 @@ -572,7 +572,184 @@ % \endisadelimmlref % +\isamarkupsubsection{Repetition tacticals% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +These tacticals provide further control over repetition of + tactics, beyond the stylized forms of ``\verb|?|'' and + ``\verb|+|'' in Isar method expressions.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{TRY}\verb|TRY: 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} + + \item \verb|TRY|~\isa{tac} applies \isa{tac} to the proof + state and returns the resulting sequence, if non-empty; otherwise it + 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}}}). + + \item \verb|REPEAT|~\isa{tac} applies \isa{tac} to the proof + state and, recursively, to each element of the resulting sequence. + The resulting sequence consists of those states that make \isa{tac} fail. Thus, it applies \isa{tac} as many times as + possible (including zero times), and allows backtracking over each + invocation of \isa{tac}. \verb|REPEAT| is more general than \verb|REPEAT_DETERM|, but requires more space. + + \item \verb|REPEAT1|~\isa{tac} is like \verb|REPEAT|~\isa{tac} + 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. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\isamarkupsubsection{Identities for tacticals% +} +\isamarkuptrue% +% +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{all\_tac}\verb|all_tac: tactic| \\ + \indexdef{}{ML}{no\_tac}\verb|no_tac: tactic| \\ + \end{mldecls} + + \begin{description} + + \item \verb|all_tac| maps any proof state to the one-element sequence + containing that state. Thus, it succeeds for all states. It is the + identity element of the tactical \verb|op THEN|. + + \item \verb|no_tac| maps any proof state to the empty sequence. Thus + it succeeds for no state. It is the identity element of + \verb|op ORELSE| and \verb|op APPEND|. Also, it is a zero element + for \verb|op THEN|, which means that \isa{tac\ THEN}~\verb|no_tac| is equivalent to \verb|no_tac|. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% +\isadelimmlex +% +\endisadelimmlex +% +\isatagmlex +% +\begin{isamarkuptext}% +The following examples illustrate how these primitive + tactics can be used to imitate existing combinators like \verb|TRY| + or \verb|REPEAT| (ignoring some further implementation tricks):% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlex +{\isafoldmlex}% +% +\isadelimmlex +% +\endisadelimmlex +% +\isadelimML +% +\endisadelimML +% +\isatagML +\isacommand{ML}\isamarkupfalse% +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline +\ \ fun\ TRY\ tac\ {\isaliteral{3D}{\isacharequal}}\ tac\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\isanewline +\ \ fun\ REPEAT\ tac\ st\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{29}{\isacharparenright}}\ st{\isaliteral{3B}{\isacharsemicolon}}\isanewline +{\isaliteral{2A7D}{\isacharverbatimclose}}% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +% +\begin{isamarkuptext}% +If \isa{tac} can return multiple outcomes then so can \verb|REPEAT|~\isa{tac}. \verb|REPEAT| uses \verb|op ORELSE| and not + \verb|op APPEND|, it applies \isa{tac} as many times as + possible in each outcome. + + \begin{warn} + Note \verb|REPEAT|'s explicit abstraction over the proof state. + Recursive tacticals must be coded in this awkward fashion to avoid + infinite recursion. With the following definition, \verb|REPEAT|~\isa{tac} would loop due to the eager evaluation + strategy of ML: + \end{warn}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isadelimML +% +\endisadelimML +% +\isatagML +\isacommand{ML}\isamarkupfalse% +\ {\isaliteral{7B2A}{\isacharverbatimopen}}\isanewline +\ \ fun\ REPEAT\ tac\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}tac\ THEN\ REPEAT\ tac{\isaliteral{29}{\isacharparenright}}\ ORELSE\ all{\isaliteral{5F}{\isacharunderscore}}tac{\isaliteral{3B}{\isacharsemicolon}}\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{2A}{\isacharasterisk}}BAD{\isaliteral{21}{\isacharbang}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{29}{\isacharparenright}}\isanewline +{\isaliteral{2A7D}{\isacharverbatimclose}}% +\endisatagML +{\isafoldML}% +% +\isadelimML +% +\endisadelimML +\isanewline +% \isadelimtheory +\isanewline % \endisadelimtheory % diff -r 89ee3bc580a8 -r 6fab37137dcb doc-src/Ref/tctical.tex --- a/doc-src/Ref/tctical.tex Wed Jan 25 18:18:59 2012 +0100 +++ b/doc-src/Ref/tctical.tex Wed Jan 25 19:04:38 2012 +0100 @@ -1,106 +1,6 @@ \chapter{Tacticals} -\section{The basic tacticals} - -\subsection{Repetition tacticals} -\index{tacticals!repetition} -\begin{ttbox} -TRY : tactic -> tactic -REPEAT_DETERM : tactic -> tactic -REPEAT_DETERM_N : int -> tactic -> tactic -REPEAT : tactic -> tactic -REPEAT1 : tactic -> tactic -DETERM_UNTIL : (thm -> bool) -> tactic -> tactic -trace_REPEAT : bool ref \hfill{\bf initially false} -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{TRY} {\it tac}] -applies {\it tac\/} to the proof state and returns the resulting sequence, -if non-empty; otherwise it returns the original state. Thus, it applies -{\it tac\/} at most once. - -\item[\ttindexbold{REPEAT_DETERM} {\it tac}] -applies {\it tac\/} to the proof state and, recursively, to the head of the -resulting sequence. It returns the first state to make {\it tac\/} fail. -It is deterministic, discarding alternative outcomes. - -\item[\ttindexbold{REPEAT_DETERM_N} {\it n} {\it tac}] -is like \hbox{\tt REPEAT_DETERM {\it tac}} but the number of repititions -is bound by {\it n} (unless negative). - -\item[\ttindexbold{REPEAT} {\it tac}] -applies {\it tac\/} to the proof state and, recursively, to each element of -the resulting sequence. The resulting sequence consists of those states -that make {\it tac\/} fail. Thus, it applies {\it tac\/} as many times as -possible (including zero times), and allows backtracking over each -invocation of {\it tac}. It is more general than {\tt REPEAT_DETERM}, but -requires more space. - -\item[\ttindexbold{REPEAT1} {\it tac}] -is like \hbox{\tt REPEAT {\it tac}} but it always applies {\it tac\/} at -least once, failing if this is impossible. - -\item[\ttindexbold{DETERM_UNTIL} {\it p} {\it tac}] -applies {\it tac\/} to the proof state and, recursively, to the head of the -resulting sequence, until the predicate {\it p} (applied on the proof state) -yields {\it true}. It fails if {\it tac\/} fails on any of the intermediate -states. It is deterministic, discarding alternative outcomes. - -\item[set \ttindexbold{trace_REPEAT};] -enables an interactive tracing mode for the tacticals {\tt REPEAT_DETERM} -and {\tt REPEAT}. To view the tracing options, type {\tt h} at the prompt. -\end{ttdescription} - - -\subsection{Identities for tacticals} -\index{tacticals!identities for} -\begin{ttbox} -all_tac : tactic -no_tac : tactic -\end{ttbox} -\begin{ttdescription} -\item[\ttindexbold{all_tac}] -maps any proof state to the one-element sequence containing that state. -Thus, it succeeds for all states. It is the identity element of the -tactical \ttindex{THEN}\@. - -\item[\ttindexbold{no_tac}] -maps any proof state to the empty sequence. Thus it succeeds for no state. -It is the identity element of \ttindex{ORELSE}, and -\ttindex{APPEND}\@. Also, it is a zero element for \ttindex{THEN}, -which means that - -\hbox{\tt$tac$ THEN no_tac} is equivalent to {\tt no_tac}. -\end{ttdescription} -These primitive tactics are useful when writing tacticals. For example, -\ttindexbold{TRY} and \ttindexbold{REPEAT} (ignoring tracing) can be coded -as follows: -\begin{ttbox} -fun TRY tac = tac ORELSE all_tac; - -fun REPEAT tac = - (fn state => ((tac THEN REPEAT tac) ORELSE all_tac) state); -\end{ttbox} -If $tac$ can return multiple outcomes then so can \hbox{\tt REPEAT $tac$}. -Since {\tt REPEAT} uses \ttindex{ORELSE} and not {\tt APPEND}, it -applies $tac$ as many times as possible in each outcome. - -\begin{warn} -Note {\tt REPEAT}'s explicit abstraction over the proof state. Recursive -tacticals must be coded in this awkward fashion to avoid infinite -recursion. With the following definition, \hbox{\tt REPEAT $tac$} would -loop due to \ML's eager evaluation strategy: -\begin{ttbox} -fun REPEAT tac = (tac THEN REPEAT tac) ORELSE all_tac; -\end{ttbox} -\par\noindent -The built-in {\tt REPEAT} avoids~{\tt THEN}, handling sequences explicitly -and using tail recursion. This sacrifices clarity, but saves much space by -discarding intermediate proof states. -\end{warn} - - \section{Control and search tacticals} \index{search!tacticals|(}