The definition of UNITY version 99

in HOL logic

This is temporarily the form of documentation I can offer untill I can free enough time to write a more decent documentation. The definitions and theorems are unfortunately listed without typing information. I try to be as consistent as possible to use the following convention:

  1. V and W are set of program variables and have the type of VAR.
  2. a is an action. It has the type of Action.
  3. s and t are program states and have the type of State.
  4. J,K,p,q,r,s are state predicates and have the type of Pred.
  5. Pr and Qr are UNITY programs and have the type of Umachine.

The convention overlaps in some cases, and sometimes I may also be inconsistent in using it. The types VAR, Action, etc are defined as follows :

val State    = ty_antiq (Type `:'var->'val`) ;
val Pred     = ty_antiq (Type `:^State->bool`) ;
val Action   = ty_antiq (Type `:^State->^State->bool`) ;
val VARS     = ty_antiq (Type `:'var->bool`) ;
val Umachine = ty_antiq (Type `:^Action->bool`) ;

Definitions

Everywhere Operator

val Pvalid_def = |- !V J p. Pvalid V J p = |== (J IMP (p pj V))

Hoare Triple

val HOA_def = |- !a p q. HOA a p q = (!s t. p s /\ a s t ==> q t)

Strongest Predicate of an Action

val SP_def =
|- !V a p. SP V a p = (\t. ?s t'. (t Pj V = t' Pj V) /\ a s t' /\ p s)

Basic UNITY Operators: Stable, Unless, Ensures, Leadsto, Until

val STABLE_def = |- !Pr J. STABLE Pr J = (!a ::Pr. HOA a J J) 

val UNLESS_def =
|- !Pr V J p q.
UNLESS Pr V J p q =
STABLE Pr J /\
(!a ::Pr.
HOA a (J AND (p pj V) AND NOT (q pj V)) ((p pj V) OR (q pj V)))


val ENSURES_def =
|- !Pr V J p q.
ENSURES Pr V J p q =
UNLESS Pr V J p q /\
(?a ::Pr. HOA a (J AND (p pj V) AND NOT (q pj V)) (q pj V))
The progress operator leads-to is defined as the least transitive and disjunctive closure of ENSURES. Following Melham and Anderssen's ideas, we first define a higher order function TDC that returns the least transitive and disjunctive closure of a given relation. 
SUBREL_def = |- !r s. r SUBREL s = (!x y. r x y ==> s x y) 

TRANS_def = |- !r. TRANS r = (!x y z. r x y /\ r y z ==> r x z) 

LDISJ_def =
|- !U.
        LDISJ U =
        (!W y. (?x. W x) /\ (!x ::W. U x y) ==> U (RES_qOR W (\x. x)) y)

TDC_def =
|- !U x y. TDC U x y = (!X. U SUBREL X /\ TRANS X /\ LDISJ X ==> X x y)
So, leads-to is now: 
LEADSTO_def = |- !Pr V J. LEADSTO Pr V J = TDC (ENSURES Pr V J)
Many UNITY laws on leads-to turns out to be derivable at the TDC level --meaning that these laws are valid regardless the underlying fairness assumption of UNITY. Check out the TDC library. One may wish to compare this with the Misra's new-UNITY idea.

More definitions: 

UNTIL_def =
|- !Pr V J p q. UNTIL Pr V J p q = LEADSTO Pr V J p q /\ UNLESS Pr V J p q

Ignore and Conditional Write

val IGNORE_def =
|- !Pr J V.
IGNORE Pr J V = (!a p. Pr a ==> HOA a (J AND (p pj V)) (p pj V))


val CONDWRITE_def =
|- !Pr J V p q.
CONDWRITE Pr J V p q =
(!a z. Pr a ==> HOA a (J AND p AND (z pj V)) (p AND (z pj V) OR q))

Always Enabledness

val ALWAYS_ENABLED_def = |- !a. ALWAYS_ENABLED a = (!s. ?t. a s t)

Other Definitions (not too relevant right now...)

val disabledBy_def =
|- !a d. disabledBy a d = (!p. HOA a (d AND p) p)


val ProgressSpace_def =
|- !Pr guard V J p.
ProgressSpace Pr guard V J p =
RES_qOR (\a. runSet Pr guard V J p a) (\a. J AND (p pj V) AND guard a)


val runSet_def =
|- !Pr guard V J p.
runSet Pr guard V J p =
(\a. Pr a /\ ~(|== (J AND (p pj V) IMP NOT (guard a))))


val NEXT_def =
|- !Pr guard V J p.
NEXT Pr guard V J p =
RES_qOR (\a. runSet Pr guard V J p a) (\a. SP V a (J AND (p pj V)))


