Theory: HolBdd

Parents

• option
• list

Types

Constants

• Reachable  :('a # 'a -> bool) -> ('a -> bool) -> 'a -> bool
• Eq  :'a -> 'a -> bool
• ReachBy  :('a # 'a -> bool) -> ('a -> bool) -> num -> 'a -> bool
• ReachIn  :('a # 'a -> bool) -> ('a -> bool) -> num -> 'a -> bool
• Stable  :('a # 'a -> bool) -> 'a -> bool
• Live  :('a # 'b -> bool) -> bool
• IsTrace_tupled  :('a # 'a -> bool) # ('a -> bool) # ('a -> bool) # 'a list -> bool
• Next  :('a # 'b -> bool) -> ('a -> bool) -> 'b -> bool
• Prev  :('a # 'b -> bool) -> ('b -> bool) -> 'a -> bool
• IsTrace  :('a # 'a -> bool) -> ('a -> bool) -> ('a -> bool) -> 'a list -> bool

Definitions

Eq_def

|- !state0 state. Eq state0 state = (state0 = state)

IsTrace_arg_munge_def

|- !x x1 x2 x3. IsTrace x x1 x2 x3 = IsTrace_tupled (x,x1,x2,x3)

IsTrace_tupled_primitive_def

|- IsTrace_tupled =
   WFREC
     (@R'. WF R' /\ !s0 B tr Q s1 R. R' (R,Eq s1,Q,s1::tr) (R,B,Q,s0::s1::tr))
     (\IsTrace_tupled' a.
        pair_case
          (\v v1.
             pair_case
               (\v2 v3.
                  pair_case
                    (\v4 v5.
                       list_case F
                         (\v6 v7.
                            list_case (v2 v6 /\ v4 v6)
                              (\v8 v9.
                                 v2 v6 /\ v (v6,v8) /\
                                 IsTrace_tupled' (v,Eq v8,v4,v8::v9)) v7) v5)
                    v3) v1) a)

Live_def

|- !R. Live R = !state. ?state'. R (state,state')

Next_def

|- !R B state. Next R B state = ?state_. B state_ /\ R (state_,state)

Prev_def

|- !R Q state. Prev R Q state = ?state'. R (state,state') /\ Q state'

Reachable_def

|- !R B state. Reachable R B state = ?n. ReachIn R B n state

ReachBy_def

|- !R B n state. ReachBy R B n state = ?m. m <= n /\ ReachIn R B m state

ReachIn_def

|- (!R B. ReachIn R B 0 = B) /\
   !R B n. ReachIn R B (SUC n) = Next R (ReachIn R B n)

Stable_def

|- !R state. Stable R state = !state'. R (state,state') ==> (state' = state)

Theorems

ABS_EXISTS_THM

|- !P rep.
     (!x' x''. (rep x' = rep x'') ==> (x' = x'')) /\
     (!x. P x = ?x'. x = rep x') ==>
     ?abs. (!a. abs (rep a) = a) /\ !r. P r = (rep (abs r) = r)

ABS_ONE_ONE

|- !abs rep.
     (!a. abs (rep a) = a) /\ (!r. range r = (rep (abs r) = r)) ==>
     !r. range r /\ range r' ==> ((abs r = abs r') = (r = r'))

COND_SIMP

|- ((if b then F else F) = F) /\ ((if b then F else T) = ~b) /\
   ((if b then T else F) = b) /\ ((if b then T else T) = T) /\
   ((if b then x else x) = x) /\ ((if b then b' else ~b') = (b = b')) /\
   ((if b then ~b' else b') = (b = ~b'))

EQ_COND

|- ((x = (if b then y else z)) = (if b then x = y else x = z)) /\
   (((if b then y else z) = x) = (if b then y = x else z = x))

EXISTS_IMP

|- (?x. P x) ==> Q = !x. P x ==> Q

EXISTS_REP

|- !abs rep P Q.
     (!a. abs (rep a) = a) /\ (!r. P r = (rep (abs r) = r)) ==>
     ((?a. Q a) = ?r. P r /\ Q (abs r))

FORALL_REP

|- !abs rep P Q.
     (!a. abs (rep a) = a) /\ (!r. P r = (rep (abs r) = r)) ==>
     ((!a. Q a) = !r. P r ==> Q (abs r))

IsTrace_def

|- (IsTrace R B Q [] = F) /\ (IsTrace R B Q [s] = B s /\ Q s) /\
   (IsTrace R B Q (s0::s1::tr) =
    B s0 /\ R (s0,s1) /\ IsTrace R (Eq s1) Q (s1::tr))

IsTrace_ind

|- !P.
     (!R B Q. P R B Q []) /\ (!R B Q s. P R B Q [s]) /\
     (!R B Q s0 s1 tr. P R (Eq s1) Q (s1::tr) ==> P R B Q (s0::s1::tr)) ==>
     !v v1 v2 v3. P v v1 v2 v3

Prev_Next_Eq

|- !R s s'. Prev R (Eq s') s = Next R (Eq s) s'

Reachable_Stable

|- Live R /\ (!state. ReachIn R B n state ==> Stable R state) ==>
   !state. Reachable R B state /\ Stable R state = ReachIn R B n state

ReachBy_fixedpoint

|- !R B n.
     (ReachBy R B n = ReachBy R B (SUC n)) ==> (Reachable R B = ReachBy R B n)

ReachBy_ReachIn

|- (!R B state. ReachBy R B 0 state = B state) /\
   !R B n state.
     ReachBy R B (SUC n) state =
     ReachBy R B n state \/ ReachIn R B (SUC n) state

ReachBy_rec

|- (!R B state. ReachBy R B 0 state = B state) /\
   !R B n state.
     ReachBy R B (SUC n) state =
     ReachBy R B n state \/ ?state_. ReachBy R B n state_ /\ R (state_,state)

ReachIn_rec

|- (!R B state. ReachIn R B 0 state = B state) /\
   !R B n state.
     ReachIn R B (SUC n) state =
     ?state_. ReachIn R B n state_ /\ R (state_,state)