Theory "ks"

Parents string pred_set

Signature

Type	Arity
KS	2
Constant	Type
wfKS	:('a, 'b) KS -> bool
mk_KS	:(('state -> bool) # ('state -> bool) # (string -> 'state # 'state -> bool) # ('prop -> bool) # ('state -> 'prop -> bool)) recspace -> ('prop, 'state) KS
ks0	:('state -> bool) -> ('state -> bool) -> (string -> 'state # 'state -> bool) -> ('prop -> bool) -> ('state -> 'prop -> bool) -> ('prop, 'state) KS
dest_KS	:('prop, 'state) KS -> (('state -> bool) # ('state -> bool) # (string -> 'state # 'state -> bool) # ('prop -> bool) # ('state -> 'prop -> bool)) recspace
TOTAL	:('a # 'b -> bool) -> bool
KS_size	:('prop -> num) -> ('state -> num) -> ('prop, 'state) KS -> num
KS_case	:(('state -> bool) -> ('state -> bool) -> (string -> 'state # 'state -> bool) -> ('prop -> bool) -> ('state -> 'prop -> bool) -> 'a) -> ('prop, 'state) KS -> 'a
KS_ap_fupd	:(('prop -> bool) -> 'prop -> bool) -> ('prop, 'state) KS -> ('prop, 'state) KS
KS_ap	:('prop, 'state) KS -> 'prop -> bool
KS_T_fupd	:((string -> 'state # 'state -> bool) -> string -> 'state # 'state -> bool) -> ('prop, 'state) KS -> ('prop, 'state) KS
KS_TRANSITION	:'state -> ('a, 'state) KS -> string -> 'state -> bool
KS_T	:('prop, 'state) KS -> string -> 'state # 'state -> bool
KS_S_fupd	:(('state -> bool) -> 'state -> bool) -> ('prop, 'state) KS -> ('prop, 'state) KS
KS_S0_fupd	:(('state -> bool) -> 'state -> bool) -> ('prop, 'state) KS -> ('prop, 'state) KS
KS_S0	:('prop, 'state) KS -> 'state -> bool
KS_S	:('prop, 'state) KS -> 'state -> bool
KS_L_fupd	:(('state -> 'prop -> bool) -> 'state -> 'prop -> bool) -> ('prop, 'state) KS -> ('prop, 'state) KS
KS_L	:('prop, 'state) KS -> 'state -> 'prop -> bool
KS	:('state -> bool) -> ('state -> bool) -> (string -> 'state # 'state -> bool) -> ('prop -> bool) -> ('state -> 'prop -> bool) -> ('prop, 'state) KS
BISIM	:('a, 'b) KS -> ('c, 'd) KS -> ('b # 'd -> bool) -> bool

Definitions

KS_TY_DEF

|- ?rep.
     TYPE_DEFINITION
       (\a0'.
          !'KS'.
            (!a0'.
               (?a0 a1 a2 a3 a4.
                  a0' =
                  (\a0 a1 a2 a3 a4.
                     ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (\n. ind_type$BOTTOM))
                    a0 a1 a2 a3 a4) ==>
               'KS' a0') ==>
            'KS' a0') rep

KS_repfns

|- (!a. mk_KS (dest_KS a) = a) /\
   !r.
     (\a0'.
        !'KS'.
          (!a0'.
             (?a0 a1 a2 a3 a4.
                a0' =
                (\a0 a1 a2 a3 a4.
                   ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (\n. ind_type$BOTTOM))
                  a0 a1 a2 a3 a4) ==>
             'KS' a0') ==>
          'KS' a0') r =
     (dest_KS (mk_KS r) = r)

ks0_def

|- ks0 =
   (\a0 a1 a2 a3 a4.
      mk_KS
        ((\a0 a1 a2 a3 a4.
            ind_type$CONSTR 0 (a0,a1,a2,a3,a4) (\n. ind_type$BOTTOM)) a0 a1 a2
           a3 a4))

KS

|- KS = ks0

KS_case_def

|- !f a0 a1 a2 a3 a4. KS_case f (KS a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4

KS_size_def

|- !f f1 a0 a1 a2 a3 a4. KS_size f f1 (KS a0 a1 a2 a3 a4) = 1

KS_S

|- !f f0 f1 f2 f3. (KS f f0 f1 f2 f3).S = f

KS_S0

|- !f f0 f1 f2 f3. (KS f f0 f1 f2 f3).S0 = f0

KS_T

|- !f f0 f1 f2 f3. (KS f f0 f1 f2 f3).T = f1

KS_ap

|- !f f0 f1 f2 f3. (KS f f0 f1 f2 f3).ap = f2

KS_L

|- !f f0 f1 f2 f3. (KS f f0 f1 f2 f3).L = f3

KS_S_fupd

|- !f4 f f0 f1 f2 f3.
     KS f f0 f1 f2 f3 with S updated_by f4 = KS (f4 f) f0 f1 f2 f3

KS_S0_fupd

|- !f4 f f0 f1 f2 f3.
     KS f f0 f1 f2 f3 with S0 updated_by f4 = KS f (f4 f0) f1 f2 f3

KS_T_fupd

|- !f4 f f0 f1 f2 f3.
     KS f f0 f1 f2 f3 with T updated_by f4 = KS f f0 (f4 f1) f2 f3

KS_ap_fupd

|- !f4 f f0 f1 f2 f3.
     KS f f0 f1 f2 f3 with ap updated_by f4 = KS f f0 f1 (f4 f2) f3

KS_L_fupd

|- !f4 f f0 f1 f2 f3.
     KS f f0 f1 f2 f3 with L updated_by f4 = KS f f0 f1 f2 (f4 f3)

wfKS_def

|- !ks. wfKS ks = ks.S0 SUBSET ks.S /\ (ks.S = UNIV)

KS_TRANSITION_def

|- !p ks a q. p>--ks/a-->q = ks.T a (p,q)

TOTAL_def

|- !R. TOTAL R = !s. ?s'. R (s,s')

BISIM_def

|- !M1 M2 BS.
     BISIM M1 M2 BS =
     !a s1 s2.
       (!s1'.
          BS (s1,s2) /\ M1.T a (s1,s1') ==>
          ?s2'. M2.T a (s2,s2') /\ BS (s1',s2')) /\
       !s2'.
         BS (s1,s2) /\ M2.T a (s2,s2') ==>
         ?s1'. M1.T a (s1,s1') /\ BS (s1',s2')

Theorems

KS_accessors

|- (!f f0 f1 f2 f3. (KS f f0 f1 f2 f3).S = f) /\
   (!f f0 f1 f2 f3. (KS f f0 f1 f2 f3).S0 = f0) /\
   (!f f0 f1 f2 f3. (KS f f0 f1 f2 f3).T = f1) /\
   (!f f0 f1 f2 f3. (KS f f0 f1 f2 f3).ap = f2) /\
   !f f0 f1 f2 f3. (KS f f0 f1 f2 f3).L = f3

KS_fn_updates

|- (!f4 f f0 f1 f2 f3.
      KS f f0 f1 f2 f3 with S updated_by f4 = KS (f4 f) f0 f1 f2 f3) /\
   (!f4 f f0 f1 f2 f3.
      KS f f0 f1 f2 f3 with S0 updated_by f4 = KS f (f4 f0) f1 f2 f3) /\
   (!f4 f f0 f1 f2 f3.
      KS f f0 f1 f2 f3 with T updated_by f4 = KS f f0 (f4 f1) f2 f3) /\
   (!f4 f f0 f1 f2 f3.
      KS f f0 f1 f2 f3 with ap updated_by f4 = KS f f0 f1 (f4 f2) f3) /\
   !f4 f f0 f1 f2 f3.
     KS f f0 f1 f2 f3 with L updated_by f4 = KS f f0 f1 f2 (f4 f3)

KS_accfupds

|- (!f K. (K with S0 updated_by f).S = K.S) /\
   (!f K. (K with T updated_by f).S = K.S) /\
   (!f K. (K with ap updated_by f).S = K.S) /\
   (!f K. (K with L updated_by f).S = K.S) /\
   (!f K. (K with S updated_by f).S0 = K.S0) /\
   (!f K. (K with T updated_by f).S0 = K.S0) /\
   (!f K. (K with ap updated_by f).S0 = K.S0) /\
   (!f K. (K with L updated_by f).S0 = K.S0) /\
   (!f K. (K with S updated_by f).T = K.T) /\
   (!f K. (K with S0 updated_by f).T = K.T) /\
   (!f K. (K with ap updated_by f).T = K.T) /\
   (!f K. (K with L updated_by f).T = K.T) /\
   (!f K. (K with S updated_by f).ap = K.ap) /\
   (!f K. (K with S0 updated_by f).ap = K.ap) /\
   (!f K. (K with T updated_by f).ap = K.ap) /\
   (!f K. (K with L updated_by f).ap = K.ap) /\
   (!f K. (K with S updated_by f).L = K.L) /\
   (!f K. (K with S0 updated_by f).L = K.L) /\
   (!f K. (K with T updated_by f).L = K.L) /\
   (!f K. (K with ap updated_by f).L = K.L) /\
   (!f K. (K with S updated_by f).S = f K.S) /\
   (!f K. (K with S0 updated_by f).S0 = f K.S0) /\
   (!f K. (K with T updated_by f).T = f K.T) /\
   (!f K. (K with ap updated_by f).ap = f K.ap) /\
   !f K. (K with L updated_by f).L = f K.L

KS_fupdfupds

|- (!g f K.
      K with <|S updated_by f; S updated_by g|> =
      K with S updated_by f o g) /\
   (!g f K.
      K with <|S0 updated_by f; S0 updated_by g|> =
      K with S0 updated_by f o g) /\
   (!g f K.
      K with <|T updated_by f; T updated_by g|> =
      K with T updated_by f o g) /\
   (!g f K.
      K with <|ap updated_by f; ap updated_by g|> =
      K with ap updated_by f o g) /\
   !g f K.
     K with <|L updated_by f; L updated_by g|> = K with L updated_by f o g

KS_fupdfupds_comp

|- ((!g f. KS_S_fupd f o KS_S_fupd g = KS_S_fupd (f o g)) /\
    !h g f. KS_S_fupd f o KS_S_fupd g o h = KS_S_fupd (f o g) o h) /\
   ((!g f. KS_S0_fupd f o KS_S0_fupd g = KS_S0_fupd (f o g)) /\
    !h g f. KS_S0_fupd f o KS_S0_fupd g o h = KS_S0_fupd (f o g) o h) /\
   ((!g f. KS_T_fupd f o KS_T_fupd g = KS_T_fupd (f o g)) /\
    !h g f. KS_T_fupd f o KS_T_fupd g o h = KS_T_fupd (f o g) o h) /\
   ((!g f. KS_ap_fupd f o KS_ap_fupd g = KS_ap_fupd (f o g)) /\
    !h g f. KS_ap_fupd f o KS_ap_fupd g o h = KS_ap_fupd (f o g) o h) /\
   (!g f. KS_L_fupd f o KS_L_fupd g = KS_L_fupd (f o g)) /\
   !h g f. KS_L_fupd f o KS_L_fupd g o h = KS_L_fupd (f o g) o h

KS_fupdcanon

|- (!g f K.
      K with <|S0 updated_by f; S updated_by g|> =
      K with <|S updated_by g; S0 updated_by f|>) /\
   (!g f K.
      K with <|T updated_by f; S updated_by g|> =
      K with <|S updated_by g; T updated_by f|>) /\
   (!g f K.
      K with <|T updated_by f; S0 updated_by g|> =
      K with <|S0 updated_by g; T updated_by f|>) /\
   (!g f K.
      K with <|ap updated_by f; S updated_by g|> =
      K with <|S updated_by g; ap updated_by f|>) /\
   (!g f K.
      K with <|ap updated_by f; S0 updated_by g|> =
      K with <|S0 updated_by g; ap updated_by f|>) /\
   (!g f K.
      K with <|ap updated_by f; T updated_by g|> =
      K with <|T updated_by g; ap updated_by f|>) /\
   (!g f K.
      K with <|L updated_by f; S updated_by g|> =
      K with <|S updated_by g; L updated_by f|>) /\
   (!g f K.
      K with <|L updated_by f; S0 updated_by g|> =
      K with <|S0 updated_by g; L updated_by f|>) /\
   (!g f K.
      K with <|L updated_by f; T updated_by g|> =
      K with <|T updated_by g; L updated_by f|>) /\
   !g f K.
     K with <|L updated_by f; ap updated_by g|> =
     K with <|ap updated_by g; L updated_by f|>

KS_fupdcanon_comp

|- ((!g f. KS_S0_fupd f o KS_S_fupd g = KS_S_fupd g o KS_S0_fupd f) /\
    !h g f.
      KS_S0_fupd f o KS_S_fupd g o h = KS_S_fupd g o KS_S0_fupd f o h) /\
   ((!g f. KS_T_fupd f o KS_S_fupd g = KS_S_fupd g o KS_T_fupd f) /\
    !h g f. KS_T_fupd f o KS_S_fupd g o h = KS_S_fupd g o KS_T_fupd f o h) /\
   ((!g f. KS_T_fupd f o KS_S0_fupd g = KS_S0_fupd g o KS_T_fupd f) /\
    !h g f.
      KS_T_fupd f o KS_S0_fupd g o h = KS_S0_fupd g o KS_T_fupd f o h) /\
   ((!g f. KS_ap_fupd f o KS_S_fupd g = KS_S_fupd g o KS_ap_fupd f) /\
    !h g f.
      KS_ap_fupd f o KS_S_fupd g o h = KS_S_fupd g o KS_ap_fupd f o h) /\
   ((!g f. KS_ap_fupd f o KS_S0_fupd g = KS_S0_fupd g o KS_ap_fupd f) /\
    !h g f.
      KS_ap_fupd f o KS_S0_fupd g o h = KS_S0_fupd g o KS_ap_fupd f o h) /\
   ((!g f. KS_ap_fupd f o KS_T_fupd g = KS_T_fupd g o KS_ap_fupd f) /\
    !h g f.
      KS_ap_fupd f o KS_T_fupd g o h = KS_T_fupd g o KS_ap_fupd f o h) /\
   ((!g f. KS_L_fupd f o KS_S_fupd g = KS_S_fupd g o KS_L_fupd f) /\
    !h g f. KS_L_fupd f o KS_S_fupd g o h = KS_S_fupd g o KS_L_fupd f o h) /\
   ((!g f. KS_L_fupd f o KS_S0_fupd g = KS_S0_fupd g o KS_L_fupd f) /\
    !h g f.
      KS_L_fupd f o KS_S0_fupd g o h = KS_S0_fupd g o KS_L_fupd f o h) /\
   ((!g f. KS_L_fupd f o KS_T_fupd g = KS_T_fupd g o KS_L_fupd f) /\
    !h g f. KS_L_fupd f o KS_T_fupd g o h = KS_T_fupd g o KS_L_fupd f o h) /\
   (!g f. KS_L_fupd f o KS_ap_fupd g = KS_ap_fupd g o KS_L_fupd f) /\
   !h g f. KS_L_fupd f o KS_ap_fupd g o h = KS_ap_fupd g o KS_L_fupd f o h

KS_component_equality

|- !K1 K2.
     (K1 = K2) =
     (K1.S = K2.S) /\ (K1.S0 = K2.S0) /\ (K1.T = K2.T) /\ (K1.ap = K2.ap) /\
     (K1.L = K2.L)

KS_updates_eq_literal

|- !K f3 f2 f1 f0 f.
     K with <|S := f3; S0 := f2; T := f1; ap := f0; L := f|> =
     <|S := f3; S0 := f2; T := f1; ap := f0; L := f|>

KS_literal_nchotomy

|- !K. ?f3 f2 f1 f0 f. K = <|S := f3; S0 := f2; T := f1; ap := f0; L := f|>

FORALL_KS

|- !P.
     (!K. P K) =
     !f3 f2 f1 f0 f. P <|S := f3; S0 := f2; T := f1; ap := f0; L := f|>

EXISTS_KS

|- !P.
     (?K. P K) =
     ?f3 f2 f1 f0 f. P <|S := f3; S0 := f2; T := f1; ap := f0; L := f|>

KS_literal_11

|- !f31 f21 f11 f01 f1 f32 f22 f12 f02 f2.
     (<|S := f31; S0 := f21; T := f11; ap := f01; L := f1|> =
      <|S := f32; S0 := f22; T := f12; ap := f02; L := f2|>) =
     (f31 = f32) /\ (f21 = f22) /\ (f11 = f12) /\ (f01 = f02) /\ (f1 = f2)

datatype_KS

|- DATATYPE (record KS S S0 T ap L)

KS_11

|- !a0 a1 a2 a3 a4 a0' a1' a2' a3' a4'.
     (KS a0 a1 a2 a3 a4 = KS a0' a1' a2' a3' a4') =
     (a0 = a0') /\ (a1 = a1') /\ (a2 = a2') /\ (a3 = a3') /\ (a4 = a4')

KS_case_cong

|- !M M' f.
     (M = M') /\
     (!a0 a1 a2 a3 a4.
        (M' = KS a0 a1 a2 a3 a4) ==>
        (f a0 a1 a2 a3 a4 = f' a0 a1 a2 a3 a4)) ==>
     (KS_case f M = KS_case f' M')

KS_nchotomy

|- !K'. ?f f0 f1 f2 f3. K' = KS f f0 f1 f2 f3

KS_Axiom

|- !f. ?fn. !a0 a1 a2 a3 a4. fn (KS a0 a1 a2 a3 a4) = f a0 a1 a2 a3 a4

KS_induction

|- !P. (!f f0 f1 f2 f3. P (KS f f0 f1 f2 f3)) ==> !K'. P K'

wfKS_UNIV

|- !ks. ks.S0 SUBSET UNIV /\ (ks.S = UNIV) ==> wfKS ks

DECIDE_AP_EQ_LEM

|- !x y. ~(x = y) = (((\s. x) = (\s. y)) = F)

TOTAL_THM

|- !R. TOTAL (\(s,s'). R (s,s') \/ ~(?s'. R (s,s')) /\ (s' = s))