--- a/doc-src/Ref/thm.tex Tue Feb 20 18:47:06 2001 +0100
+++ b/doc-src/Ref/thm.tex Tue Feb 20 18:47:22 2001 +0100
@@ -193,6 +193,7 @@
rule_by_tactic : tactic -> thm -> thm
rotate_prems : int -> thm -> thm
permute_prems : int -> int -> thm -> thm
+rearrange_prems : int list -> thm -> thm
\end{ttbox}
\begin{ttdescription}
\item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
@@ -232,6 +233,11 @@
requires $0\leq j\leq n$, where $n$ is the number of premises. If $k$ is
positive then it rotates the remaining $n-j$ premises to the left; if $k$ is
negative then it rotates the premises to the right.
+
+\item[\ttindexbold{rearrange_prems} $ps$ $thm$] permutes the premises of $thm$
+ where the value at the $i$-th position (counting from $0$) in the list $ps$
+ gives the position within the original thm to be transferred to position $i$.
+ Any remaining trailing positions are left unchanged.
\end{ttdescription}
--- a/src/Pure/drule.ML Tue Feb 20 18:47:06 2001 +0100
+++ b/src/Pure/drule.ML Tue Feb 20 18:47:22 2001 +0100
@@ -40,6 +40,7 @@
val zero_var_indexes : thm -> thm
val standard : thm -> thm
val rotate_prems : int -> thm -> thm
+ val rearrange_prems : int list -> thm -> thm
val assume_ax : theory -> string -> thm
val RSN : thm * (int * thm) -> thm
val RS : thm * thm -> thm
@@ -367,6 +368,15 @@
(*Rotates a rule's premises to the left by k*)
val rotate_prems = permute_prems 0;
+(* permute prems, where the i-th position in the argument list (counting from 0)
+ gives the position within the original thm to be transferred to position i.
+ Any remaining trailing positions are left unchanged. *)
+val rearrange_prems = let
+ fun rearr new [] thm = thm
+ | rearr new (p::ps) thm = rearr (new+1)
+ (map (fn q => if new<=q andalso q<p then q+1 else q) ps)
+ (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
+ in rearr 0 end;
(*Assume a new formula, read following the same conventions as axioms.
Generalizes over Free variables,