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_MCOMP_def

⊢ ∀g f m. OPTION_MCOMP g f m = OPTION_BIND (f m) g

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 ∘ 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

IS_SOME_MAP

⊢ IS_SOME (OPTION_MAP f x) ⇔ IS_SOME x

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_MAP_CASE

⊢ OPTION_MAP f x = option_CASE x NONE (SOME ∘ f)

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)

IS_SOME_BIND

⊢ IS_SOME (OPTION_BIND x g) ⇒ IS_SOME x

OPTION_IGNORE_BIND_thm

⊢ OPTION_IGNORE_BIND NONE m = NONE ∧ OPTION_IGNORE_BIND (SOME v) m = m

OPTION_IGNORE_BIND_EQUALS_OPTION

⊢ (OPTION_IGNORE_BIND m1 m2 = NONE ⇔ m1 = NONE ∨ m2 = NONE) ∧
  (OPTION_IGNORE_BIND m1 m2 = SOME y ⇔ ∃x. m1 = SOME x ∧ m2 = SOME y)

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_CHOICE_NONE

⊢ OPTION_CHOICE m1 NONE = m1

OPTION_MCOMP_ASSOC

⊢ OPTION_MCOMP f (OPTION_MCOMP g h) = OPTION_MCOMP (OPTION_MCOMP f g) h

OPTION_MCOMP_ID

⊢ OPTION_MCOMP g SOME = g ∧ OPTION_MCOMP SOME f = f

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')

option_case_eq

⊢ option_CASE opt nc sc = v ⇔
  opt = NONE ∧ nc = v ∨ ∃x. opt = SOME x ∧ sc x = v

option_Induct

⊢ ∀P. (∀a. P (SOME a)) ∧ P NONE ⇒ ∀x. P x

option_CASES

⊢ ∀opt. (∃x. opt = SOME x) ∨ opt = NONE

datatype_option

⊢ DATATYPE (option NONE SOME)