[FEATURE] Type theorems

[konnov]

Following the discussions in #162 and #179, it may be useful to produce THEOREMs after running type inference.

EXTENDS Sequences
CONSTANTS Range
ASSUME(Range <: "set(Int)")

VARIABLES list

Mem(e, es) ==
  \E i \in DOMAIN es:
    e = es[i]

Init ==
  list = <<>>

Next ==
  \E e \in Range:
    list' = Append(list, e)

If type inference computes the types of list and Mem, we can introduce the following theorems:

THEOREM list \in Seq(Int)
THEOREM \A e \in Int, es \in Seq(Int): Mem(e, es) \in BOOLEAN

Although the translation from types to the statements about sets looks straightforward, some attention should be paid to the following TLA+ values: records and sets of records (we can only compute supertypes of records) and operators (we cannot use operators as values).

The above theorems may be useful for writing manual proofs in TLAPS.

[konnov]

I don't think it's relevant anymore