Theory "option"

Signature

Definitions

option_TY_DEF

|- ∃rep. TYPE_DEFINITION (λx. T) rep

option_REP_ABS_DEF

|- (∀a. option_ABS (option_REP a) = a) ∧
   ∀r. (λx. T) r ⇔ (option_REP (option_ABS r) = r)

SOME_DEF

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

NONE_DEF

|- NONE = option_ABS (INR ())

option_case_def

|- (∀v f. option_CASE NONE v f = v) ∧ ∀x v f. option_CASE (SOME x) v f = f x

OPTION_MAP_DEF

|- (∀f x. OPTION_MAP f (SOME x) = SOME (f x)) ∧ ∀f. OPTION_MAP f NONE = NONE

IS_SOME_DEF

|- (∀x. IS_SOME (SOME x) ⇔ T) ∧ (IS_SOME NONE ⇔ F)

IS_NONE_DEF

|- (∀x. IS_NONE (SOME x) ⇔ F) ∧ (IS_NONE NONE ⇔ T)

THE_DEF

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

OPTION_MAP2_DEF

|- ∀f x y.
     OPTION_MAP2 f x y =
     if IS_SOME x ∧ IS_SOME y then SOME (f (THE x) (THE y)) else NONE

OPTION_JOIN_DEF

|- (OPTION_JOIN NONE = NONE) ∧ ∀x. OPTION_JOIN (SOME x) = x

OPTION_BIND_def

|- (∀f. OPTION_BIND NONE f = NONE) ∧ ∀x f. OPTION_BIND (SOME x) f = f x

OPTION_IGNORE_BIND_def

|- ∀m1 m2. OPTION_IGNORE_BIND m1 m2 = OPTION_BIND m1 (K m2)

OPTION_GUARD_def

|- (OPTION_GUARD T = SOME ()) ∧ (OPTION_GUARD F = NONE)

OPTION_CHOICE_def

|- (∀m2. OPTION_CHOICE NONE m2 = m2) ∧
   ∀x m2. OPTION_CHOICE (SOME x) m2 = SOME x

OPTION_APPLY_def

|- (∀x. NONE <*> x = NONE) ∧ ∀f x. SOME f <*> x = OPTION_MAP f x

OPTREL_def

|- ∀R x y.
     OPTREL R x y ⇔
     (x = NONE) ∧ (y = NONE) ∨ ∃x0 y0. (x = SOME x0) ∧ (y = SOME y0) ∧ R x0 y0

some_def

|- ∀P. $some P = if ∃x. P x then SOME (@x. P x) else NONE

OPTION_ALL_def

|- (∀P. OPTION_ALL P NONE ⇔ T) ∧ ∀P x. OPTION_ALL P (SOME x) ⇔ P x

Theorems

option_Axiom

|- ∀e f. ∃fn. (fn NONE = e) ∧ ∀x. fn (SOME x) = f x

option_induction

|- ∀P. P NONE ∧ (∀a. P (SOME a)) ⇒ ∀x. P x

option_nchotomy

|- ∀opt. (opt = NONE) ∨ ∃x. opt = SOME x

FORALL_OPTION

|- (∀opt. P opt) ⇔ P NONE ∧ ∀x. P (SOME x)

EXISTS_OPTION

|- (∃opt. P opt) ⇔ P NONE ∨ ∃x. P (SOME x)

SOME_11

|- ∀x y. (SOME x = SOME y) ⇔ (x = y)

NOT_NONE_SOME

|- ∀x. NONE ≠ SOME x

NOT_SOME_NONE

|- ∀x. SOME x ≠ NONE

OPTION_MAP2_THM

|- (OPTION_MAP2 f (SOME x) (SOME y) = SOME (f x y)) ∧
   (OPTION_MAP2 f (SOME x) NONE = NONE) ∧
   (OPTION_MAP2 f NONE (SOME y) = NONE) ∧ (OPTION_MAP2 f NONE NONE = NONE)

IS_SOME_EXISTS

|- ∀opt. IS_SOME opt ⇔ ∃x. opt = SOME x

IS_NONE_EQ_NONE

|- ∀x. IS_NONE x ⇔ (x = NONE)

NOT_IS_SOME_EQ_NONE

|- ∀x. ¬IS_SOME x ⇔ (x = NONE)

option_case_ID

|- ∀x. option_CASE x NONE SOME = x

option_case_SOME_ID

|- ∀x. option_CASE x x SOME = x

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 x NONE SOME = x) ∧ (∀x. option_CASE x x SOME = x) ∧
   (∀x. IS_NONE x ⇒ (option_CASE x e f = e)) ∧
   (∀x. IS_SOME x ⇒ (option_CASE x e f = f (THE x))) ∧
   (∀x. IS_SOME x ⇒ (option_CASE x e SOME = x)) ∧
   (∀v f. option_CASE NONE v f = v) ∧
   (∀x v f. option_CASE (SOME x) v f = f x) ∧
   (∀f x. OPTION_MAP f (SOME x) = SOME (f x)) ∧
   (∀f. OPTION_MAP f NONE = NONE) ∧ (OPTION_JOIN NONE = NONE) ∧
   ∀x. OPTION_JOIN (SOME x) = x

option_case_compute

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

IF_EQUALS_OPTION

|- (((if P then SOME x else NONE) = NONE) ⇔ ¬P) ∧
   (((if P then NONE else SOME x) = NONE) ⇔ P) ∧
   (((if P then SOME x else NONE) = SOME y) ⇔ P ∧ (x = y)) ∧
   (((if P then NONE else SOME x) = SOME y) ⇔ ¬P ∧ (x = y))

