Theory "cear"

Parents mu Omega int_arith

Signature

Constant	Type
SCC	:('a # 'a -> bool) -> 'a -> 'a -> bool
ReachToRec	:('a # 'a -> bool) -> 'a -> num -> 'a -> bool
ReachTo	:('a # 'a -> bool) -> 'a -> 'a -> bool
ReachFromRec	:('a # 'a -> bool) -> 'a -> num -> 'a -> bool
ReachFrom	:('a # 'a -> bool) -> 'a -> 'a -> bool
R_TRANS	:('a # 'a -> bool) -> bool
R_SYM	:('a # 'a -> 'b) -> bool
R_REFL	:('a # 'a -> bool) -> bool
R_EQR	:('a # 'a -> bool) -> bool
QP3	:('b # 'c -> 'a) # 'b -> 'c -> 'a
QP2	:('b # 'c -> 'a) -> 'b -> 'c -> 'a
Prev	:('b # 'c -> 'a) -> 'c -> 'b -> 'a
Next	:('b # 'c -> 'a) -> 'b -> 'c -> 'a
IS_ABS_FUN	:('prop, 'state) KS -> (string -> 'state -> bool) -> ('state # 'astate -> bool) -> bool
ABS_KS	:('c, 'a) KS -> ('a # 'b -> bool) -> ('c, 'b) KS

Definitions

Next_def

|- !R s s'. Next R s s' = R (s,s')

Prev_def

|- !R s s'. Prev R s s' = R (s',s)

ReachFromRec_def

|- (!R s. ReachFromRec R s 0 = {s}) /\
   !R s n.
     ReachFromRec R s (SUC n) =
     {s' |
      s' IN ReachFromRec R s n \/
      ?s''. Next R s'' s' /\ s'' IN ReachFromRec R s n}

ReachFrom_def

|- !R s. ReachFrom R s = BIGUNION {P | ?n. P = ReachFromRec R s n}

ReachToRec_def

|- (!R s. ReachToRec R s 0 = {s}) /\
   !R s n.
     ReachToRec R s (SUC n) =
     {s' |
      s' IN ReachToRec R s n \/
      ?s''. Prev R s'' s' /\ s'' IN ReachToRec R s n}

ReachTo_def

|- !R s. ReachTo R s = BIGUNION {P | ?n. P = ReachToRec R s n}

R_REFL_def

|- !R. R_REFL R = !x. R (x,x)

R_SYM_def

|- !R. R_SYM R = !x y. R (x,y) = R (y,x)

R_TRANS_def

|- !R. R_TRANS R = !x y z. R (x,y) /\ R (y,z) ==> R (x,z)

R_EQR_def

|- !R. R_EQR R = R_REFL R /\ R_SYM R /\ R_TRANS R

QP2_def

|- !h q q'. QP2 h q q' = h (q,q')

QP3_def

|- !h q q'. QP3 (h,q) q' = QP2 h q q'

IS_ABS_FUN_def

|- !ks e h.
     IS_ABS_FUN ks e h =
     (!s. ?sh. h (s,sh)) /\
     !s1 s2 sh.
       h (s1,sh) /\ h (s2,sh) ==>
       !p.
         p IN ks.ap ==> (s1 IN STATES (AP p) ks e = s2 IN STATES (AP p) ks e)

Theorems

ReachFromFP

|- !R s n'.
     (ReachFromRec R s n' = ReachFromRec R s (SUC n')) ==>
     (ReachFrom R s = ReachFromRec R s n')

ReachToFP

|- !R s n'.
     (ReachToRec R s n' = ReachToRec R s (SUC n')) ==>
     (ReachTo R s = ReachToRec R s n')

ReachToClosed

|- !si R s. R_EQR R ==> (s IN ReachTo R si = R (s,si))

ReachFromClosed

|- !si R s. R_EQR R ==> (s IN ReachFrom R si = R (si,s))

SCC_def

|- !R s. SCC R s = ReachFrom R s UNION ReachTo R s

ABS_KS_def

|- !M h.
     ABS_KS M h =
     <|S := UNIV; S0 := {sh | ?s'. s' IN M.S0 /\ h (s',sh)};
       T :=
         (\a (sh,sh'). ?s' s''. M.T a (s',s'') /\ h (s',sh) /\ h (s'',sh'));
       L := (\sh. BIGUNION {X | ?s. (X = M.L s) /\ h (s,sh)})|>

wf_absKS

|- !ks h. wfKS ks ==> wfKS (ABS_KS ks h)

ABS_CONS_LEM

|- !f h ks s sh e eh.
     wfKS ks ==>
     (!Q. ~(~RV Q SUBF NNF f)) ==>
     (!s. ?sh. h (s,sh)) ==>
     (!a g. ~(<> g SUBF NNF f)) ==>
     (!p. AP p SUBF f ==> p IN ks.ap) ==>
     (!s1 s2 sh.
        h (s1,sh) /\ h (s2,sh) ==>
        !p.
          p IN ks.ap ==>
          (s1 IN STATES (AP p) ks e = s2 IN STATES (AP p) ks e)) ==>
     (!Q s sh. h (s,sh) ==> sh IN eh Q ==> s IN e Q) ==>
     h (s,sh) ==>
     sh IN STATES (NNF f) (ABS_KS ks h) eh ==>
     s IN STATES (NNF f) ks e

ABS_CONS_STATES

|- !f h ks s sh e eh.
     wfKS ks ==>
     (!Q. ~(~RV Q SUBF NNF f)) ==>
     (!s. ?sh. h (s,sh)) ==>
     (!a g. ~(<> g SUBF NNF f)) ==>
     (!p. AP p SUBF f ==> p IN ks.ap) ==>
     (!s1 s2 sh.
        h (s1,sh) /\ h (s2,sh) ==>
        !p.
          p IN ks.ap ==>
          (s1 IN STATES (AP p) ks e = s2 IN STATES (AP p) ks e)) ==>
     (!Q s sh. h (s,sh) ==> sh IN eh Q ==> s IN e Q) ==>
     h (s,sh) ==>
     sh IN STATES f (ABS_KS ks h) eh ==>
     s IN STATES f ks e

ABS_INIT

|- !ks h s sh. h (s,sh) ==> s IN ks.S0 ==> sh IN (ABS_KS ks h).S0

ABS_REACH

|- !ks h a s sh.
     (!s. ?sh. h (s,sh)) ==>
     h (s,sh) ==>
     s IN Reachable (ks.T a) ks.S0 ==>
     sh IN Reachable ((ABS_KS ks h).T a) (ABS_KS ks h).S0

ABS_CONS_MODEL

|- !f h ks e eh.
     wfKS ks ==>
     (!Q. ~(~RV Q SUBF NNF f)) ==>
     (!a g. ~(<> g SUBF NNF f)) ==>
     (!p. AP p SUBF f ==> p IN ks.ap) ==>
     IS_ABS_FUN ks e h ==>
     (!Q s sh. h (s,sh) ==> sh IN eh Q ==> s IN e Q) ==>
     MU_MODEL_SAT f (ABS_KS ks h) eh ==>
     MU_MODEL_SAT f ks e

SCC_FOLD_BASE

|- !f g pf R s sh k.
     (s IN {s | !i. i <= k ==> SCC (R i) (f i 0) (pf i s)} = g 0 sh) /\
     (s IN {s | !i. i <= k ==> SCC (R i) (f i 1) (pf i s)} = g 1 sh) =
     s IN
     {s |
      !j.
        j <= 1 ==>
        (s IN {s | !i. i <= k ==> pf i s IN SCC (R i) (f i j)} = g j sh)}

SCC_FOLD_STEP

|- !f g pf R s sh k n.
     s IN
     {s |
      !j.
        j <= n ==>
        (s IN {s | !i. i <= k ==> SCC (R i) (f i j) (pf i s)} = g j sh)} /\
     (s IN {s | !i. i <= k ==> SCC (R i) (f i (SUC n)) (pf i s)} =
      g (SUC n) sh) =
     s IN
     {s |
      !j.
        j <= SUC n ==>
        (s IN {s | !i. i <= k ==> SCC (R i) (f i j) (pf i s)} = g j sh)}

SCC_INNER_FOLD_BASE1

|- !R j f pf s.
     SCC (R 0) (f 0 j) (pf 0 s) =
     s IN {s | !i. i <= 0 ==> SCC (R i) (f i j) (pf i s)}

SCC_INNER_FOLD_BASE

|- !f pf R s sh j.
     SCC (R 0) (f 0 j) (pf 0 s) /\ SCC (R 1) (f 1 j) (pf 1 s) =
     s IN {s | !i. i <= 1 ==> pf i s IN SCC (R i) (f i j)}

SCC_INNER_FOLD_STEP

|- !f pf R s sh j n.
     s IN {s | !i. i <= n ==> pf i s IN SCC (R i) (f i j)} /\
     SCC (R (SUC n)) (f (SUC n) j) (pf (SUC n) s) =
     s IN {s | !i. i <= SUC n ==> pf i s IN SCC (R i) (f i j)}

SCC_REL

|- !R s si. R_EQR R ==> (s IN SCC R si = R (s,si))

SCC_REL_IMP

|- !R s1 s2 si. R_EQR R ==> s1 IN SCC R si /\ s2 IN SCC R si ==> R (s1,s2)

BIGOR_OVER_AND

|- !P Q k.
     (?i. i <= k /\ P i) /\ (?i. i <= k /\ Q i) =
     ?i j. i <= k /\ j <= k /\ P i /\ Q j

abst_lem1

|- !f sh k i j.
     (!i. i <= k /\ f i sh ==> !j. j <= k /\ f j sh ==> (i = j)) ==>
     i <= k /\ j <= k /\ f i sh /\ f j sh ==>
     (i = j)