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

K_DEF

⊢ K = (λx y. x)

S_DEF

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

I_DEF

⊢ I = S K K

C_DEF

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

W_DEF

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

o_DEF

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

APP_DEF

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

UPDATE_def

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

ASSOC_DEF

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

COMM_DEF

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

FCOMM_DEF

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

RIGHT_ID_DEF

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

LEFT_ID_DEF

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

MONOID_DEF

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

FAIL_DEF

⊢ FAIL = (λx y. x)

Theorems

o_THM

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

o_ASSOC

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

o_ABS_L

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

o_ABS_R

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

K_THM

⊢ ∀x y. K x y = x

S_THM

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

S_ABS_L

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

S_ABS_R

⊢ S f (λx. g x) = (λx. f x (g 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)

W_THM

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

I_THM

⊢ ∀x. I x = x

I_o_ID

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

K_o_THM

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

UPDATE_APPLY

⊢ (∀a x f. (a =+ x) f a = x) ∧ ∀a b x f. a ≠ b ⇒ (a =+ x) f b = f b

APPLY_UPDATE_THM

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

UPDATE_COMMUTES

⊢ ∀f a b c d. a ≠ b ⇒ (a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f)

UPDATE_EQ

⊢ ∀f a b c. (a =+ c) ((a =+ b) f) = (a =+ c) f

UPDATE_APPLY_ID

⊢ ∀f a b. f a = b ⇔ (a =+ b) f = f

UPDATE_APPLY_IMP_ID

⊢ ∀f b a. f a = b ⇒ (a =+ b) f = f

APPLY_UPDATE_ID

⊢ ∀f a. (a =+ f a) f = f

UPD11_SAME_BASE

⊢ ∀f a b c d.
      (a =+ c) f = (b =+ d) f ⇔
      a = b ∧ c = d ∨ a ≠ b ∧ (a =+ c) f = f ∧ (b =+ d) f = f

SAME_KEY_UPDATE_DIFFER

⊢ ∀f1 f2 a b c. b ≠ c ⇒ (a =+ b) f ≠ (a =+ c) f

UPD11_SAME_KEY_AND_BASE

⊢ ∀f a b c. (a =+ b) f = (a =+ c) f ⇔ b = c

UPD_SAME_KEY_UNWIND

⊢ ∀f1 f2 a b c.
      (a =+ b) f1 = (a =+ c) f2 ⇒ b = c ∧ ∀v. (a =+ v) f1 = (a =+ v) f2

GEN_LET_RAND

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

GEN_LET_RATOR

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

LET_FORALL_ELIM

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

GEN_literal_case_RAND

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

GEN_literal_case_RATOR

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

literal_case_FORALL_ELIM

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

ASSOC_CONJ

⊢ ASSOC $/\

ASSOC_SYM

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

ASSOC_DISJ

⊢ ASSOC $\/

FCOMM_ASSOC

⊢ ∀f. FCOMM f f ⇔ ASSOC f

MONOID_CONJ_T

⊢ MONOID $/\ T

MONOID_DISJ_F

⊢ MONOID $\/ F

FAIL_THM

⊢ FAIL x y = x