summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | lcp |

Fri, 24 Sep 1993 10:52:55 +0200 | |

changeset 11 | d0e17c42dbb4 |

parent 10 | e37080f41102 |

child 12 | f17d542276b6 |

Added MRS, MRL from ZF/ROOT.ML. These support forward proof, resolving a
rule's premises against a list of other proofs.

src/Pure/drule.ML | file | annotate | diff | comparison | revisions |

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