Structure combinTheory

signature combinTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val C_DEF : thm
    val FAIL_DEF : thm
    val I_DEF : thm
    val K_DEF : thm
    val S_DEF : thm
    val W_DEF : thm
    val o_DEF : thm
  
  (*  Theorems  *)
    val C_ABS_L : thm
    val C_THM : thm
    val FAIL_THM : thm
    val GEN_LET_RAND : thm
    val GEN_LET_RATOR : thm
    val GEN_literal_case_RAND : thm
    val GEN_literal_case_RATOR : thm
    val I_THM : thm
    val I_o_ID : thm
    val K_THM : thm
    val K_o_THM : thm
    val LET_FORALL_ELIM : thm
    val S_ABS_L : thm
    val S_ABS_R : thm
    val S_THM : thm
    val W_THM : thm
    val literal_case_FORALL_ELIM : thm
    val o_ABS_R : thm
    val o_ASSOC : thm
    val o_THM : thm
  
  val combin_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [marker] Parent theory of "combin"
   
   [C_DEF]  Definition
      
      |- C = (\f x y. f y x)
   
   [FAIL_DEF]  Definition
      
      |- FAIL = (\x y. x)
   
   [I_DEF]  Definition
      
      |- I = S K K
   
   [K_DEF]  Definition
      
      |- K = (\x y. x)
   
   [S_DEF]  Definition
      
      |- S = (\f g x. f x (g x))
   
   [W_DEF]  Definition
      
      |- W = (\f x. f x x)
   
   [o_DEF]  Definition
      
      |- !f g. f o g = (\x. f (g x))
   
   [C_ABS_L]  Theorem
      
      |- C (\x. f x) y = (\x. f x y)
   
   [C_THM]  Theorem
      
      |- !f x y. C f x y = f y x
   
   [FAIL_THM]  Theorem
      
      |- FAIL x y = x
   
   [GEN_LET_RAND]  Theorem
      
      |- P (LET f v) = LET (P o f) v
   
   [GEN_LET_RATOR]  Theorem
      
      |- LET f v x = LET (C f x) v
   
   [GEN_literal_case_RAND]  Theorem
      
      |- P (literal_case f v) = literal_case (P o f) v
   
   [GEN_literal_case_RATOR]  Theorem
      
      |- literal_case f v x = literal_case (C f x) v
   
   [I_THM]  Theorem
      
      |- !x. I x = x
   
   [I_o_ID]  Theorem
      
      |- !f. (I o f = f) /\ (f o I = f)
   
   [K_THM]  Theorem
      
      |- !x y. K x y = x
   
   [K_o_THM]  Theorem
      
      |- (!f v. K v o f = K v) /\ !f v. f o K v = K (f v)
   
   [LET_FORALL_ELIM]  Theorem
      
      |- LET f v = $! (S ($==> o Abbrev o C $= v) f)
   
   [S_ABS_L]  Theorem
      
      |- S (\x. f x) g = (\x. f x (g x))
   
   [S_ABS_R]  Theorem
      
      |- S f (\x. g x) = (\x. f x (g x))
   
   [S_THM]  Theorem
      
      |- !f g x. S f g x = f x (g x)
   
   [W_THM]  Theorem
      
      |- !f x. W f x = f x x
   
   [literal_case_FORALL_ELIM]  Theorem
      
      |- literal_case f v = $! (S ($==> o Abbrev o C $= v) f)
   
   [o_ABS_R]  Theorem
      
      |- f o (\x. g x) = (\x. f (g x))
   
   [o_ASSOC]  Theorem
      
      |- !f g h. f o g o h = (f o g) o h
   
   [o_THM]  Theorem
      
      |- !f g x. (f o g) x = f (g x)
   
   
*)
end