IF_NONE_EQUALS_OPTION

|- (((if P then X else NONE) = NONE) ⇔ P ⇒ IS_NONE X) ∧
   (((if P then NONE else X) = NONE) ⇔ IS_SOME X ⇒ P) ∧
   (((if P then X else NONE) = SOME x) ⇔ P ∧ (X = SOME x)) ∧
   (((if P then NONE else X) = SOME x) ⇔ ¬P ∧ (X = SOME x))

OPTION_MAP_EQ_SOME

|- ∀f x y. (OPTION_MAP f x = SOME y) ⇔ ∃z. (x = SOME z) ∧ (y = f z)

OPTION_MAP_EQ_NONE

|- ∀f x. (OPTION_MAP f x = NONE) ⇔ (x = NONE)

OPTION_MAP_EQ_NONE_both_ways

|- ((OPTION_MAP f x = NONE) ⇔ (x = NONE)) ∧
   ((NONE = OPTION_MAP f x) ⇔ (x = NONE))

OPTION_MAP_COMPOSE

|- OPTION_MAP f (OPTION_MAP g x) = OPTION_MAP (f o g) x

OPTION_MAP_CONG

|- ∀opt1 opt2 f1 f2.
     (opt1 = opt2) ∧ (∀x. (opt2 = SOME x) ⇒ (f1 x = f2 x)) ⇒
     (OPTION_MAP f1 opt1 = OPTION_MAP f2 opt2)

OPTION_JOIN_EQ_SOME

|- ∀x y. (OPTION_JOIN x = SOME y) ⇔ (x = SOME (SOME y))

OPTION_MAP2_SOME

|- (OPTION_MAP2 f o1 o2 = SOME v) ⇔
   ∃x1 x2. (o1 = SOME x1) ∧ (o2 = SOME x2) ∧ (v = f x1 x2)

OPTION_MAP2_NONE

|- (OPTION_MAP2 f o1 o2 = NONE) ⇔ (o1 = NONE) ∨ (o2 = NONE)

OPTION_MAP2_cong

|- ∀x1 x2 y1 y2 f1 f2.
     (x1 = x2) ∧ (y1 = y2) ∧
     (∀x y. (x2 = SOME x) ∧ (y2 = SOME y) ⇒ (f1 x y = f2 x y)) ⇒
     (OPTION_MAP2 f1 x1 y1 = OPTION_MAP2 f2 x2 y2)

OPTION_BIND_cong

|- ∀o1 o2 f1 f2.
     (o1 = o2) ∧ (∀x. (o2 = SOME x) ⇒ (f1 x = f2 x)) ⇒
     (OPTION_BIND o1 f1 = OPTION_BIND o2 f2)

OPTION_BIND_EQUALS_OPTION

|- ((OPTION_BIND p f = NONE) ⇔ (p = NONE) ∨ ∃x. (p = SOME x) ∧ (f x = NONE)) ∧
   ((OPTION_BIND p f = SOME y) ⇔ ∃x. (p = SOME x) ∧ (f x = SOME y))

OPTION_IGNORE_BIND_thm

|- (OPTION_IGNORE_BIND NONE m = NONE) ∧ (OPTION_IGNORE_BIND (SOME v) m = m)

OPTION_GUARD_COND

|- OPTION_GUARD b = if b then SOME () else NONE

OPTION_GUARD_EQ_THM

|- ((OPTION_GUARD b = SOME ()) ⇔ b) ∧ ((OPTION_GUARD b = NONE) ⇔ ¬b)

OPTION_CHOICE_EQ_NONE

|- (OPTION_CHOICE m1 m2 = NONE) ⇔ (m1 = NONE) ∧ (m2 = NONE)

OPTION_APPLY_MAP2

|- OPTION_MAP f x <*> y = OPTION_MAP2 f x y

SOME_SOME_APPLY

|- SOME f <*> SOME x = SOME (f x)

SOME_APPLY_PERMUTE

|- f <*> SOME x = SOME (λf. f x) <*> f

OPTION_APPLY_o

|- SOME $o <*> f <*> g <*> x = f <*> (g <*> x)

OPTREL_MONO

|- (∀x y. P x y ⇒ Q x y) ⇒ OPTREL P x y ⇒ OPTREL Q x y

OPTREL_refl

|- (∀x. R x x) ⇒ ∀x. OPTREL R x x

some_intro

|- (∀x. P x ⇒ Q (SOME x)) ∧ ((∀x. ¬P x) ⇒ Q NONE) ⇒ Q ($some P)

some_elim

|- Q ($some P) ⇒ (∃x. P x ∧ Q (SOME x)) ∨ (∀x. ¬P x) ∧ Q NONE

some_F

|- (some x. F) = NONE

some_EQ

|- ((some x. x = y) = SOME y) ∧ ((some x. y = x) = SOME y)

option_case_cong

|- ∀M M' v f.
     (M = M') ∧ ((M' = NONE) ⇒ (v = v')) ∧
     (∀x. (M' = SOME x) ⇒ (f x = f' x)) ⇒
     (option_CASE M v f = option_CASE M' v' f')

OPTION_ALL_MONO

|- (∀x. P x ⇒ P' x) ⇒ OPTION_ALL P opt ⇒ OPTION_ALL P' opt

OPTION_ALL_CONG

|- ∀opt opt' P P'.
     (opt = opt') ∧ (∀x. (opt' = SOME x) ⇒ (P x ⇔ P' x)) ⇒
     (OPTION_ALL P opt ⇔ OPTION_ALL P' opt')

datatype_option

|- DATATYPE (option NONE SOME)