equal
deleted
inserted
replaced
1 (* Title: Provers/hypsubst |
1 (* Title: Provers/hypsubst |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Martin D Coen, Cambridge University Computer Laboratory |
4 Copyright 1993 University of Cambridge |
4 Copyright 1993 University of Cambridge |
5 |
5 |
6 Martin Coen's tactic for substitution in the hypotheses |
6 Martin Coen's tactic for substitution in the hypotheses |
7 *) |
7 *) |
8 |
8 |
47 |
47 |
48 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); |
48 fun loose (i,t) = 0 mem add_loose_bnos(t,i,[]); |
49 |
49 |
50 (*It's not safe to substitute for a constant; consider 0=1. |
50 (*It's not safe to substitute for a constant; consider 0=1. |
51 It's not safe to substitute for x=t[x] since x is not eliminated. |
51 It's not safe to substitute for x=t[x] since x is not eliminated. |
|
52 It's not safe to substitute for a Var; what if it appears in other goals? |
52 It's not safe to substitute for a variable free in the premises, |
53 It's not safe to substitute for a variable free in the premises, |
53 but how could we check for this?*) |
54 but how could we check for this?*) |
54 fun inspect_pair bnd (t,u) = |
55 fun inspect_pair bnd (t,u) = |
55 case (Pattern.eta_contract t, Pattern.eta_contract u) of |
56 case (Pattern.eta_contract t, Pattern.eta_contract u) of |
56 (Bound i, _) => if loose(i,u) then raise Match |
57 (Bound i, _) => if loose(i,u) then raise Match |