Theory "quotient_option"

Theorems

SOME_RSP

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀x y. R x y ⇒ OPTREL R (SOME x) (SOME y)

SOME_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀x. SOME x = OPTION_MAP abs (SOME (rep x))

OPTION_REL_EQ

⊢ OPTREL $= = $=

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_QUOTIENT

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒
      QUOTIENT (OPTREL R) (OPTION_MAP abs) (OPTION_MAP rep)

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)

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_I

⊢ OPTION_MAP I = I

OPTION_EQUIV

⊢ ∀R. EQUIV R ⇒ EQUIV (OPTREL R)

NONE_RSP

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ OPTREL R NONE NONE

NONE_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ (NONE = OPTION_MAP abs NONE)

IS_SOME_RSP

⊢ ∀R abs rep.
      QUOTIENT R abs rep ⇒ ∀x y. OPTREL R x y ⇒ (IS_SOME x ⇔ IS_SOME y)

IS_SOME_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀x. IS_SOME x ⇔ IS_SOME (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)

IS_NONE_PRS

⊢ ∀R abs rep. QUOTIENT R abs rep ⇒ ∀x. IS_NONE x ⇔ IS_NONE (OPTION_MAP rep x)