Structure combinTheory

signature combinTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val APP_DEF : thm
    val ASSOC_DEF : thm
    val COMM_DEF : thm
    val C_DEF : thm
    val EXTENSIONAL_def : thm
    val FAIL_DEF : thm
    val FCOMM_DEF : thm
    val I_DEF : thm
    val K_DEF : thm
    val LEFT_ID_DEF : thm
    val MONOID_DEF : thm
    val RESTRICTION : thm
    val RIGHT_ID_DEF : thm
    val S_DEF : thm
    val UPDATE_def : thm
    val W_DEF : thm
    val o_DEF : thm
  
  (*  Theorems  *)
    val APPLY_UPDATE_ID : thm
    val APPLY_UPDATE_THM : thm
    val ASSOC_CONJ : thm
    val ASSOC_DISJ : thm
    val ASSOC_SYM : thm
    val C_ABS_L : thm
    val C_THM : thm
    val EXTENSIONAL_RESTRICTION : thm
    val FAIL_THM : thm
    val FCOMM_ASSOC : thm
    val GEN_LET_RAND : thm
    val GEN_LET_RATOR : thm
    val GEN_literal_case_RAND : thm
    val GEN_literal_case_RATOR : thm
    val IN_EXTENSIONAL : thm
    val IN_EXTENSIONAL_UNDEFINED : thm
    val I_EQ_IDABS : thm
    val I_THM : thm
    val I_o_ID : thm
    val K_PARTIAL : thm
    val K_THM : thm
    val K_o_THM : thm
    val LET_FORALL_ELIM : thm
    val MONOID_CONJ_T : thm
    val MONOID_DISJ_F : thm
    val RESTRICTION_DEFINED : thm
    val RESTRICTION_EQ : thm
    val RESTRICTION_THM : thm
    val RESTRICTION_UNDEFINED : thm
    val SAME_KEY_UPDATE_DIFFER : thm
    val S_ABS_L : thm
    val S_ABS_R : thm
    val S_THM : thm
    val UPD11_SAME_BASE : thm
    val UPD11_SAME_KEY_AND_BASE : thm
    val UPDATE_APPLY : thm
    val UPDATE_APPLY1 : thm
    val UPDATE_APPLY_ID : thm
    val UPDATE_APPLY_ID_RWT : thm
    val UPDATE_APPLY_IMP_ID : thm
    val UPDATE_COMMUTES : thm
    val UPDATE_EQ : thm
    val UPD_SAME_KEY_UNWIND : thm
    val W_THM : thm
    val literal_case_FORALL_ELIM : thm
    val o_ABS_L : thm
    val o_ABS_R : thm
    val o_ASSOC : thm
    val o_ASSOC' : thm
    val o_CONG : thm
    val o_THM : thm
  
  val combin_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [marker] Parent theory of "combin"
   
   [APP_DEF]  Definition
      
      ⊢ ∀x f. (x :> f) = f x
   
   [ASSOC_DEF]  Definition
      
      ⊢ ∀f. ASSOC f ⇔ ∀x y z. f x (f y z) = f (f x y) z
   
   [COMM_DEF]  Definition
      
      ⊢ ∀f. COMM f ⇔ ∀x y. f x y = f y x
   
   [C_DEF]  Definition
      
      ⊢ flip = (λf x y. f y x)
   
   [EXTENSIONAL_def]  Definition
      
      ⊢ ∀s f. EXTENSIONAL s f ⇔ ∀x. x ∉ s ⇒ f x = ARB
   
   [FAIL_DEF]  Definition
      
      ⊢ FAIL = (λx y. x)
   
   [FCOMM_DEF]  Definition
      
      ⊢ ∀f g. FCOMM f g ⇔ ∀x y z. g x (f y z) = f (g x y) z
   
   [I_DEF]  Definition
      
      ⊢ I = S K K
   
   [K_DEF]  Definition
      
      ⊢ K = (λx y. x)
   
   [LEFT_ID_DEF]  Definition
      
      ⊢ ∀f e. LEFT_ID f e ⇔ ∀x. f e x = x
   
   [MONOID_DEF]  Definition
      
      ⊢ ∀f e. MONOID f e ⇔ ASSOC f ∧ RIGHT_ID f e ∧ LEFT_ID f e
   
   [RESTRICTION]  Definition
      
      ⊢ ∀s f x. RESTRICTION s f x = if x ∈ s then f x else ARB
   
   [RIGHT_ID_DEF]  Definition
      
      ⊢ ∀f e. RIGHT_ID f e ⇔ ∀x. f x e = x
   
   [S_DEF]  Definition
      
      ⊢ S = (λf g x. f x (g x))
   
   [UPDATE_def]  Definition
      
      ⊢ ∀a b. (a =+ b) = (λf c. if a = c then b else f c)
   
   [W_DEF]  Definition
      
      ⊢ W = (λf x. f x x)
   
   [o_DEF]  Definition
      
      ⊢ ∀f g. f ∘ g = (λx. f (g x))
   
   [APPLY_UPDATE_ID]  Theorem
      
      ⊢ ∀f a. f⦇a ↦ f a⦈ = f
   
   [APPLY_UPDATE_THM]  Theorem
      
      ⊢ ∀f a b c. f⦇a ↦ b⦈ c = if a = c then b else f c
   
   [ASSOC_CONJ]  Theorem
      
      ⊢ ASSOC $/\
   
   [ASSOC_DISJ]  Theorem
      
      ⊢ ASSOC $\/
   
   [ASSOC_SYM]  Theorem
      
      ⊢ ∀f. ASSOC f ⇔ ∀x y z. f (f x y) z = f x (f y z)
   
   [C_ABS_L]  Theorem
      
      ⊢ flip (λx. f x) y = (λx. f x y)
   
   [C_THM]  Theorem
      
      ⊢ ∀f x y. flip f x y = f y x
   
   [EXTENSIONAL_RESTRICTION]  Theorem
      
      ⊢ ∀s f. EXTENSIONAL s (RESTRICTION s f)
   
   [FAIL_THM]  Theorem
      
      ⊢ FAIL x y = x
   
   [FCOMM_ASSOC]  Theorem
      
      ⊢ ∀f. FCOMM f f ⇔ ASSOC f
   
   [GEN_LET_RAND]  Theorem
      
      ⊢ P (LET f v) = LET (P ∘ f) v
   
   [GEN_LET_RATOR]  Theorem
      
      ⊢ LET f v x = LET (flip f x) v
   
   [GEN_literal_case_RAND]  Theorem
      
      ⊢ P (literal_case f v) = literal_case (P ∘ f) v
   
   [GEN_literal_case_RATOR]  Theorem
      
      ⊢ literal_case f v x = literal_case (flip f x) v
   
   [IN_EXTENSIONAL]  Theorem
      
      ⊢ ∀s f. f ∈ EXTENSIONAL s ⇔ ∀x. x ∉ s ⇒ f x = ARB
   
   [IN_EXTENSIONAL_UNDEFINED]  Theorem
      
      ⊢ ∀s f x. f ∈ EXTENSIONAL s ∧ x ∉ s ⇒ f x = ARB
   
   [I_EQ_IDABS]  Theorem
      
      ⊢ I = (λx. x)
   
   [I_THM]  Theorem
      
      ⊢ ∀x. I x = x
   
   [I_o_ID]  Theorem
      
      ⊢ ∀f. I ∘ f = f ∧ f ∘ I = f
   
   [K_PARTIAL]  Theorem
      
      ⊢ ∀x. K x = (λz. x)
   
   [K_THM]  Theorem
      
      ⊢ ∀x y. K x y = x
   
   [K_o_THM]  Theorem
      
      ⊢ (∀f v. K v ∘ f = K v) ∧ ∀f v. f ∘ K v = K (f v)
   
   [LET_FORALL_ELIM]  Theorem
      
      ⊢ LET f v ⇔ $! (S ($==> ∘ Abbrev ∘ flip $= v) f)
   
   [MONOID_CONJ_T]  Theorem
      
      ⊢ MONOID $/\ T
   
   [MONOID_DISJ_F]  Theorem
      
      ⊢ MONOID $\/ F
   
   [RESTRICTION_DEFINED]  Theorem
      
      ⊢ ∀s f x. x ∈ s ⇒ RESTRICTION s f x = f x
   
   [RESTRICTION_EQ]  Theorem
      
      ⊢ ∀s f x y. x ∈ s ∧ f x = y ⇒ RESTRICTION s f x = y
   
   [RESTRICTION_THM]  Theorem
      
      ⊢ ∀s f. RESTRICTION s f = (λx. if x ∈ s then f x else ARB)
   
   [RESTRICTION_UNDEFINED]  Theorem
      
      ⊢ ∀s f x. x ∉ s ⇒ RESTRICTION s f x = ARB
   
   [SAME_KEY_UPDATE_DIFFER]  Theorem
      
      ⊢ ∀f1 f2 a b c. b ≠ c ⇒ f⦇a ↦ b⦈ ≠ f⦇a ↦ c⦈
   
   [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)
   
   [UPD11_SAME_BASE]  Theorem
      
      ⊢ ∀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
   
   [UPD11_SAME_KEY_AND_BASE]  Theorem
      
      ⊢ ∀f a b c. f⦇a ↦ b⦈ = f⦇a ↦ c⦈ ⇔ b = c
   
   [UPDATE_APPLY]  Theorem
      
      ⊢ (∀a x f. f⦇a ↦ x⦈ a = x) ∧ ∀a b x f. a ≠ b ⇒ f⦇a ↦ x⦈ b = f b
   
   [UPDATE_APPLY1]  Theorem
      
      ⊢ ∀a x f. f⦇a ↦ x⦈ a = x
   
   [UPDATE_APPLY_ID]  Theorem
      
      ⊢ ∀f a b. f a = b ⇔ f⦇a ↦ b⦈ = f
   
   [UPDATE_APPLY_ID_RWT]  Theorem
      
      ⊢ (∀f a b. f⦇a ↦ b⦈ = f ⇔ f a = b) ∧ ∀f a b. f = f⦇a ↦ b⦈ ⇔ f a = b
   
   [UPDATE_APPLY_IMP_ID]  Theorem
      
      ⊢ ∀f b a. f a = b ⇒ f⦇a ↦ b⦈ = f
   
   [UPDATE_COMMUTES]  Theorem
      
      ⊢ ∀f a b c d. a ≠ b ⇒ f⦇a ↦ c; b ↦ d⦈ = f⦇b ↦ d; a ↦ c⦈
   
   [UPDATE_EQ]  Theorem
      
      ⊢ ∀f a b c. f⦇a ↦ c; a ↦ b⦈ = f⦇a ↦ c⦈
   
   [UPD_SAME_KEY_UNWIND]  Theorem
      
      ⊢ ∀f1 f2 a b c.
          f1⦇a ↦ b⦈ = f2⦇a ↦ c⦈ ⇒ b = c ∧ ∀v. f1⦇a ↦ v⦈ = f2⦇a ↦ v⦈
   
   [W_THM]  Theorem
      
      ⊢ ∀f x. W f x = f x x
   
   [literal_case_FORALL_ELIM]  Theorem
      
      ⊢ literal_case f v ⇔ $! (S ($==> ∘ Abbrev ∘ flip $= v) f)
   
   [o_ABS_L]  Theorem
      
      ⊢ (λx. f x) ∘ g = (λx. f (g x))
   
   [o_ABS_R]  Theorem
      
      ⊢ f ∘ (λx. g x) = (λx. f (g x))
   
   [o_ASSOC]  Theorem
      
      ⊢ ∀f g h. f ∘ g ∘ h = (f ∘ g) ∘ h
   
   [o_ASSOC']  Theorem
      
      ⊢ ∀f g h. (f ∘ g) ∘ h = f ∘ g ∘ h
   
   [o_CONG]  Theorem
      
      ⊢ ∀a1 a2 g1 g2 f1 f2.
          a1 = a2 ∧ (∀x. x = a2 ⇒ g1 x = g2 x) ∧
          (∀y. y = g2 a2 ⇒ f1 y = f2 y) ⇒
          (f1 ∘ g1) a1 = (f2 ∘ g2) a2
   
   [o_THM]  Theorem
      
      ⊢ ∀f g x. (f ∘ g) x = f (g x)
   
   
*)
end

HOL 4, Trindemossen-1