# HG changeset patch
# User lcp
# Date 748860775 -7200
# Node ID d0e17c42dbb4f32adf216e8364ab133f7e9b736f
# Parent  e37080f41102a361f308600045ea7b11f1d468d9
Added MRS, MRL from ZF/ROOT.ML.  These support forward proof, resolving a
rule's premises against a list of other proofs.

diff -r e37080f41102 -r d0e17c42dbb4 src/Pure/drule.ML
--- a/src/Pure/drule.ML	Tue Sep 21 11:16:19 1993 +0200
+++ b/src/Pure/drule.ML	Fri Sep 24 10:52:55 1993 +0200
@@ -6,7 +6,7 @@
 Derived rules and other operations on theorems and theories
 *)
 
-infix 0 RS RSN RL RLN COMP;
+infix 0 RS RSN RL RLN MRS MRL COMP;
 
 signature DRULE =
   sig
@@ -31,6 +31,8 @@
   val forall_elim_vars: int -> thm -> thm
   val implies_elim_list: thm -> thm list -> thm
   val implies_intr_list: Sign.cterm list -> thm -> thm
+  val MRL: thm list list * thm list -> thm list
+  val MRS: thm list * thm -> thm
   val print_cterm: Sign.cterm -> unit
   val print_ctyp: Sign.ctyp -> unit
   val print_goals: int -> thm -> unit
@@ -191,6 +193,19 @@
 
 fun thas RL thbs = thas RLN (1,thbs);
 
+(*Resolve a list of rules against bottom_rl from right to left;
+  makes proof trees*)
+fun rls MRS bottom_rl = 
+  let fun rs_aux i [] = bottom_rl
+	| rs_aux i (rl::rls) = rl RSN (i, rs_aux (i+1) rls)
+  in  rs_aux 1 rls  end;
+
+(*As above, but for rule lists*)
+fun rlss MRL bottom_rls = 
+  let fun rs_aux i [] = bottom_rls
+	| rs_aux i (rls::rlss) = rls RLN (i, rs_aux (i+1) rlss)
+  in  rs_aux 1 rlss  end;
+
 (*compose Q and [...,Qi,Q(i+1),...]==>R to [...,Q(i+1),...]==>R 
   with no lifting or renaming!  Q may contain ==> or meta-quants
   ALWAYS deletes premise i *)