src/Provers/quantifier1.ML
 changeset 38457 b8760b6e7c65 parent 38452 abc655166d61 parent 38456 6769ccd90ad6 child 42361 23f352990944
equal 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.`