src/Provers/hypsubst.ML
changeset 4299 22596d62ce0b
parent 4223 f60e3d2c81d3
child 4466 305390f23734
equal deleted inserted replaced
4298:b69eedd3aa6c 4299:22596d62ce0b
    76 (*If novars then we forbid Vars in the equality.
    76 (*If novars then we forbid Vars in the equality.
    77   If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
    77   If bnd then we only look for Bound (or dotted Free) variables to eliminate. 
    78   When can we safely delete the equality?
    78   When can we safely delete the equality?
    79     Not if it equates two constants; consider 0=1.
    79     Not if it equates two constants; consider 0=1.
    80     Not if it resembles x=t[x], since substitution does not eliminate x.
    80     Not if it resembles x=t[x], since substitution does not eliminate x.
    81     Not if it resembles ?x=0; another goal could instantiate ?x to Suc(i)
    81     Not if it resembles ?x=0; consider ?x=0 ==> ?x=1 or even ?x=0 ==> P
    82     Not if it involves a variable free in the premises, 
    82     Not if it involves a variable free in the premises, 
    83         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    83         but we can't check for this -- hence bnd and bound_hyp_subst_tac
    84   Prefer to eliminate Bound variables if possible.
    84   Prefer to eliminate Bound variables if possible.
    85   Result:  true = use as is,  false = reorient first *)
    85   Result:  true = use as is,  false = reorient first *)
    86 fun inspect_pair bnd novars (t,u,T) =
    86 fun inspect_pair bnd novars (t,u,T) =