Theory "env"

Signature

Definitions

EMPTY_ENV_def

|- EMPTY_ENV = (\s. {})

Theorems

ENV_UPDATE_def

|- !e Q s. e[[[Q<--s]]] = (\q. (if q = Q then s else e q))

ENV_SWAP

|- !e Q Q' X X'.
     ~(Q = Q') ==> (e[[[Q<--X]]][[[Q'<--X']]] = e[[[Q'<--X']]][[[Q<--X]]])

ENV_UPDATE

|- !Q e X Y. e[[[Q<--X]]][[[Q<--Y]]] = e[[[Q<--Y]]]

ENV_EVAL

|- !e Q X. e[[[Q<--X]]] Q = X

ENV_UPDATE_INV

|- !e Q Q' X. ~(Q = Q') ==> (e[[[Q'<--X]]] Q = e Q)

ENV_EVAL_EQ_INV

|- !e e' Q P X. (Q = P) ==> (e[[[Q<--X]]] P = e'[[[Q<--X]]] P)

ENV_EVAL_NEQ_INV

|- !e e' Q P X.
     ~(Q = P) ==> ((e[[[Q<--X]]] P = e'[[[Q<--X]]] P) = (e P = e' P))

EMPTY_ENV_MAP

|- !x y. EMPTY_ENV x = EMPTY_ENV y

ENV_UPDATE_BOTH_INV

|- !e Q Q' X Y. ~(Q = Q') ==> (e[[[Q'<--X]]] Q = e[[[Q'<--Y]]] Q)

ENV_CASES

|- !e e' P Q X Y.
     e[[[P<--X]]] Q SUBSET e'[[[P<--Y]]] Q =
     (if Q = P then X SUBSET Y else e Q SUBSET e' Q)