src/Provers/hypsubst.ML
 changeset 646 7928c9760667 parent 231 cb6a24451544 child 680 f9e24455bbd1
equal inserted replaced
645:77474875da92 646:7928c9760667
`     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 `