added rearrange_prems
authoroheimb
Tue Feb 20 18:47:22 2001 +0100 (2001-02-20)
changeset 1116314732e3eaa6e
parent 11162 9e2ec5f02217
child 11164 03f5dc539fd9
added rearrange_prems
doc-src/Ref/thm.tex
src/Pure/drule.ML
     1.1 --- a/doc-src/Ref/thm.tex	Tue Feb 20 18:47:06 2001 +0100
     1.2 +++ b/doc-src/Ref/thm.tex	Tue Feb 20 18:47:22 2001 +0100
     1.3 @@ -193,6 +193,7 @@
     1.4  rule_by_tactic   :     tactic -> thm -> thm
     1.5  rotate_prems     :        int -> thm -> thm
     1.6  permute_prems    : int -> int -> thm -> thm
     1.7 +rearrange_prems  :   int list -> thm -> thm
     1.8  \end{ttbox}
     1.9  \begin{ttdescription}
    1.10  \item[\ttindexbold{standard} $thm$] puts $thm$ into the standard form
    1.11 @@ -232,6 +233,11 @@
    1.12    requires $0\leq j\leq n$, where $n$ is the number of premises.  If $k$ is
    1.13    positive then it rotates the remaining $n-j$ premises to the left; if $k$ is
    1.14    negative then it rotates the premises to the right.
    1.15 +
    1.16 +\item[\ttindexbold{rearrange_prems} $ps$ $thm$] permutes the premises of $thm$
    1.17 +   where the value at the $i$-th position (counting from $0$) in the list $ps$
    1.18 +   gives the position within the original thm to be transferred to position $i$.
    1.19 +   Any remaining trailing positions are left unchanged.
    1.20  \end{ttdescription}
    1.21  
    1.22  
     2.1 --- a/src/Pure/drule.ML	Tue Feb 20 18:47:06 2001 +0100
     2.2 +++ b/src/Pure/drule.ML	Tue Feb 20 18:47:22 2001 +0100
     2.3 @@ -40,6 +40,7 @@
     2.4    val zero_var_indexes  : thm -> thm
     2.5    val standard          : thm -> thm
     2.6    val rotate_prems      : int -> thm -> thm
     2.7 +  val rearrange_prems   : int list -> thm -> thm
     2.8    val assume_ax         : theory -> string -> thm
     2.9    val RSN               : thm * (int * thm) -> thm
    2.10    val RS                : thm * thm -> thm
    2.11 @@ -367,6 +368,15 @@
    2.12  (*Rotates a rule's premises to the left by k*)
    2.13  val rotate_prems = permute_prems 0;
    2.14  
    2.15 +(* permute prems, where the i-th position in the argument list (counting from 0)
    2.16 +   gives the position within the original thm to be transferred to position i.
    2.17 +   Any remaining trailing positions are left unchanged. *)
    2.18 +val rearrange_prems = let
    2.19 +  fun rearr new []      thm = thm
    2.20 +  |   rearr new (p::ps) thm = rearr (new+1) 
    2.21 +     (map (fn q => if new<=q andalso q<p then q+1 else q) ps)
    2.22 +     (permute_prems (new+1) (new-p) (permute_prems new (p-new) thm))
    2.23 +  in rearr 0 end;
    2.24  
    2.25  (*Assume a new formula, read following the same conventions as axioms.
    2.26    Generalizes over Free variables,