- OPTION_MAP_I
-
|- OPTION_MAP I = I
- OPTION_REL_def
-
|- (OPTREL R NONE NONE ⇔ T) ∧ (OPTREL R (SOME x) NONE ⇔ F) ∧
(OPTREL R NONE (SOME y) ⇔ F) ∧ (OPTREL R (SOME x) (SOME y) ⇔ R x y)
- OPTION_REL_EQ
-
|- OPTREL $= = $=
- OPTION_EQUIV
-
|- ∀R. EQUIV R ⇒ EQUIV (OPTREL R)
- OPTION_QUOTIENT
-
|- ∀R abs rep.
QUOTIENT R abs rep ⇒
QUOTIENT (OPTREL 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 ⇒ OPTREL 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 ⇒ OPTREL 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. OPTREL 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. OPTREL 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 ∧ OPTREL R1 a1 a2 ⇒
OPTREL R2 (OPTION_MAP f1 a1) (OPTION_MAP f2 a2)