Re: [tlaplus] Function domains in TLAPS

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

On Tuesday, June 14, 2016 at 5:18:04 PM UTC+3, Stephan Merz wrote:

Just knowing that g[3] = 8 doesn't allow you to infer that g is a function or to conclude anything about DOMAIN g, so TLAPS does the right thing. (For example, 42[3] denotes some unspecified value in TLA+, would you want to conclude that 42 is a function?) You want to state "type predicates" for the functions that appear in your specification – typically as ASSUME clauses for constant parameters, and as invariants for variables.

But this doesn't help, either:

    CONSTANT f

    ASSUME A1 == f = [x \in DOMAIN f |-> f[x]]

    ASSUME A2 == f[3] = 8

    LEMMA  3 \in DOMAIN f BY A1, A2

So now we know it's a function, but still don't infer anything about the domain from the mapping.