[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Function domains in TLAPS


I've noticed that TLAPS does not automatically deduce anything about a function's domain from facts about its mapping. E.g., the lemma in the following snippet fails:


    AXIOM A == f[3] = 8

    LEMMA 3 \in DOMAIN f BY A

This means that axioms must be specified/theorems proven separately for functions' mappings and their domains, which is extra work. Is this an artifact of the logic (if 3 is outside f's domain, f[3] may be anything, and if I know it's 8, that doesn't mean that 3 is in the domain) or just a limitation of TLAPS?