--- a/src/Doc/IsarImplementation/Tactic.thy Wed Nov 07 16:09:39 2012 +0100
+++ b/src/Doc/IsarImplementation/Tactic.thy Wed Nov 07 16:45:33 2012 +0100
@@ -462,6 +462,56 @@
\end{description}
*}
+
+subsection {* Raw composition: resolution without lifting *}
+
+text {*
+ Raw composition of two rules means resolving them without prior
+ lifting or renaming of unknowns. This low-level operation, which
+ underlies the resolution tactics, may occasionally be useful for
+ special effects. Schematic variables are not renamed, so beware of
+ clashes!
+*}
+
+text %mlref {*
+ \begin{mldecls}
+ @{index_ML compose_tac: "(bool * thm * int) -> int -> tactic"} \\
+ @{index_ML compose: "thm * int * thm -> thm list"} \\
+ @{index_ML_op COMP: "thm * thm -> thm"} \\
+ \end{mldecls}
+
+ \begin{description}
+
+ \item @{ML compose_tac}~@{text "(flag, rule, m) i"} refines subgoal
+ @{text "i"} using @{text "rule"}, without lifting. The @{text
+ "rule"} is taken to have the form @{text "\<psi>\<^sub>1 \<Longrightarrow> \<dots> \<psi>\<^sub>m \<Longrightarrow> \<psi>"}, where
+ @{text "\<psi>"} need not be atomic; thus @{text "m"} determines the
+ number of new subgoals. If @{text "flag"} is @{text "true"} then it
+ performs elim-resolution --- it solves the first premise of @{text
+ "rule"} by assumption and deletes that assumption.
+
+ \item @{ML compose}~@{text "(thm\<^sub>1, i, thm\<^sub>2)"} uses @{text "thm\<^sub>1"},
+ regarded as an atomic formula, to solve premise @{text "i"} of
+ @{text "thm\<^sub>2"}. Let @{text "thm\<^sub>1"} and @{text "thm\<^sub>2"} be @{text
+ "\<psi>"} and @{text "\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>"}. For each @{text "s"} that unifies
+ @{text "\<psi>"} and @{text "\<phi>"}, the result list contains the theorem
+ @{text "(\<phi>\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>i\<^sub>-\<^sub>1 \<Longrightarrow> \<phi>\<^sub>i\<^sub>+\<^sub>1 \<Longrightarrow> \<dots> \<phi>\<^sub>n \<Longrightarrow> \<phi>)s"}.
+
+ \item @{text "thm\<^sub>1 COMP thm\<^sub>2"} calls @{text "compose (thm\<^sub>1, 1,
+ thm\<^sub>2)"} and returns the result, if unique; otherwise, it raises
+ exception @{ML THM}.
+
+ \end{description}
+
+ \begin{warn}
+ These low-level operations are stepping outside the structure
+ imposed by regular rule resolution. Used without understanding of
+ the consequences, they may produce results that cause problems with
+ standard rules and tactics later on.
+ \end{warn}
+*}
+
+
section {* Tacticals \label{sec:tacticals} *}
text {* A \emph{tactical} is a functional combinator for building up
--- a/src/Doc/ROOT Wed Nov 07 16:09:39 2012 +0100
+++ b/src/Doc/ROOT Wed Nov 07 16:45:33 2012 +0100
@@ -265,7 +265,6 @@
"document/simplifier.tex"
"document/substitution.tex"
"document/syntax.tex"
- "document/tactic.tex"
"document/thm.tex"
session Sledgehammer (doc) in "Sledgehammer" = Pure +
--- a/src/Doc/Ref/document/root.tex Wed Nov 07 16:09:39 2012 +0100
+++ b/src/Doc/Ref/document/root.tex Wed Nov 07 16:45:33 2012 +0100
@@ -40,7 +40,6 @@
\pagenumbering{roman} \tableofcontents \clearfirst
-\input{tactic}
\input{thm}
\input{syntax}
\input{substitution}
--- a/src/Doc/Ref/document/tactic.tex Wed Nov 07 16:09:39 2012 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,29 +0,0 @@
-
-\chapter{Tactics} \label{tactics}
-\index{tactics|(}
-
-\section{Other basic tactics}
-
-\subsection{Composition: resolution without lifting}
-\index{tactics!for composition}
-\begin{ttbox}
-compose_tac: (bool * thm * int) -> int -> tactic
-\end{ttbox}
-{\bf Composing} two rules means resolving them without prior lifting or
-renaming of unknowns. This low-level operation, which underlies the
-resolution tactics, may occasionally be useful for special effects.
-A typical application is \ttindex{res_inst_tac}, which lifts and instantiates a
-rule, then passes the result to {\tt compose_tac}.
-\begin{ttdescription}
-\item[\ttindexbold{compose_tac} ($flag$, $rule$, $m$) $i$]
-refines subgoal~$i$ using $rule$, without lifting. The $rule$ is taken to
-have the form $\List{\psi@1; \ldots; \psi@m} \Imp \psi$, where $\psi$ need
-not be atomic; thus $m$ determines the number of new subgoals. If
-$flag$ is {\tt true} then it performs elim-resolution --- it solves the
-first premise of~$rule$ by assumption and deletes that assumption.
-\end{ttdescription}
-
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "ref"
-%%% End:
--- a/src/Doc/Ref/document/thm.tex Wed Nov 07 16:09:39 2012 +0100
+++ b/src/Doc/Ref/document/thm.tex Wed Nov 07 16:45:33 2012 +0100
@@ -309,11 +309,13 @@
Most of these rules have the sole purpose of implementing particular
tactics. There are few occasions for applying them directly to a theorem.
-\subsection{Resolution}
+\subsection{Resolution and raw composition}
\index{resolution}
\begin{ttbox}
biresolution : bool -> (bool*thm)list -> int -> thm
-> thm Seq.seq
+bicompose : bool -> bool * thm * int -> int -> thm
+ -> thm Seq.seq
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{biresolution} $match$ $rules$ $i$ $state$]
@@ -321,38 +323,6 @@
(flag,rule)$ pairs. For each pair, it applies resolution if the flag
is~{\tt false} and elim-resolution if the flag is~{\tt true}. If $match$
is~{\tt true}, the $state$ is not instantiated.
-\end{ttdescription}
-
-
-\subsection{Composition: resolution without lifting}
-\index{resolution!without lifting}
-\begin{ttbox}
-compose : thm * int * thm -> thm list
-COMP : thm * thm -> thm
-bicompose : bool -> bool * thm * int -> int -> thm
- -> thm Seq.seq
-\end{ttbox}
-In forward proof, a typical use of composition is to regard an assertion of
-the form $\phi\Imp\psi$ as atomic. Schematic variables are not renamed, so
-beware of clashes!
-\begin{ttdescription}
-\item[\ttindexbold{compose} ($thm@1$, $i$, $thm@2$)]
-uses $thm@1$, regarded as an atomic formula, to solve premise~$i$
-of~$thm@2$. Let $thm@1$ and $thm@2$ be $\psi$ and $\List{\phi@1; \ldots;
-\phi@n} \Imp \phi$. For each $s$ that unifies~$\psi$ and $\phi@i$, the
-result list contains the theorem
-\[ (\List{\phi@1; \ldots; \phi@{i-1}; \phi@{i+1}; \ldots; \phi@n} \Imp \phi)s.
-\]
-
-\item[$thm@1$ \ttindexbold{COMP} $thm@2$]
-calls \hbox{\tt compose ($thm@1$, 1, $thm@2$)} and returns the result, if
-unique; otherwise, it raises exception~\xdx{THM}\@. It is
-analogous to {\tt RS}\@.
-
-For example, suppose that $thm@1$ is $a=b\Imp b=a$, a symmetry rule, and
-that $thm@2$ is $\List{P\Imp Q; \neg Q} \Imp\neg P$, which is the
-principle of contrapositives. Then the result would be the
-derived rule $\neg(b=a)\Imp\neg(a=b)$.
\item[\ttindexbold{bicompose} $match$ ($flag$, $rule$, $m$) $i$ $state$]
refines subgoal~$i$ of $state$ using $rule$, without lifting. The $rule$