# HG changeset patch # User wenzelm # Date 1327511939 -3600 # Node ID 89ee3bc580a8ed449b5bc5f2c727e3ef525fb480 # Parent 3ba3681d89301cda16dd1022b7e73a043caf2036 updated THEN, ORELSE, APPEND, and derivatives; discontinued obscure INTLEAVE; diff -r 3ba3681d8930 -r 89ee3bc580a8 doc-src/IsarImplementation/Thy/Tactic.thy --- a/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 16:16:20 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/Tactic.thy Wed Jan 25 18:18:59 2012 +0100 @@ -399,15 +399,88 @@ section {* Tacticals \label{sec:tacticals} *} -text {* - A \emph{tactical} is a functional combinator for building up complex - tactics from simpler ones. Typical tactical perform sequential - composition, disjunction (choice), iteration, or goal addressing. - Various search strategies may be expressed via tacticals. +text {* A \emph{tactical} is a functional combinator for building up + complex tactics from simpler ones. Common tacticals perform + sequential composition, disjunctive choice, iteration, or goal + addressing. Various search strategies may be expressed via + tacticals. + + \medskip The chapter on tacticals in old \cite{isabelle-ref} is + still applicable for further details. *} + + +subsection {* Combining tactics *} + +text {* Sequential composition and alternative choices are the most + basic ways to combine tactics, similarly to ``@{verbatim ","}'' and + ``@{verbatim "|"}'' in Isar method notation. This corresponds to + @{text "THEN"} and @{text "ORELSE"} in ML, but there are further + possibilities for fine-tuning alternation of tactics such as @{text + "APPEND"}. Further details become visible in ML due to explicit + subgoal addressing. *} + +text %mlref {* + \begin{mldecls} + @{index_ML "op THEN": "tactic * tactic -> tactic"} \\ + @{index_ML "op ORELSE": "tactic * tactic -> tactic"} \\ + @{index_ML "op APPEND": "tactic * tactic -> tactic"} \\ + @{index_ML "EVERY": "tactic list -> tactic"} \\ + @{index_ML "FIRST": "tactic list -> tactic"} \\[0.5ex] + + @{index_ML "op THEN'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{index_ML "op ORELSE'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{index_ML "op APPEND'": "('a -> tactic) * ('a -> tactic) -> 'a -> tactic"} \\ + @{index_ML "EVERY'": "('a -> tactic) list -> 'a -> tactic"} \\ + @{index_ML "FIRST'": "('a -> tactic) list -> 'a -> tactic"} \\ + @{index_ML "EVERY1": "(int -> tactic) list -> tactic"} \\ + @{index_ML "FIRST1": "(int -> tactic) list -> tactic"} \\[0.5ex] + \end{mldecls} + + \begin{description} - \medskip FIXME + \item @{text "tac\<^sub>1 THEN tac\<^sub>2"} is the sequential composition of + @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a proof state, it + returns all states reachable in two steps by applying @{text "tac\<^sub>1"} + followed by @{text "tac\<^sub>2"}. First, it applies @{text "tac\<^sub>1"} to the + proof state, getting a sequence of possible next states; then, it + applies @{text "tac\<^sub>2"} to each of these and concatenates the results + to produce again one flat sequence of states. + + \item @{text "tac\<^sub>1 ORELSE tac\<^sub>2"} makes a choice between @{text + "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Applied to a state, it tries @{text + "tac\<^sub>1"} and returns the result if non-empty; if @{text "tac\<^sub>1"} fails + then it uses @{text "tac\<^sub>2"}. This is a deterministic choice: if + @{text "tac\<^sub>1"} succeeds then @{text "tac\<^sub>2"} is excluded from the + result. + + \item @{text "tac\<^sub>1 APPEND tac\<^sub>2"} concatenates the possible results + of @{text "tac\<^sub>1"} and @{text "tac\<^sub>2"}. Unlike @{text "ORELSE"} there + is \emph{no commitment} to either tactic, so @{text "APPEND"} helps + to avoid incompleteness during search, at the cost of potential + inefficiencies. - \medskip The chapter on tacticals in \cite{isabelle-ref} is still - applicable, despite a few outdated details. *} + \item @{text "EVERY [tac\<^sub>1, \, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 THEN + \ THEN tac\<^sub>n"}. Note that @{text "EVERY []"} is the same as @{ML + all_tac}: it always succeeds. + + \item @{text "FIRST [tac\<^sub>1, \, tac\<^sub>n]"} abbreviates @{text "tac\<^sub>1 + ORELSE \ ORELSE tac\<^sub>n"}. Note that @{text "FIRST []"} is the same as + @{ML no_tac}: it always fails. + + \item @{text "THEN'"}, @{text "ORELSE'"}, and @{text "APPEND'"} are + lifted versions of @{text "THEN"}, @{text "ORELSE"}, and @{text + "APPEND"}, for tactics with explicit subgoal addressing. This means + @{text "(tac\<^sub>1 THEN' tac\<^sub>2) i"} is the same as @{text "(tac\<^sub>1 i THEN + tac\<^sub>2 i)"} etc. + + \item @{text "EVERY'"} and @{text "FIRST'"} are lifted versions of + @{text "EVERY'"} and @{text "FIRST'"}, for tactics with explicit + subgoal addressing. + + \item @{text "EVERY1"} and @{text "FIRST1"} are convenience versions + of @{text "EVERY'"} and @{text "FIRST'"}, applied to subgoal 1. + + \end{description} +*} end diff -r 3ba3681d8930 -r 89ee3bc580a8 doc-src/IsarImplementation/Thy/document/Tactic.tex --- a/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 16:16:20 2012 +0100 +++ b/doc-src/IsarImplementation/Thy/document/Tactic.tex Wed Jan 25 18:18:59 2012 +0100 @@ -476,18 +476,102 @@ \isamarkuptrue% % \begin{isamarkuptext}% -A \emph{tactical} is a functional combinator for building up complex - tactics from simpler ones. Typical tactical perform sequential - composition, disjunction (choice), iteration, or goal addressing. - Various search strategies may be expressed via tacticals. +A \emph{tactical} is a functional combinator for building up + complex tactics from simpler ones. Common tacticals perform + sequential composition, disjunctive choice, iteration, or goal + addressing. Various search strategies may be expressed via + tacticals. - \medskip FIXME - - \medskip The chapter on tacticals in \cite{isabelle-ref} is still - applicable, despite a few outdated details.% + \medskip The chapter on tacticals in old \cite{isabelle-ref} is + still applicable for further details.% +\end{isamarkuptext}% +\isamarkuptrue% +% +\isamarkupsubsection{Combining tactics% +} +\isamarkuptrue% +% +\begin{isamarkuptext}% +Sequential composition and alternative choices are the most + basic ways to combine tactics, similarly to ``\verb|,|'' and + ``\verb||\verb,|,\verb||'' in Isar method notation. This corresponds to + \isa{THEN} and \isa{ORELSE} in ML, but there are further + possibilities for fine-tuning alternation of tactics such as \isa{APPEND}. Further details become visible in ML due to explicit + subgoal addressing.% \end{isamarkuptext}% \isamarkuptrue% % +\isadelimmlref +% +\endisadelimmlref +% +\isatagmlref +% +\begin{isamarkuptext}% +\begin{mldecls} + \indexdef{}{ML}{THEN}\verb|op THEN: tactic * tactic -> tactic| \\ + \indexdef{}{ML}{ORELSE}\verb|op ORELSE: tactic * tactic -> tactic| \\ + \indexdef{}{ML}{APPEND}\verb|op APPEND: tactic * tactic -> tactic| \\ + \indexdef{}{ML}{EVERY}\verb|EVERY: tactic list -> tactic| \\ + \indexdef{}{ML}{FIRST}\verb|FIRST: tactic list -> tactic| \\[0.5ex] + + \indexdef{}{ML}{THEN'}\verb|op THEN': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ + \indexdef{}{ML}{ORELSE'}\verb|op ORELSE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ + \indexdef{}{ML}{APPEND'}\verb|op APPEND': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic| \\ + \indexdef{}{ML}{EVERY'}\verb|EVERY': ('a -> tactic) list -> 'a -> tactic| \\ + \indexdef{}{ML}{FIRST'}\verb|FIRST': ('a -> tactic) list -> 'a -> tactic| \\ + \indexdef{}{ML}{EVERY1}\verb|EVERY1: (int -> tactic) list -> tactic| \\ + \indexdef{}{ML}{FIRST1}\verb|FIRST1: (int -> tactic) list -> tactic| \\[0.5ex] + \end{mldecls} + + \begin{description} + + \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is the sequential composition of + \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a proof state, it + returns all states reachable in two steps by applying \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} + followed by \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. First, it applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} to the + proof state, getting a sequence of possible next states; then, it + applies \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} to each of these and concatenates the results + to produce again one flat sequence of states. + + \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} makes a choice between \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Applied to a state, it tries \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and returns the result if non-empty; if \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} fails + then it uses \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. This is a deterministic choice: if + \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} succeeds then \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} is excluded from the + result. + + \item \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ APPEND\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} concatenates the possible results + of \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}. Unlike \isa{ORELSE} there + is \emph{no commitment} to either tactic, so \isa{APPEND} helps + to avoid incompleteness during search, at the cost of potential + inefficiencies. + + \item \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{EVERY\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as \verb|all_tac|: it always succeeds. + + \item \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}} abbreviates \isa{tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ ORELSE\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ ORELSE\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub n}. Note that \isa{FIRST\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} is the same as + \verb|no_tac|: it always fails. + + \item \isa{THEN{\isaliteral{27}{\isacharprime}}}, \isa{ORELSE{\isaliteral{27}{\isacharprime}}}, and \isa{APPEND{\isaliteral{27}{\isacharprime}}} are + lifted versions of \isa{THEN}, \isa{ORELSE}, and \isa{APPEND}, for tactics with explicit subgoal addressing. This means + \isa{{\isaliteral{28}{\isacharparenleft}}tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ THEN{\isaliteral{27}{\isacharprime}}\ 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\ THEN\ tac\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ i{\isaliteral{29}{\isacharparenright}}} etc. + + \item \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}} are lifted versions of + \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, for tactics with explicit + subgoal addressing. + + \item \isa{EVERY{\isadigit{1}}} and \isa{FIRST{\isadigit{1}}} are convenience versions + of \isa{EVERY{\isaliteral{27}{\isacharprime}}} and \isa{FIRST{\isaliteral{27}{\isacharprime}}}, applied to subgoal 1. + + \end{description}% +\end{isamarkuptext}% +\isamarkuptrue% +% +\endisatagmlref +{\isafoldmlref}% +% +\isadelimmlref +% +\endisadelimmlref +% \isadelimtheory % \endisadelimtheory diff -r 3ba3681d8930 -r 89ee3bc580a8 doc-src/Ref/tctical.tex --- a/doc-src/Ref/tctical.tex Wed Jan 25 16:16:20 2012 +0100 +++ b/doc-src/Ref/tctical.tex Wed Jan 25 18:18:59 2012 +0100 @@ -1,68 +1,7 @@ \chapter{Tacticals} -\index{tacticals|(} -Tacticals are operations on tactics. Their implementation makes use of -functional programming techniques, especially for sequences. Most of the -time, you may forget about this and regard tacticals as high-level control -structures. \section{The basic tacticals} -\subsection{Joining two tactics} -\index{tacticals!joining two tactics} -The tacticals {\tt THEN} and {\tt ORELSE}, which provide sequencing and -alternation, underlie most of the other control structures in Isabelle. -{\tt APPEND} and {\tt INTLEAVE} provide more sophisticated forms of -alternation. -\begin{ttbox} -THEN : tactic * tactic -> tactic \hfill{\bf infix 1} -ORELSE : tactic * tactic -> tactic \hfill{\bf infix} -APPEND : tactic * tactic -> tactic \hfill{\bf infix} -INTLEAVE : tactic * tactic -> tactic \hfill{\bf infix} -\end{ttbox} -\begin{ttdescription} -\item[$tac@1$ \ttindexbold{THEN} $tac@2$] -is the sequential composition of the two tactics. Applied to a proof -state, it returns all states reachable in two steps by applying $tac@1$ -followed by~$tac@2$. First, it applies $tac@1$ to the proof state, getting a -sequence of next states; then, it applies $tac@2$ to each of these and -concatenates the results. - -\item[$tac@1$ \ttindexbold{ORELSE} $tac@2$] -makes a choice between the two tactics. Applied to a state, it -tries~$tac@1$ and returns the result if non-empty; if $tac@1$ fails then it -uses~$tac@2$. This is a deterministic choice: if $tac@1$ succeeds then -$tac@2$ is excluded. - -\item[$tac@1$ \ttindexbold{APPEND} $tac@2$] -concatenates the results of $tac@1$ and~$tac@2$. By not making a commitment -to either tactic, {\tt APPEND} helps avoid incompleteness during -search.\index{search} - -\item[$tac@1$ \ttindexbold{INTLEAVE} $tac@2$] -interleaves the results of $tac@1$ and~$tac@2$. Thus, it includes all -possible next states, even if one of the tactics returns an infinite -sequence. -\end{ttdescription} - - -\subsection{Joining a list of tactics} -\index{tacticals!joining a list of tactics} -\begin{ttbox} -EVERY : tactic list -> tactic -FIRST : tactic list -> tactic -\end{ttbox} -{\tt EVERY} and {\tt FIRST} are block structured versions of {\tt THEN} and -{\tt ORELSE}\@. -\begin{ttdescription} -\item[\ttindexbold{EVERY} {$[tac@1,\ldots,tac@n]$}] -abbreviates \hbox{\tt$tac@1$ THEN \ldots{} THEN $tac@n$}. It is useful for -writing a series of tactics to be executed in sequence. - -\item[\ttindexbold{FIRST} {$[tac@1,\ldots,tac@n]$}] -abbreviates \hbox{\tt$tac@1$ ORELSE \ldots{} ORELSE $tac@n$}. It is useful for -writing a series of tactics to be attempted one after another. -\end{ttdescription} - \subsection{Repetition tacticals} \index{tacticals!repetition} @@ -128,8 +67,10 @@ \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}, \ttindex{APPEND}, and -\ttindex{INTLEAVE}\@. Also, it is a zero element for \ttindex{THEN}, which means that +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, @@ -142,9 +83,8 @@ (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} or {\tt -INTLEAVE}, it applies $tac$ as many times as possible in each -outcome. +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 @@ -429,79 +369,6 @@ with {\tt SOMEGOAL} and {\tt FIRSTGOAL}. \end{ttdescription} - -\subsection{Joining tactic functions} -\index{tacticals!joining tactic functions} -\begin{ttbox} -THEN' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix 1} -ORELSE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix} -APPEND' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix} -INTLEAVE' : ('a -> tactic) * ('a -> tactic) -> 'a -> tactic \hfill{\bf infix} -EVERY' : ('a -> tactic) list -> 'a -> tactic -FIRST' : ('a -> tactic) list -> 'a -> tactic -\end{ttbox} -These help to express tactics that specify subgoal numbers. The tactic -\begin{ttbox} -SOMEGOAL (fn i => resolve_tac rls i ORELSE eresolve_tac erls i) -\end{ttbox} -can be simplified to -\begin{ttbox} -SOMEGOAL (resolve_tac rls ORELSE' eresolve_tac erls) -\end{ttbox} -Note that {\tt TRY'}, {\tt REPEAT'}, {\tt DEPTH_FIRST'}, etc.\ are not -provided, because function composition accomplishes the same purpose. -The tactic -\begin{ttbox} -ALLGOALS (fn i => REPEAT (etac exE i ORELSE atac i)) -\end{ttbox} -can be simplified to -\begin{ttbox} -ALLGOALS (REPEAT o (etac exE ORELSE' atac)) -\end{ttbox} -These tacticals are polymorphic; $x$ need not be an integer. -\begin{center} \tt -\begin{tabular}{r@{\rm\ \ yields\ \ }l} - $(tacf@1$~~THEN'~~$tacf@2)(x)$ \index{*THEN'} & - $tacf@1(x)$~~THEN~~$tacf@2(x)$ \\ - - $(tacf@1$ ORELSE' $tacf@2)(x)$ \index{*ORELSE'} & - $tacf@1(x)$ ORELSE $tacf@2(x)$ \\ - - $(tacf@1$ APPEND' $tacf@2)(x)$ \index{*APPEND'} & - $tacf@1(x)$ APPEND $tacf@2(x)$ \\ - - $(tacf@1$ INTLEAVE' $tacf@2)(x)$ \index{*INTLEAVE'} & - $tacf@1(x)$ INTLEAVE $tacf@2(x)$ \\ - - EVERY' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*EVERY'} & - EVERY $[tacf@1(x),\ldots,tacf@n(x)]$ \\ - - FIRST' $[tacf@1,\ldots,tacf@n] \; (x)$ \index{*FIRST'} & - FIRST $[tacf@1(x),\ldots,tacf@n(x)]$ -\end{tabular} -\end{center} - - -\subsection{Applying a list of tactics to 1} -\index{tacticals!joining tactic functions} -\begin{ttbox} -EVERY1: (int -> tactic) list -> tactic -FIRST1: (int -> tactic) list -> tactic -\end{ttbox} -A common proof style is to treat the subgoals as a stack, always -restricting attention to the first subgoal. Such proofs contain long lists -of tactics, each applied to~1. These can be simplified using {\tt EVERY1} -and {\tt FIRST1}: -\begin{center} \tt -\begin{tabular}{r@{\rm\ \ abbreviates\ \ }l} - EVERY1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*EVERY1} & - EVERY $[tacf@1(1),\ldots,tacf@n(1)]$ \\ - - FIRST1 $[tacf@1,\ldots,tacf@n]$ \indexbold{*FIRST1} & - FIRST $[tacf@1(1),\ldots,tacf@n(1)]$ -\end{tabular} -\end{center} - \index{tacticals|)}