Theory "combin"

Parents marker

Signature

Constant	Type
:>	:β -> (β -> α) -> α
ASSOC	:(α -> α -> α) -> bool
C	:(α -> β -> γ) -> β -> α -> γ
COMM	:(α -> α -> β) -> bool
FAIL	:α -> β -> α
FCOMM	:(α -> β -> α) -> (γ -> α -> α) -> bool
I	:α -> α
K	:α -> β -> α
LEFT_ID	:(α -> β -> β) -> α -> bool
MONOID	:(α -> α -> α) -> α -> bool
RIGHT_ID	:(α -> β -> α) -> β -> bool
S	:(α -> β -> γ) -> (α -> β) -> α -> γ
UPDATE	:α -> β -> (α -> β) -> α -> β
W	:(α -> α -> β) -> α -> β
o	:(γ -> β) -> (α -> γ) -> α -> β

Definitions

W_DEF

⊢ W = (λf x. f x x)

UPDATE_def

⊢ ∀a b. a =+ b = (λf c. if a = c then b else f c)

S_DEF

⊢ S = (λf g x. f x (g x))

RIGHT_ID_DEF

⊢ ∀f e. RIGHT_ID f e ⇔ ∀x. f x e = x

o_DEF

⊢ ∀f g. f ∘ g = (λx. f (g x))

MONOID_DEF

⊢ ∀f e. MONOID f e ⇔ ASSOC f ∧ RIGHT_ID f e ∧ LEFT_ID f e

LEFT_ID_DEF

⊢ ∀f e. LEFT_ID f e ⇔ ∀x. f e x = x

K_DEF

⊢ K = (λx y. x)

I_DEF

⊢ I = S K K

FCOMM_DEF

⊢ ∀f g. FCOMM f g ⇔ ∀x y z. g x (f y z) = f (g x y) z

FAIL_DEF

⊢ FAIL = (λx y. x)

COMM_DEF

⊢ ∀f. COMM f ⇔ ∀x y. f x y = f y x

C_DEF

⊢ combin$C = (λf x y. f y x)

ASSOC_DEF

⊢ ∀f. ASSOC f ⇔ ∀x y z. f x (f y z) = f (f x y) z

APP_DEF

⊢ ∀x f. x :> f = f x

Theorems

W_THM

⊢ ∀f x. W f x = f x x

UPDATE_EQ

⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ c⦈

UPDATE_COMMUTES

⊢ ∀f a b c d. a ≠ b ⇒ (f⦇a ↦ c; b ↦ d⦈ = f⦇b ↦ d; a ↦ c⦈)

UPDATE_APPLY_IMP_ID

⊢ ∀f b a. (f a = b) ⇒ (f⦇a ↦ b⦈ = f)

UPDATE_APPLY_ID

⊢ ∀f a b. (f a = b) ⇔ (f⦇a ↦ b⦈ = f)

UPDATE_APPLY

⊢ (∀a x f. f⦇a ↦ x⦈ a = x) ∧ ∀a b x f. a ≠ b ⇒ (f⦇a ↦ x⦈ b = f b)

UPD_SAME_KEY_UNWIND

⊢ ∀f1 f2 a b c. (f1⦇a ↦ b⦈ = f2⦇a ↦ c⦈) ⇒ (b = c) ∧ ∀v. f1⦇a ↦ v⦈ = f2⦇a ↦ v⦈

UPD11_SAME_KEY_AND_BASE

⊢ ∀f a b c. (f⦇a ↦ b⦈ = f⦇a ↦ c⦈) ⇔ (b = c)

UPD11_SAME_BASE

⊢ ∀f a b c d.
      (f⦇a ↦ c⦈ = f⦇b ↦ d⦈) ⇔
      (a = b) ∧ (c = d) ∨ a ≠ b ∧ (f⦇a ↦ c⦈ = f) ∧ (f⦇b ↦ d⦈ = f)

SAME_KEY_UPDATE_DIFFER

⊢ ∀f1 f2 a b c. b ≠ c ⇒ f⦇a ↦ b⦈ ≠ f⦇a ↦ c⦈

S_THM

⊢ ∀f g x. S f g x = f x (g x)

S_ABS_R

⊢ S f (λx. g x) = (λx. f x (g x))

S_ABS_L

⊢ S (λx. f x) g = (λx. f x (g x))

o_THM

⊢ ∀f g x. (f ∘ g) x = f (g x)

o_ASSOC

⊢ ∀f g h. f ∘ g ∘ h = (f ∘ g) ∘ h

o_ABS_R

⊢ f ∘ (λx. g x) = (λx. f (g x))

o_ABS_L

⊢ (λx. f x) ∘ g = (λx. f (g x))

MONOID_DISJ_F

⊢ MONOID $\/ F

MONOID_CONJ_T

⊢ MONOID $/\ T

literal_case_FORALL_ELIM

⊢ literal_case f v ⇔ $! (S ($==> ∘ Abbrev ∘ combin$C $= v) f)

LET_FORALL_ELIM

⊢ LET f v ⇔ $! (S ($==> ∘ Abbrev ∘ combin$C $= v) f)

K_THM

⊢ ∀x y. K x y = x

K_o_THM

⊢ (∀f v. K v ∘ f = K v) ∧ ∀f v. f ∘ K v = K (f v)

I_THM

⊢ ∀x. I x = x

I_o_ID

⊢ ∀f. (I ∘ f = f) ∧ (f ∘ I = f)

GEN_literal_case_RATOR

⊢ literal_case f v x = literal_case (combin$C f x) v

GEN_literal_case_RAND

⊢ P (literal_case f v) = literal_case (P ∘ f) v

GEN_LET_RATOR

⊢ LET f v x = LET (combin$C f x) v

GEN_LET_RAND

⊢ P (LET f v) = LET (P ∘ f) v

FCOMM_ASSOC

⊢ ∀f. FCOMM f f ⇔ ASSOC f

FAIL_THM

⊢ FAIL x y = x

C_THM

⊢ ∀f x y. combin$C f x y = f y x

C_ABS_L

⊢ combin$C (λx. f x) y = (λx. f x y)

ASSOC_SYM

⊢ ∀f. ASSOC f ⇔ ∀x y z. f (f x y) z = f x (f y z)

ASSOC_DISJ

⊢ ASSOC $\/

ASSOC_CONJ

⊢ ASSOC $/\

APPLY_UPDATE_THM

⊢ ∀f a b c. f⦇a ↦ b⦈ c = if a = c then b else f c

APPLY_UPDATE_ID

⊢ ∀f a. f⦇a ↦ f a⦈ = f