val N_LEADSTO_def =
|- (!Pr guard V J p q.
N_LEADSTO Pr guard V J 0 p q = Pvalid V J (p IMP q)) /\
(!Pr guard V J n p q.
N_LEADSTO Pr guard V J (SUC n) p q =
Pvalid V J
(p AND NOT q IMP ProgressSpace Pr guard V J (p AND NOT q)) /\
N_LEADSTO Pr guard V J n (NEXT Pr guard V J (p AND NOT q)) q)

Some Deribable Alternative Definitions

val UNLESS_adef1 =
|- UNLESS Pr V J p q =
STABLE Pr J /\
(!a ::Pr.
HOA a (J AND (p pj V) AND NOT (q pj V))
(J AND ((p pj V) OR (q pj V))))


val ENSURES_adef1 =
|- ENSURES Pr V J p q =
UNLESS Pr V J p q /\
(?a ::Pr. HOA a (J AND (p pj V) AND NOT (q pj V)) (J AND (q pj V)))


val IGNORE_adef1 = |- IGNORE Pr J V = CONDWRITE Pr J V TT FF 

val IGNORE_adef2 =
|- IGNORE Pr J V =
(!a X. Pr a ==> HOA a (J AND (\s. s Pj V = X)) (\s. s Pj V = X))


val CONDWRITE_adef1 =
|- CONDWRITE Pr J V p q =
(!a X.
Pr a ==>
HOA a (J AND p AND (\s. s Pj V = X)) (p AND (\s. s Pj V = X) OR q))


val disabledBy_adef1 =
|- disabledBy a d = (!s t. d s /\ a s t ==> (t = s))

Derivable Theorems

Sorry ... the theorems are not sorted.

val LEADSTO_BOUNDED_PROG =
|- ADMIT_WF_INDUCTION LESS /\
(!m.
LEADSTO Pr V J (p AND (\s. M s = m))
(p AND (\s. LESS (M s) m) OR q)) ==>
LEADSTO Pr V J p q

val LEADSTO_DISJ2 =
|- LEADSTO Pr V J p q /\ LEADSTO Pr V J r s ==>
LEADSTO Pr V J (p OR r) (q OR s)

val LEADSTO_IMP_NONEMPTY = |- LEADSTO Pr V J p q ==> (?a. Pr a) 
val LEADSTO_V_EXTEND =
|- LEADSTO Pr V J p q ==> LEADSTO Pr (V OR W) J (p pj V) (q pj V)

val UNLESS_SUBST =
|- Pvalid V J (p EQUAL r) /\
Pvalid V J (q EQUAL s) /\
UNLESS Pr V J p q ==>
UNLESS Pr V J r s

val UNLESS_CONSQ_WEAK =
|- Pvalid V J (q IMP r) /\ UNLESS Pr V J p q ==> UNLESS Pr V J p r

val LEADSTO_WD_COMPO =
|- LEADSTO Pr V J p q /\ STABLE Qr J /\ IGNORE Qr J V ==>
LEADSTO (Pr OR Qr) V J p q

val LEADSTO_CONSQ_WEAK =
|- LEADSTO Pr V J p q /\ Pvalid V J (q IMP r) ==> LEADSTO Pr V J p r

val LEADSTO_LDISJ2 =
|- LEADSTO Pr V J p s /\ LEADSTO Pr V J r s ==> LEADSTO Pr V J (p OR r) s

val SP_thm1 = |- HOA a p (q pj V) ==> |== (SP V a p IMP (q pj V)) 
val LEADSTO_ENS_LIFT = |- ENSURES Pr V J p q ==> LEADSTO Pr V J p q 
val SP_thm2 = |- HOA a p (SP V a p) 
val SP_thm3 = |- SP V a p pj V = SP V a p 
val LEADSTO_LDISJ =
|- W p /\ (!p ::W. LEADSTO Pr V J p q) ==>
LEADSTO Pr V J (RES_qOR W (\p. p)) q

val LEADSTO_REFL = |- Pr a /\ STABLE Pr J ==> LEADSTO Pr V J p p 
val UNLESS_V_EXTEND =
|- UNLESS Pr V J p q ==> UNLESS Pr (V OR W) J (p pj V) (q pj V)

val ENSURES_PSP =
|- ENSURES Pr V J p q /\ UNLESS Pr V J r s ==>
ENSURES Pr V J (p AND r) (q AND r OR s)

val LEADSTO_SINGH =
|- LEADSTO Pr V J p q /\
STABLE Qr J /\
CONDWRITE Qr J V (r pj V OR W) (s pj V OR W) ==>
LEADSTO (Pr OR Qr) (V OR W) J ((p pj V) AND r)
((q pj V) AND r OR NOT r OR s)

