summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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