--- a/doc-src/IsarImplementation/Thy/Logic.thy Wed Jan 25 14:13:59 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/Logic.thy Wed Jan 25 15:39:08 2012 +0100
@@ -1084,23 +1084,50 @@
text %mlref {*
\begin{mldecls}
+ @{index_ML "op RSN": "thm * (int * thm) -> thm"} \\
@{index_ML "op RS": "thm * thm -> thm"} \\
+
+ @{index_ML "op RLN": "thm list * (int * thm list) -> thm list"} \\
+ @{index_ML "op RL": "thm list * thm list -> thm list"} \\
+
+ @{index_ML "op MRS": "thm list * thm -> thm"} \\
@{index_ML "op OF": "thm * thm list -> thm"} \\
\end{mldecls}
\begin{description}
- \item @{text "rule\<^sub>1 RS rule\<^sub>2"} resolves @{text "rule\<^sub>1"} with @{text
- "rule\<^sub>2"} according to the @{inference resolution} principle
- explained above. Note that the corresponding rule attribute in the
- Isar language is called @{attribute THEN}.
+ \item @{text "rule\<^sub>1 RSN (i, rule\<^sub>2)"} resolves the conclusion of
+ @{text "rule\<^sub>1"} with the @{text i}-th premise of @{text "rule\<^sub>2"},
+ according to the @{inference resolution} principle explained above.
+ Unless there is precisely one resolvent it raises exception @{ML
+ THM}.
+
+ This corresponds to the rule attribute @{attribute THEN} in Isar
+ source language.
+
+ \item @{text "rule\<^sub>1 RS rule\<^sub>2"} abbreviates @{text "rule\<^sub>1 RS (1,
+ rule\<^sub>2)"}.
- \item @{text "rule OF rules"} resolves a list of rules with the
- first rule, addressing its premises @{text "1, \<dots>, length rules"}
- (operating from last to first). This means the newly emerging
- premises are all concatenated, without interfering. Also note that
- compared to @{text "RS"}, the rule argument order is swapped: @{text
- "rule\<^sub>1 RS rule\<^sub>2 = rule\<^sub>2 OF [rule\<^sub>1]"}.
+ \item @{text "rules\<^sub>1 RLN (i, rules\<^sub>2)"} joins lists of rules. For
+ every @{text "rule\<^sub>1"} in @{text "rules\<^sub>1"} and @{text "rule\<^sub>2"} in
+ @{text "rules\<^sub>2"}, it resolves the conclusion of @{text "rule\<^sub>1"} with
+ the @{text "i"}-th premise of @{text "rule\<^sub>2"}, accumulating multiple
+ results in one big list. Note that such strict enumerations of
+ higher-order unifications can be inefficient compared to the lazy
+ variant seen in elementary tactics like @{ML resolve_tac}.
+
+ \item @{text "rules\<^sub>1 RL rules\<^sub>2"} abbreviates @{text "rules\<^sub>1 RLN (1,
+ rules\<^sub>2)"}.
+
+ \item @{text "[rule\<^sub>1, \<dots>, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^isub>i"}
+ against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \<dots>,
+ 1"}. By working from right to left, newly emerging premises are
+ concatenated in the result, without interfering.
+
+ \item @{text "rule OF rules"} abbreviates @{text "rules MRS rule"}.
+
+ This corresponds to the rule attribute @{attribute OF} in Isar
+ source language.
\end{description}
*}
--- a/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 14:13:59 2012 +0100
+++ b/doc-src/IsarImplementation/Thy/document/Logic.tex Wed Jan 25 15:39:08 2012 +0100
@@ -1226,21 +1226,46 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
+ \indexdef{}{ML}{RSN}\verb|op RSN: thm * (int * thm) -> thm| \\
\indexdef{}{ML}{RS}\verb|op RS: thm * thm -> thm| \\
+
+ \indexdef{}{ML}{RLN}\verb|op RLN: thm list * (int * thm list) -> thm list| \\
+ \indexdef{}{ML}{RL}\verb|op RL: thm list * thm list -> thm list| \\
+
+ \indexdef{}{ML}{MRS}\verb|op MRS: thm list * thm -> thm| \\
\indexdef{}{ML}{OF}\verb|op OF: thm * thm list -> thm| \\
\end{mldecls}
\begin{description}
- \item \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} resolves \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} with \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} according to the \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle
- explained above. Note that the corresponding rule attribute in the
- Isar language is called \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}}.
+ \item \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RSN\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} resolves the conclusion of
+ \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} with the \isa{i}-th premise of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}},
+ according to the \hyperlink{inference.resolution}{\mbox{\isa{resolution}}} principle explained above.
+ Unless there is precisely one resolvent it raises exception \verb|THM|.
+
+ This corresponds to the rule attribute \hyperlink{attribute.THEN}{\mbox{\isa{THEN}}} in Isar
+ source language.
+
+ \item \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} abbreviates \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}.
- \item \isa{rule\ OF\ rules} resolves a list of rules with the
- first rule, addressing its premises \isa{{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ length\ rules}
- (operating from last to first). This means the newly emerging
- premises are all concatenated, without interfering. Also note that
- compared to \isa{RS}, the rule argument order is swapped: \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RS\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}\ OF\ {\isaliteral{5B}{\isacharbrackleft}}rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}}.
+ \item \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RLN\ {\isaliteral{28}{\isacharparenleft}}i{\isaliteral{2C}{\isacharcomma}}\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} joins lists of rules. For
+ every \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} in \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} and \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} in
+ \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}, it resolves the conclusion of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}} with
+ the \isa{i}-th premise of \isa{rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}}, accumulating multiple
+ results in one big list. Note that such strict enumerations of
+ higher-order unifications can be inefficient compared to the lazy
+ variant seen in elementary tactics like \verb|resolve_tac|.
+
+ \item \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RL\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}} abbreviates \isa{rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}\ RLN\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ rules\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}.
+
+ \item \isa{{\isaliteral{5B}{\isacharbrackleft}}rule\isaliteral{5C3C5E7375623E}{}\isactrlsub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ rule\isaliteral{5C3C5E7375623E}{}\isactrlsub n{\isaliteral{5D}{\isacharbrackright}}\ MRS\ rule} resolves \isa{rule\isaliteral{5C3C5E697375623E}{}\isactrlisub i}
+ against premise \isa{i} of \isa{rule}, for \isa{i\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{2C}{\isacharcomma}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}\ {\isadigit{1}}}. By working from right to left, newly emerging premises are
+ concatenated in the result, without interfering.
+
+ \item \isa{rule\ OF\ rules} abbreviates \isa{rules\ MRS\ rule}.
+
+ This corresponds to the rule attribute \hyperlink{attribute.OF}{\mbox{\isa{OF}}} in Isar
+ source language.
\end{description}%
\end{isamarkuptext}%
--- a/doc-src/Ref/thm.tex Wed Jan 25 14:13:59 2012 +0100
+++ b/doc-src/Ref/thm.tex Wed Jan 25 15:39:08 2012 +0100
@@ -11,57 +11,6 @@
\section{Basic operations on theorems}
-\subsection{Forward proof: joining rules by resolution}
-\index{theorems!joining by resolution}
-\index{resolution}\index{forward proof}
-\begin{ttbox}
-RSN : thm * (int * thm) -> thm \hfill\textbf{infix}
-RS : thm * thm -> thm \hfill\textbf{infix}
-MRS : thm list * thm -> thm \hfill\textbf{infix}
-OF : thm * thm list -> thm \hfill\textbf{infix}
-RLN : thm list * (int * thm list) -> thm list \hfill\textbf{infix}
-RL : thm list * thm list -> thm list \hfill\textbf{infix}
-MRL : thm list list * thm list -> thm list \hfill\textbf{infix}
-\end{ttbox}
-Joining rules together is a simple way of deriving new rules. These
-functions are especially useful with destruction rules. To store
-the result in the theorem database, use \ttindex{bind_thm}
-(\S\ref{ExtractingAndStoringTheProvedTheorem}).
-\begin{ttdescription}
-\item[\tt$thm@1$ RSN $(i,thm@2)$] \indexbold{*RSN}
- resolves the conclusion of $thm@1$ with the $i$th premise of~$thm@2$.
- Unless there is precisely one resolvent it raises exception
- \xdx{THM}; in that case, use {\tt RLN}.
-
-\item[\tt$thm@1$ RS $thm@2$] \indexbold{*RS}
-abbreviates \hbox{\tt$thm@1$ RSN $(1,thm@2)$}. Thus, it resolves the
-conclusion of $thm@1$ with the first premise of~$thm@2$.
-
-\item[\tt {$[thm@1,\ldots,thm@n]$} MRS $thm$] \indexbold{*MRS}
- uses {\tt RSN} to resolve $thm@i$ against premise~$i$ of $thm$, for
- $i=n$, \ldots,~1. This applies $thm@n$, \ldots, $thm@1$ to the first $n$
- premises of $thm$. Because the theorems are used from right to left, it
- does not matter if the $thm@i$ create new premises. {\tt MRS} is useful
- for expressing proof trees.
-
-\item[\tt {$thm$ OF $[thm@1,\ldots,thm@n]$}] \indexbold{*OF} is the same as
- \texttt{$[thm@1,\ldots,thm@n]$ MRS $thm$}, with slightly more readable
- argument order, though.
-
-\item[\tt$thms@1$ RLN $(i,thms@2)$] \indexbold{*RLN}
- joins lists of theorems. For every $thm@1$ in $thms@1$ and $thm@2$ in
- $thms@2$, it resolves the conclusion of $thm@1$ with the $i$th premise
- of~$thm@2$, accumulating the results.
-
-\item[\tt$thms@1$ RL $thms@2$] \indexbold{*RL}
-abbreviates \hbox{\tt$thms@1$ RLN $(1,thms@2)$}.
-
-\item[\tt {$[thms@1,\ldots,thms@n]$} MRL $thms$] \indexbold{*MRL}
-is analogous to {\tt MRS}, but combines theorem lists rather than theorems.
-It too is useful for expressing proof trees.
-\end{ttdescription}
-
-
\subsection{Expanding definitions in theorems}
\index{meta-rewriting!in theorems}
\begin{ttbox}