val STABLE_EXTEND =
|- STABLE Pr J1 /\ (!a ::Pr. HOA a (J1 AND J2) J2) ==>
STABLE Pr (J1 AND J2)

val UNLESS_SINGH =
|- UNLESS Pr V J p q /\
STABLE Qr J /\
CONDWRITE Qr J V (r pj V OR W) (s pj V OR W) ==>
UNLESS (Pr OR Qr) (V OR W) J ((p pj V) AND r)
((q pj V) AND r OR NOT r OR s)

val UNLESS_WD_COMPO =
|- UNLESS Pr V J p q /\ STABLE Qr J /\ IGNORE Qr J V ==>
UNLESS (Pr OR Qr) V J p q

val ENSURES_SINGH =
|- ENSURES Pr V J p q /\
STABLE Qr J /\
CONDWRITE Qr J V (r pj V OR W) (s pj V OR W) ==>
ENSURES (Pr OR Qr) (V OR W) J ((p pj V) AND r)
((q pj V) AND r OR NOT r OR s)

val UNLESS_STABLE_DISJ =
|- UNLESS Pr V J1 p q /\ UNLESS Pr V J2 p q ==> UNLESS Pr V (J1 OR J2) p q

val UNTIL_COMPO =
|- UNTIL Pr V J p q /\
STABLE Qr J /\
CONDWRITE Qr J V (p pj V) (q pj V) ==>
UNTIL (Pr OR Qr) V J p q

val LEADSTO_PSP =
|- LEADSTO Pr V J p q /\ UNLESS Pr V J r s ==>
LEADSTO Pr V J (p AND r) (q AND r OR s)

val SP_TO_LEADSTO_thm1 =
|- Pr a /\
STABLE Pr J /\
(!a. Pr a ==> disabledBy a (NOT (guard a))) /\
N_LEADSTO Pr guard V J n p q ==>
LEADSTO Pr V J p q

val ENSURES_STABLE_CONJ =
|- ENSURES Pr V J1 p q /\ ENSURES Pr V J2 p q ==>
ENSURES Pr V (J1 AND J2) p q

val LEADSTO_LDISJ_GEN =
|- W i /\ (!i ::W. LEADSTO Pr V J (f i) q) ==>
LEADSTO Pr V J (RES_qOR W (\i. f i)) q

val LEADSTO_CANCEL =
|- LEADSTO Pr V J p (q OR r) /\ LEADSTO Pr V J r s ==>
LEADSTO Pr V J p (q OR s)

val HOA_AND = |- HOA a p (q AND r) = HOA a p q /\ HOA a p r 
val LEADSTO_TRANS =
|- LEADSTO Pr V J p q /\ LEADSTO Pr V J q r ==> LEADSTO Pr V J p r

val UNLESS_STABLE_STRONG =
|- UNLESS Pr V J1 p q /\ STABLE Pr J2 ==> UNLESS Pr V (J1 AND J2) p q

val LEADSTO_ANTE_STRONG =
|- LEADSTO Pr V J q r /\ Pvalid V J (p IMP q) ==> LEADSTO Pr V J p r

val LEADSTO_STABLE_LSHIFT =
|- LEADSTO Pr V J (p AND q) r /\ STABLE Pr (J AND (p pj V)) ==>
LEADSTO Pr V (J AND (p pj V)) q r

val LEADSTO_STABLE_STRONG =
|- LEADSTO Pr V J1 p q /\ STABLE Pr J2 ==> LEADSTO Pr V (J1 AND J2) p q

val UNLESS_STABLE_CONJ =
|- UNLESS Pr V J1 p q /\ UNLESS Pr V J2 p q ==> UNLESS Pr V (J1 AND J2) p q

val LEADSTO_INDUCT_thm1 =
|- ENSURES Pr V J SUBREL U /\ TRANS U /\ LDISJ U ==>
(!p q. LEADSTO Pr V J p q ==> U p q)

val NEXT_LEADSTO_thm =
|- Pr a /\
STABLE Pr J /\
(!a. Pr a ==> disabledBy a (NOT (guard a))) /\
Pvalid V J (p IMP ProgressSpace Pr guard V J p) ==>
LEADSTO Pr V J p (NEXT Pr guard V J p)

val UNLESS_COMPO =
|- UNLESS Pr V J p q /\ UNLESS Qr V J p q ==> UNLESS (Pr OR Qr) V J p q

val ENSURES_IMP_LIFT =
|- Pr a /\ Pvalid V J (p IMP q) /\ STABLE Pr J ==> ENSURES Pr V J p q

