src/Pure/drule.ML
 changeset 11 d0e17c42dbb4 parent 0 a5a9c433f639 child 67 8380bc0adde7
```--- 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 *)```