# HG changeset patch # User wenzelm # Date 1327502348 -3600 # Node ID bc874d2ee55a5b7e6e84b53728bb63c160995246 # Parent 6fae74ee591a658c7b0c20c54897bd17c4f0bb09 updated RSN, RL, RLN, MRS; discontinued obscure MRL; diff -r 6fae74ee591a -r bc874d2ee55a doc-src/IsarImplementation/Thy/Logic.thy --- 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, \, 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, \, rule\<^sub>n] MRS rule"} resolves @{text "rule\<^isub>i"} + against premise @{text "i"} of @{text "rule"}, for @{text "i = n, \, + 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} *} diff -r 6fae74ee591a -r bc874d2ee55a doc-src/IsarImplementation/Thy/document/Logic.tex --- 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}% diff -r 6fae74ee591a -r bc874d2ee55a doc-src/Ref/thm.tex --- 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}