val ENSURES_COMPO =
|- ENSURES Pr V J p q /\ UNLESS Qr V J p q ==> ENSURES (Pr OR Qr) V J p q

val ENSURES_CONSQ_WEAK =
|- Pvalid V J (q IMP r) /\ ENSURES Pr V J p q ==> ENSURES Pr V J p r

val LEADSTO_STABLE_RSHIFT =
|- LEADSTO Pr V (J AND (p pj V)) q r /\ STABLE Pr J ==>
LEADSTO Pr V J (p AND q) (p AND r)

val ENSURES_STABLE_STRONG =
|- ENSURES Pr V J1 p q /\ STABLE Pr J2 ==> ENSURES Pr V (J1 AND J2) p q

val LEADSTO_IMP_STABLE = |- LEADSTO Pr V J p q ==> STABLE Pr J 
val STABLE_COMPO =
|- STABLE Pr J /\ STABLE Qr J ==> STABLE (Pr OR Qr) J

val UNLESS_DISJ =
|- UNLESS Pr V J p q /\ UNLESS Pr V J r s ==>
UNLESS Pr V J (p OR r) (NOT p AND s OR NOT r AND q OR q AND s)

val UNLESS_STABLE_LSHIFT =
|- UNLESS Pr V J (p AND q) r /\ STABLE Pr (J AND (p pj V)) ==>
UNLESS Pr V (J AND (p pj V)) q r

val ENSURES_V_EXTEND =
|- ENSURES Pr V J p q ==> ENSURES Pr (V OR W) J (p pj V) (q pj V)

val HOA_OR = |- HOA a (p OR q) r = HOA a p r /\ HOA a q r 
val LEADSTO_pj =
|- LEADSTO Pr V J p q = LEADSTO Pr V J (p pj V) (q pj V)

val LEADSTO_STABLE_STRONG2 =
|- LEADSTO Pr V J1 p q /\ STABLE Pr (J1 AND J2) ==>
LEADSTO Pr V (J1 AND J2) p q

val ENSURES_WD_COMPO =
|- ENSURES Pr V J p q /\ STABLE Qr J /\ IGNORE Qr J V ==>
ENSURES (Pr OR Qr) V J p q

val UNLESS_IMP_LIFT1 =
|- Pvalid V J (p IMP q) /\ STABLE Pr J ==> UNLESS Pr V J p q

val UNLESS_STABLE_STRONG2 =
|- UNLESS Pr V J1 p q /\ STABLE Pr (J1 AND J2) ==>
UNLESS Pr V (J1 AND J2) p q

val LEADSTO_DISJ_GEN =
|- W i /\ (!i ::W. LEADSTO Pr V J (f i) (g i)) ==>
LEADSTO Pr V J (RES_qOR W (\i. f i)) (RES_qOR W (\i. g i))

val UNLESS_IMP_LIFT2 =
|- Pvalid V J (NOT p IMP q) /\ STABLE Pr J ==> UNLESS Pr V J p q

val UNLESS_STABLE_RSHIFT =
|- UNLESS Pr V (J AND (p pj V)) q r /\ STABLE Pr J ==>
UNLESS Pr V J (p AND q) (p AND r)

val ENSURES_STABLE_LSHIFT =
|- ENSURES Pr V J (p AND q) r /\ STABLE Pr (J AND (p pj V)) ==>
ENSURES Pr V (J AND (p pj V)) q r

val UNLESS_pj =
|- UNLESS Pr V J p q = UNLESS Pr V J (p pj V) (q pj V)

val UNLESS_CONJ =
|- UNLESS Pr V J p q /\ UNLESS Pr V J r s ==>
UNLESS Pr V J (p AND r) (p AND s OR r AND q OR q AND s)

val ENSURES_pj =
|- ENSURES Pr V J p q = ENSURES Pr V J (p pj V) (q pj V)

val LEADSTO_IMP_LIFT =
|- Pr a /\ Pvalid V J (p IMP q) /\ STABLE Pr J ==> LEADSTO Pr V J p q

val STABLE_CONJ =
|- STABLE Pr J1 /\ STABLE Pr J2 ==> STABLE Pr (J1 AND J2)

val ENSURES_STABLE_STRONG2 =
|- ENSURES Pr V J1 p q /\ STABLE Pr (J1 AND J2) ==>
ENSURES Pr V (J1 AND J2) p q

val ENSURES_STABLE_RSHIFT =
|- ENSURES Pr V (J AND (p pj V)) q r /\ STABLE Pr J ==>
ENSURES Pr V J (p AND q) (p AND r)