Theory "reach"

Parents setLemmas

Signature

Constant	Type
ReachableRec	:('a # 'a -> bool) -> ('a -> bool) -> num -> 'a -> bool
Reachable	:('a # 'a -> bool) -> ('a -> bool) -> 'a -> bool
ReachNext	:('b # 'c -> 'a) -> 'b -> 'c -> 'a

Definitions

ReachNext_def

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

ReachableRec_def

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

Reachable_def

|- !R s. Reachable R s = BIGUNION {P | ?n. P = ReachableRec R s n}

Theorems

ReachableRecSimp

|- !R s n state.
     ReachableRec R s (SUC n) state =
     ReachableRec R s n state \/
     ?state'. R (state',state) /\ ReachableRec R s n state'

ReachableFP

|- !R s n'.
     (ReachableRec R s n' = ReachableRec R s (SUC n')) ==>
     (Reachable R s = ReachableRec R s n')