Theory "quotient_option"

Parents quotient

Signature

Constant	Type
OPTION_REL_tupled	:('a -> 'a -> bool) # 'a option # 'a option -> bool
OPTION_REL	:('a -> 'a -> bool) -> 'a option -> 'a option -> bool

Definitions

OPTION_REL_tupled_primitive_def

|- OPTION_REL_tupled =
   WFREC (@R'. WF R')
     (\OPTION_REL_tupled a.
        case a of
           (R,NONE,NONE) -> I T
        || (R,NONE,SOME y) -> I F
        || (R,SOME x,NONE) -> I F
        || (R,SOME x,SOME y') -> I (R x y'))

OPTION_REL_curried_def

|- !x x1 x2. OPTION_REL x x1 x2 = OPTION_REL_tupled (x,x1,x2)

Theorems

OPTION_MAP_I

|- OPTION_MAP I = I

OPTION_REL_ind

|- !P.
     (!R. P R NONE NONE) /\ (!R x. P R (SOME x) NONE) /\
     (!R y. P R NONE (SOME y)) /\ (!R x y. P R (SOME x) (SOME y)) ==>
     !v v1 v2. P v v1 v2

OPTION_REL_def

|- (OPTION_REL R NONE NONE = T) /\ (OPTION_REL R (SOME x) NONE = F) /\
   (OPTION_REL R NONE (SOME y) = F) /\
   (OPTION_REL R (SOME x) (SOME y) = R x y)

OPTION_REL_EQ

|- OPTION_REL $= = $=

OPTION_EQUIV

|- !R. EQUIV R ==> EQUIV (OPTION_REL R)

OPTION_QUOTIENT

|- !R abs rep.
     QUOTIENT R abs rep ==>
     QUOTIENT (OPTION_REL R) (OPTION_MAP abs) (OPTION_MAP rep)

NONE_PRS

|- !R abs rep. QUOTIENT R abs rep ==> (NONE = OPTION_MAP abs NONE)

NONE_RSP

|- !R abs rep. QUOTIENT R abs rep ==> OPTION_REL R NONE NONE

SOME_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==> !x. SOME x = OPTION_MAP abs (SOME (rep x))

SOME_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==> !x y. R x y ==> OPTION_REL R (SOME x) (SOME y)

IS_SOME_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==> !x. IS_SOME x = IS_SOME (OPTION_MAP rep x)

IS_SOME_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==> !x y. OPTION_REL R x y ==> (IS_SOME x = IS_SOME y)

IS_NONE_PRS

|- !R abs rep.
     QUOTIENT R abs rep ==> !x. IS_NONE x = IS_NONE (OPTION_MAP rep x)

IS_NONE_RSP

|- !R abs rep.
     QUOTIENT R abs rep ==> !x y. OPTION_REL R x y ==> (IS_NONE x = IS_NONE y)

OPTION_MAP_PRS

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !a f.
         OPTION_MAP f a =
         OPTION_MAP abs2 (OPTION_MAP ((abs1 --> rep2) f) (OPTION_MAP rep1 a))

OPTION_MAP_RSP

|- !R1 abs1 rep1.
     QUOTIENT R1 abs1 rep1 ==>
     !R2 abs2 rep2.
       QUOTIENT R2 abs2 rep2 ==>
       !a1 a2 f1 f2.
         (R1 ===> R2) f1 f2 /\ OPTION_REL R1 a1 a2 ==>
         OPTION_REL R2 (OPTION_MAP f1 a1) (OPTION_MAP f2 a2)