# HG changeset patch
# User oheimb
# Date 982691242 -3600
# Node ID 14732e3eaa6e4adb6a19d505ea166b85179a7ddc
# Parent  9e2ec5f02217c36d78a6f7e486d0af7f6a1d2aa8
added rearrange_prems

diff -r 9e2ec5f02217 -r 14732e3eaa6e doc-src/Ref/thm.tex
--- 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}
 
 
diff -r 9e2ec5f02217 -r 14732e3eaa6e src/Pure/drule.ML
--- 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,