Theory "sum"

Parents sat combin

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_CASE	:α + β -> (α -> γ) -> (β -> γ) -> γ

Definitions

IS_SUM_REP

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

sum_TY_DEF

⊢ ∃rep. TYPE_DEFINITION IS_SUM_REP rep

sum_ISO_DEF

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

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)

OUTL

⊢ ∀x. OUTL (INL x) = x

OUTR

⊢ ∀x. OUTR (INR x) = x

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

SUM_MAP_def

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

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

Theorems

INL_11

⊢ INL x = INL y ⇔ x = y

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

sum_axiom

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

sum_INDUCT

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

FORALL_SUM

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

EXISTS_SUM

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

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_distinct

⊢ ∀x y. INL x ≠ INR y

sum_distinct1

⊢ ∀x y. INR y ≠ INL x

ISL_OR_ISR

⊢ ∀x. ISL x ∨ ISR x

INL

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

INR

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

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_MAP

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

SUM_MAP_CASE

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

SUM_MAP_I

⊢ I ++ I = I

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

NOT_ISL_ISR

⊢ ∀x. ¬ISL x ⇔ ISR x

NOT_ISR_ISL

⊢ ∀x. ¬ISR x ⇔ ISL x

SUM_ALL_MONO

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

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

datatype_sum

⊢ DATATYPE (sum INL INR)