# HG changeset patch # User wenzelm # Date 1352303133 -3600 # Node ID 0b02aaf7c7c518d178c2562af3de5519a46006f4 # Parent 7e899409834734b1876ec9bc26ef3f2dfd5bd646 some coverage of "resolution without lifting", which should be normally avoided; diff -r 7e8994098347 -r 0b02aaf7c7c5 src/Doc/IsarImplementation/Tactic.thy --- 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 "\\<^sub>1 \ \ \\<^sub>m \ \"}, where + @{text "\"} 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 + "\"} and @{text "\\<^sub>1 \ \ \\<^sub>n \ \"}. For each @{text "s"} that unifies + @{text "\"} and @{text "\"}, the result list contains the theorem + @{text "(\\<^sub>1 \ \ \\<^sub>i\<^sub>-\<^sub>1 \ \\<^sub>i\<^sub>+\<^sub>1 \ \ \\<^sub>n \ \)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 diff -r 7e8994098347 -r 0b02aaf7c7c5 src/Doc/ROOT --- 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 + diff -r 7e8994098347 -r 0b02aaf7c7c5 src/Doc/Ref/document/root.tex --- 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} diff -r 7e8994098347 -r 0b02aaf7c7c5 src/Doc/Ref/document/tactic.tex --- 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: diff -r 7e8994098347 -r 0b02aaf7c7c5 src/Doc/Ref/document/thm.tex --- 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$