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.