TLA+ is mainly intended for describing state machines. You apparently want to specify functional expressions. A syntactically correct version of your definition (ignoring leap years) could be represented as follows in TLA+:
-------- MODULE Test ---------
IsDayOfMonth(m,d) ==
IF m = 2 THEN d = 28
ELSE IF m \in {1,3,5,7,8,10,12} THEN d \in 1 .. 31
ELSE d \in 1 .. 30
=======================
Using the Toolbox, you can check such a definition by creating a model, checking the box "No Behavior Spec" in the Model Overview pane, then switch to the "Model Checking Results" pane and enter expressions such as
IsDayOfMonth(7, 30) or IsDayOfMonth(2, 30)
in the "Expression" field of the sub-window "Evaluate Constant Expression". Clicking on the triangle on green background makes TLC evaluate the expression and display the result.
Evaluating constant expressions in this way is useful for debugging your specification, but it is not what TLA+ is mainly useful for.
Regards,