Theory: option

Parents

• one
• sum

Types

• option(Arity = 1)

Constants

• option_JOIN  :'a option option -> 'a option
• option_case  :'b -> ('a -> 'b) -> 'a option -> 'b
• NONE  :'a option
• SOME  :'a -> 'a option
• IS_NONE  :'a option -> bool
• option_ABS  :'a + one -> 'a option
• IS_SOME  :'a option -> bool
• option_APPLY  :('a -> 'b) -> 'a option -> 'b option
• option_REP  :'a option -> 'a + one
• THE  :'a option -> 'a

Definitions

IS_NONE_DEF

|- (!x. IS_NONE (SOME x) = F) /\ (IS_NONE NONE = T)

IS_SOME_DEF

|- (!x. IS_SOME (SOME x) = T) /\ (IS_SOME NONE = F)

NONE_DEF

|- NONE = option_ABS (INR one)

option_APPLY_DEF

|- (!f x. option_APPLY f (SOME x) = SOME (f x)) /\
   !f. option_APPLY f NONE = NONE

option_case_def

|- (!u f. option_case u f NONE = u) /\ !u f x. option_case u f (SOME x) = f x

option_JOIN_DEF

|- (option_JOIN NONE = NONE) /\ !x. option_JOIN (SOME x) = x

option_REP_ABS_DEF

|- (!a. option_ABS (option_REP a) = a) /\
   !r. (\x. T) r = (option_REP (option_ABS r) = r)

option_TY_DEF

|- ?rep. TYPE_DEFINITION (\x. T) rep

SOME_DEF

|- !x. SOME x = option_ABS (INL x)

THE_DEF

|- !x. THE (SOME x) = x

Theorems

NOT_NONE_SOME

|- !x. ~(NONE = SOME x)

NOT_SOME_NONE

|- !x. ~(SOME x = NONE)

option_APPLY_EQ_SOME

|- !f x y. (option_APPLY f x = SOME y) = ?z. (x = SOME z) /\ (y = f z)

option_Axiom

|- !e f. ?fn. (!x. fn (SOME x) = f x) /\ (fn NONE = e)

option_case_compute

|- option_case e f x = (if IS_SOME x then f (THE x) else e)

option_case_cong

|- !f' f u' u M' M.
     (M = M') /\ ((M' = NONE) ==> (u = u')) /\
     (!x. (M' = SOME x) ==> (f x = f' x)) ==>
     (option_case u f M = option_case u' f' M')

option_CLAUSES

|- (!x y. (SOME x = SOME y) = (x = y)) /\ (!x. THE (SOME x) = x) /\
   (!x. ~(NONE = SOME x)) /\ (!x. ~(SOME x = NONE)) /\
   (!x. IS_SOME (SOME x) = T) /\ (IS_SOME NONE = F) /\
   (!x. IS_NONE x = (x = NONE)) /\ (!x. ~IS_SOME x = (x = NONE)) /\
   (!x. IS_SOME x ==> (SOME (THE x) = x)) /\
   (!x. option_case NONE SOME x = x) /\ (!x. option_case x SOME x = x) /\
   (!x. IS_NONE x ==> (option_case e f x = e)) /\
   (!x. IS_SOME x ==> (option_case e f x = f (THE x))) /\
   (!x. IS_SOME x ==> (option_case e SOME x = x)) /\
   (!u f. option_case u f NONE = u) /\
   (!u f x. option_case u f (SOME x) = f x) /\
   (!f x. option_APPLY f (SOME x) = SOME (f x)) /\
   !f. option_APPLY f NONE = NONE

option_induction

|- !P. P NONE /\ (!a. P (SOME a)) ==> !x. P x

option_JOIN_EQ_SOME

|- !x y. (option_JOIN x = SOME y) = (x = SOME (SOME y))

option_nchotomy

|- !opt. (opt = NONE) \/ ?x. opt = SOME x

SOME_11

|- !x y. (SOME x = SOME y) = (x = y)