Theory "combin"

Parents     marker

Signature

Constant Type
o :('c -> 'b) -> ('a -> 'c) -> 'a -> 'b
W :('a -> 'a -> 'b) -> 'a -> 'b
S :('a -> 'b -> 'c) -> ('a -> 'b) -> 'a -> 'c
K :'a -> 'b -> 'a
I :'a -> 'a
FAIL :'a -> 'b -> 'a
C :('a -> 'b -> 'c) -> 'b -> 'a -> 'c

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 o g = (\x. f (g x))
FAIL_DEF 
|- FAIL = (\x y. x)

Theorems

o_THM 
|- !f g x. (f o g) x = f (g x)
o_ASSOC 
|- !f g h. f o g o h = (f o g) o h
o_ABS_R 
|- f o (\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 o f = f) /\ (f o I = f)
K_o_THM 
|- (!f v. K v o f = K v) /\ !f v. f o K v = K (f v)
GEN_LET_RAND 
|- P (LET f v) = LET (P o f) v
GEN_LET_RATOR 
|- LET f v x = LET (combin$C f x) v
LET_FORALL_ELIM 
|- LET f v = $! (S ($==> o Abbrev o combin$C $= v) f)
GEN_literal_case_RAND 
|- P (literal_case f v) = literal_case (P o 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 ($==> o Abbrev o combin$C $= v) f)
FAIL_THM 
|- FAIL x y = x