# 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 *)