States and Predicates

The Model

We semantically model program states as functions variables to values. The universe of variables and the universe of values are repesented by two distinct type variables. A predicate over a is a function of type a->bool. A state predicate is a predicate over states.

Predicate Operators

All boolean operators such as /\ and \/ are lifted to work on our semantical model of states and predicates. For example, the liften version of /\ is defined as follows:

p AND q = (\s. p s /\ q s)

Disjunction, negation, and implication can be defined in much the same way. Universal and existensial quantifications are defined like this:

(!!i::P. Q i) s = (!i::P. Q i s)

(??i::P. Q i) s = (?i::P. Q i s)

And the every where operator is defined like this:

|== p = (!s. p s)

(so |== p means the predicate p holds every where.

Theory uvars: State Projection

Definitions

State Projection

Let f be a polymorphic function from type 's (state) to 'v (value). Nov is an unspecified value of type 'v. We use it's unspecifiedness is used to model undefinedness. So, when f x returns Nov this is to model the fact that f is undefined in x. This is our way to encode partial functions with total functions.

val Pj_def = |- !f A x. (f Pj A) x = ((A x) => (f x) | Nov)

Predicate Projection

val pj_def = |- !p V. p pj V = (\s. p (s Pj V))

Derived Theorems

Composition of two projections

val pj_COMPO = |- (p pj V) pj W = p pj V AND W 

val Pj_COMPO = |- (f Pj A) Pj B = f Pj B AND A

val Pj_Pj = |- (f Pj A) Pj A = f Pj A 

val pj_pj = |- (p pj V) pj V = p pj V

Extensionality Theorem

  val Pj_EQ =
  |- !f g A. (f Pj A = g Pj A) = (!x. A x ==> (f x = g x))

Monotonicity Related Theorems

val Pj_EQ_MONO =
|- !A B f g. |== (A IMP B) /\ (f Pj B = g Pj B) ==> (f Pj A = g Pj A)

Projection Distributes over Predicates Operators

val pj_EQUAL = |- p EQUAL q pj V = (p pj V) EQUAL (q pj V) 

val pj_qAND_GEN =
|- RES_qAND W (\i. f i) pj V = RES_qAND W (\i. f i pj V)


val pj_qAND = |- RES_qAND W (\i. i) pj V = RES_qAND W (\i. i pj V) 

val pj_qOR_GEN =
|- RES_qOR W (\i. f i) pj V = RES_qOR W (\i. f i pj V)


val pj_qOR = |- RES_qOR W (\i. i) pj V = RES_qOR W (\i. i pj V) 

val pj_AND = |- p AND q pj V = (p pj V) AND (q pj V) 

val pj_OR = |- p OR q pj V = (p pj V) OR (q pj V) 

val pj_NOT = |- NOT p pj V = NOT (p pj V) 

val pj_IMP = |- p IMP q pj V = (p pj V) IMP (q pj V)