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 o INL = f) ∧ (h o 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 o f) (INR o 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)