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

src/Provers/quantifier1.ML

changeset 38457 | b8760b6e7c65 |

parent 38452 | abc655166d61 |

parent 38456 | 6769ccd90ad6 |

child 42361 | 23f352990944 |

equal
deleted
inserted
replaced

38453:6e7f8121b4f7 | 38457:b8760b6e7c65 |
---|---|

15 by ordinary simplification. |
15 by ordinary simplification. |

16 |
16 |

17 And analogously for t=x, but the eqn is not turned around! |
17 And analogously for t=x, but the eqn is not turned around! |

18 |
18 |

19 NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; |
19 NB Simproc is only triggered by "!x. P(x) & P'(x) --> Q(x)"; |

20 "!x. x=t --> P(x)" is covered by the congreunce rule for -->; |
20 "!x. x=t --> P(x)" is covered by the congruence rule for -->; |

21 "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. |
21 "!x. t=x --> P(x)" must be taken care of by an ordinary rewrite rule. |

22 As must be "? x. t=x & P(x)". |
22 As must be "? x. t=x & P(x)". |

23 |
23 |

24 And similarly for the bounded quantifiers. |
24 And similarly for the bounded quantifiers. |

25 |
25 |

26 Gries etc call this the "1 point rules" |
26 Gries etc call this the "1 point rules" |

27 |
27 |

28 The above also works for !x1..xn. and ?x1..xn by moving the defined |
28 The above also works for !x1..xn. and ?x1..xn by moving the defined |

29 qunatifier inside first, but not for nested bounded quantifiers. |
29 quantifier inside first, but not for nested bounded quantifiers. |

30 |
30 |

31 For set comprehensions the basic permutations |
31 For set comprehensions the basic permutations |

32 ... & x = t & ... -> x = t & (... & ...) |
32 ... & x = t & ... -> x = t & (... & ...) |

33 ... & t = x & ... -> t = x & (... & ...) |
33 ... & t = x & ... -> t = x & (... & ...) |

34 are also exported. |
34 are also exported. |