On Tuesday, June 14, 2016 at 5:18:04 PM UTC+3, Stephan Merz wrote:
Just knowing that g = 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 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:
ASSUME A1 == f = [x \in DOMAIN f |-> f[x]]
ASSUME A2 == f = 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.