Theory "ctl2mu"

Parents rich_list mu ctl

Signature

Constant	Type
unc	:('a # 'b -> 'c) -> 'a -> 'b -> 'c
ctl2muks	:('prop, 'state) kripke_structure -> ('prop, 'state) KS
PREFIX	:'a path -> num -> 'a list
P6	:('a # 'a -> bool) -> ('a -> bool) -> 'a -> num -> 'a -> bool
P5	:('a # 'a -> bool) -> ('a -> bool) -> 'a -> num -> 'a -> bool
P4	:('a # 'b -> bool) -> ('b -> bool) -> 'a -> 'b -> bool
P3	:('a -> bool) -> ('a # 'a -> bool) -> num -> 'a -> bool
P2	:('a -> bool) -> ('a # 'a -> bool) -> num -> 'a -> bool
P1	:('a -> bool) -> ('b # 'a -> bool) -> 'a -> bool
Nf5	:('state # 'state -> bool) -> ('state -> bool) -> 'state -> num -> 'state
Nf4	:('state # 'state -> bool) -> ('state -> bool) -> num -> 'state
Nf3	:('state # 'state -> bool) -> 'state -> 'state -> num -> 'state
Nf2	:('state # 'state -> bool) -> 'state -> num -> 'state
Nf	:('state # 'state -> bool) -> 'state -> 'state -> num -> 'state
LFP	:('prop, 'state) kripke_structure -> 'prop ctl -> 'prop ctl -> num -> 'state -> bool
INF_PFX	:(num -> 'a) -> num -> 'a list
GFP	:('prop, 'state) kripke_structure -> 'prop ctl -> num -> 'state -> bool
FIN_PFX	:'a list -> num -> 'a list
CTL2MU	:'a ctl -> 'a mu
BEXP2MU	:'prop bexp -> 'prop mu

Definitions

BEXP2MU_primitive_def

|- BEXP2MU =
   WFREC
     (@R.
        WF R /\ (!be. R be ~be) /\ (!be2 be1. R be1 (B_AND (be1,be2))) /\
        !be1 be2. R be2 (B_AND (be1,be2)))
     (\BEXP2MU a.
        case a of
           T -> I T
        || B_PROP b -> I AP b
        || ~be -> I ~BEXP2MU be
        || B_AND (be1,be2) -> I (BEXP2MU be1 /\ BEXP2MU be2))

CTL2MU_primitive_def

|- CTL2MU =
   WFREC
     (@R.
        WF R /\ (!f. R f ~f) /\ (!f g. R g (C_AND (f,g))) /\
        (!g f. R f (C_AND (f,g))) /\ (!f. R f (C_EX f)) /\
        (!f. R f (C_EG f)) /\ (!g f. R f (C_EU (f,g))) /\
        !f g. R g (C_EU (f,g)))
     (\CTL2MU a.
        case a of
           C_BOOL b -> I (BEXP2MU b)
        || ~f -> I ~CTL2MU f
        || C_AND (f',g) -> I (CTL2MU f' /\ CTL2MU g)
        || C_EX f'' -> I <<".">> (CTL2MU f'')
        || C_EU (f'''',g') ->
             I (mu "Q".. CTL2MU g' \/ CTL2MU f'''' /\ <<".">> (RV "Q"))
        || C_EG f''' -> I nu "Q".. CTL2MU f''' /\ <<".">> (RV "Q"))

ctl2muks_def

|- !M.
     ctl2muks M =
     <|S := M.S; S0 := M.S0; T := (\q. M.R); ap := M.P; L := M.L|>

Nf2_def

|- (!R s. Nf2 R s 0 = s) /\ !R s n. Nf2 R s (SUC n) = @r. R (Nf2 R s n,r)

unc_def

|- !R. unc R = (\x y. R (x,y))

Nf_def

|- (!R s q. Nf R s q 0 = s) /\
   !R s q n. Nf R s q (SUC n) = (if n = 0 then q else @r. R (Nf R s q n,r))

Nf3_def

|- (!R x q. Nf3 R x q 0 = x) /\
   !R x q n. Nf3 R x q (SUC n) = (if n = 0 then q else @r. R (Nf3 R x q n,r))

GFP_def

|- (!M f. GFP M f 0 = UNIV) /\
   !M f n.
     GFP M f (SUC n) =
     C_SEM M f INTER {s | ?s'. M.R (s,s') /\ s' IN GFP M f n}

Nf4_def

|- (!R P. Nf4 R P 0 = ARB) /\
   !R P n. Nf4 R P (SUC n) = @r. R (Nf4 R P n,r) /\ P r

P1_def

|- !P R s. P1 P R s = R (ARB,s) /\ P s

P2_def

|- !P R n s. P2 P R n s = R (Nf4 R P n,s) /\ P s

P3_def

|- !P R n s. P3 P R n s = R ((@r. P2 P R n r),s) /\ P s

Nf5_def

|- (!R P s. Nf5 R P s 0 = s) /\
   !R P s n. Nf5 R P s (SUC n) = @r. R (Nf5 R P s n,r) /\ P r

P4_def

|- !R P s s'. P4 R P s s' = R (s,s') /\ P s'

P5_def

|- !R P s n s'. P5 R P s n s' = R (Nf5 R P s n,s') /\ P s'

P6_def

|- !R P s n s'. P6 R P s n s' = R ((@r. P5 R P s n r),s') /\ P s'

LFP_def

|- (!M f g. LFP M f g 0 = {}) /\
   !M f g n.
     LFP M f g (SUC n) =
     C_SEM M g UNION
     C_SEM M f INTER {s | ?s'. M.R (s,s') /\ s' IN LFP M f g n}

FIN_PFX_def

|- (!l. FIN_PFX l 0 = []) /\ !l n. FIN_PFX l (SUC n) = HD l::FIN_PFX (TL l) n

INF_PFX_def

|- (!f. INF_PFX f 0 = []) /\
   !f n. INF_PFX f (SUC n) = SNOC (f n) (INF_PFX f n)

PREFIX_def

|- (!l n. PREFIX (FINITE l) n = FIN_PFX l n) /\
   !f n. PREFIX (INFINITE f) n = INF_PFX f n

Theorems

BEXP2MU_ind

|- !P.
     P T /\ (!b. P (B_PROP b)) /\ (!be. P be ==> P ~be) /\
     (!be1 be2. P be1 /\ P be2 ==> P (B_AND (be1,be2))) ==>
     !v. P v

BEXP2MU_def

|- (BEXP2MU T = T) /\ (BEXP2MU (B_PROP b) = AP b) /\
   (BEXP2MU ~be = ~BEXP2MU be) /\
   (BEXP2MU (B_AND (be1,be2)) = BEXP2MU be1 /\ BEXP2MU be2)

CTL2MU_ind

|- !P.
     (!b. P (C_BOOL b)) /\ (!f. P f ==> P ~f) /\
     (!f g. P f /\ P g ==> P (C_AND (f,g))) /\ (!f. P f ==> P (C_EX f)) /\
     (!f. P f ==> P (C_EG f)) /\ (!f g. P f /\ P g ==> P (C_EU (f,g))) ==>
     !v. P v

CTL2MU_def

|- (CTL2MU (C_BOOL b) = BEXP2MU b) /\ (CTL2MU ~f = ~CTL2MU f) /\
   (CTL2MU (C_AND (f,g)) = CTL2MU f /\ CTL2MU g) /\
   (CTL2MU (C_EX f) = <<".">> (CTL2MU f)) /\
   (CTL2MU (C_EG f) = nu "Q".. CTL2MU f /\ <<".">> (RV "Q")) /\
   (CTL2MU (C_EU (f,g)) = mu "Q".. CTL2MU g \/ CTL2MU f /\ <<".">> (RV "Q"))

REST_RESTN

|- !p. REST p = RESTN p 1

ELEM_REST

|- !p n. ELEM (REST p) n = ELEM p (n + 1)

PATH_REST

|- !p M s. PATH M p s ==> PATH M (REST p) (ELEM p 1)

unc_thm

|- !P x y. P (x,y) = unc P x y

FV_BEXP2MU

|- !b. FV (BEXP2MU b) = {}

FV_CTL2MU

|- !f. FV (CTL2MU f) = {}

IMF_CTL_LEM

|- !f Q. IMF (CTL2MU f) ==> ~(~RV Q SUBF NNF (CTL2MU f))

IMF_CTL

|- !f. IMF (CTL2MU f)

STATES_FV_ENV_INV_SPEC

|- !f M X.
     STATES (CTL2MU f) (ctl2muks M) EMPTY_ENV[[["Q"<--X]]] =
     STATES (CTL2MU f) (ctl2muks M) EMPTY_ENV

INF_PREFIX_LENGTH

|- !f k. LENGTH (PREFIX (INFINITE f) k) = k

IDX_BIGUNION

|- !P s. s IN BIGUNION {p | ?i. p = P i} = ?i. s IN P i

CTL2MU

|- !f M.
     TOTAL M.R /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S ==>
     (C_SEM M f = MU_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV)

CTL2MU_MODEL

|- !f M.
     TOTAL M.R /\ wfKS (ctl2muks M) /\ FINITE (ctl2muks M).S ==>
     (CTL_MODEL_SAT M f = MU_MODEL_SAT (CTL2MU f) (ctl2muks M) EMPTY_ENV)