Function domains in TLAPS

[Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>]

Hi.

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:

    CONSTANT f

    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?

Ron