Theory "sum"

Parents pair

Signature

Type	Arity
sum	2
Constant	Type
ABS_sum	:(bool -> α -> β -> bool) -> α + β
INL	:α -> α + β
INR	:β -> α + β
ISL	:α + β -> bool
ISR	:α + β -> bool
IS_SUM_REP	:(bool -> α -> β -> bool) -> bool
OUTL	:α + β -> α
OUTR	:α + β -> β
REP_sum	:α + β -> bool -> α -> β -> bool
SUM_ALL	:(α -> bool) -> (β -> bool) -> α + β -> bool
SUM_MAP	:(α -> γ) -> (β -> δ) -> α + β -> γ + δ
sum_CASE	:α + β -> (α -> γ) -> (β -> γ) -> γ

Definitions

INL_DEF

⊢ ∀e. INL e = ABS_sum (λb x y. (x = e) ∧ b)

INR_DEF

⊢ ∀e. INR e = ABS_sum (λb x y. (y = e) ∧ ¬b)

ISL

⊢ (∀x. ISL (INL x)) ∧ ∀y. ¬ISL (INR y)

ISR

⊢ (∀x. ISR (INR x)) ∧ ∀y. ¬ISR (INL y)

IS_SUM_REP

⊢ ∀f. IS_SUM_REP f ⇔
      ∃v1 v2. (f = (λb x y. (x = v1) ∧ b)) ∨ (f = (λb x y. (y = v2) ∧ ¬b))

OUTL

⊢ ∀x. OUTL (INL x) = x

OUTR

⊢ ∀x. OUTR (INR x) = x

SUM_ALL_def

⊢ (∀P Q x. SUM_ALL P Q (INL x) ⇔ P x) ∧ ∀P Q y. SUM_ALL P Q (INR y) ⇔ Q y

SUM_MAP_def

⊢ (∀f g a. SUM_MAP f g (INL a) = INL (f a)) ∧
  ∀f g b. SUM_MAP f g (INR b) = INR (g b)

sum_ISO_DEF

⊢ (∀a. ABS_sum (REP_sum a) = a) ∧ ∀r. IS_SUM_REP r ⇔ (REP_sum (ABS_sum r) = r)

sum_TY_DEF

⊢ ∃rep. TYPE_DEFINITION IS_SUM_REP rep

sum_case_def

⊢ (∀x f f1. sum_CASE (INL x) f f1 = f x) ∧
  ∀y f f1. sum_CASE (INR y) f f1 = f1 y

Theorems

EXISTS_SUM

⊢ ∀P. (∃s. P s) ⇔ (∃x. P (INL x)) ∨ ∃y. P (INR y)

FORALL_SUM

⊢ (∀s. P s) ⇔ (∀x. P (INL x)) ∧ ∀y. P (INR y)

INL

⊢ ∀x. ISL x ⇒ (INL (OUTL x) = x)

INL_11

⊢ (INL x = INL y) ⇔ (x = y)

INR

⊢ ∀x. ISR x ⇒ (INR (OUTR x) = x)

INR_11

⊢ (INR x = INR y) ⇔ (x = y)

INR_INL_11

⊢ (∀y x. (INL x = INL y) ⇔ (x = y)) ∧ ∀y x. (INR x = INR y) ⇔ (x = y)

INR_neq_INL

⊢ ∀v1 v2. INR v2 ≠ INL v1

ISL_OR_ISR

⊢ ∀x. ISL x ∨ ISR x

NOT_ISL_ISR

⊢ ∀x. ¬ISL x ⇔ ISR x

NOT_ISR_ISL

⊢ ∀x. ¬ISR x ⇔ ISL x

SUM_ALL_CONG

⊢ ∀s s' P P' Q Q'.
    (s = s') ∧ (∀a. (s' = INL a) ⇒ (P a ⇔ P' a)) ∧
    (∀b. (s' = INR b) ⇒ (Q b ⇔ Q' b)) ⇒
    (SUM_ALL P Q s ⇔ SUM_ALL P' Q' s')

SUM_ALL_MONO

⊢ (∀x. P x ⇒ P' x) ∧ (∀y. Q y ⇒ Q' y) ⇒ SUM_ALL P Q s ⇒ SUM_ALL P' Q' s

SUM_MAP

⊢ ∀f g z. SUM_MAP f g z = if ISL z then INL (f (OUTL z)) else INR (g (OUTR z))

SUM_MAP_CASE

⊢ ∀f g z. SUM_MAP f g z = sum_CASE z (INL ∘ f) (INR ∘ g)

SUM_MAP_I

⊢ SUM_MAP I I = I

SUM_MAP_o

⊢ SUM_MAP f g ∘ SUM_MAP h k = SUM_MAP (f ∘ h) (g ∘ k)

cond_sum_expand

⊢ (∀x y z. ((if P then INR x else INL y) = INR z) ⇔ P ∧ (z = x)) ∧
  (∀x y z. ((if P then INR x else INL y) = INL z) ⇔ ¬P ∧ (z = y)) ∧
  (∀x y z. ((if P then INL x else INR y) = INL z) ⇔ P ∧ (z = x)) ∧
  ∀x y z. ((if P then INL x else INR y) = INR z) ⇔ ¬P ∧ (z = y)

datatype_sum

⊢ DATATYPE (sum INL INR)

sum_Axiom

⊢ ∀f g. ∃h. (∀x. h (INL x) = f x) ∧ ∀y. h (INR y) = g y

sum_CASES

⊢ ∀ss. (∃x. ss = INL x) ∨ ∃y. ss = INR y

sum_INDUCT

⊢ ∀P. (∀x. P (INL x)) ∧ (∀y. P (INR y)) ⇒ ∀s. P s

sum_axiom

⊢ ∀f g. ∃!h. (h ∘ INL = f) ∧ (h ∘ INR = g)

sum_case_cong

⊢ ∀M M' f f1.
    (M = M') ∧ (∀x. (M' = INL x) ⇒ (f x = f' x)) ∧
    (∀y. (M' = INR y) ⇒ (f1 y = f1' y)) ⇒
    (sum_CASE M f f1 = sum_CASE M' f' f1')

sum_distinct

⊢ ∀x y. INL x ≠ INR y

sum_distinct1

⊢ ∀x y. INR y ≠ INL x