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 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 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 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 I_THM : thm
val I_o_ID : 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 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_APPLY_ID : 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_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
⊢ combin$C = (λf x y. f y x)
[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
[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. (a =+ f a) f = f
[APPLY_UPDATE_THM] Theorem
⊢ ∀f a b c. (a =+ b) f 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
⊢ combin$C (λx. f x) y = (λx. f x y)
[C_THM] Theorem
⊢ ∀f x y. combin$C f x y = f y x
[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 (combin$C 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 (combin$C f x) v
[I_THM] Theorem
⊢ ∀x. I x = x
[I_o_ID] Theorem
⊢ ∀f. (I ∘ f = f) ∧ (f ∘ I = f)
[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 ∘ combin$C $= v) f)
[MONOID_CONJ_T] Theorem
⊢ MONOID $/\ T
[MONOID_DISJ_F] Theorem
⊢ MONOID $\/ F
[SAME_KEY_UPDATE_DIFFER] Theorem
⊢ ∀f1 f2 a b c. b ≠ c ⇒ (a =+ b) f ≠ (a =+ c) 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)
[UPD11_SAME_BASE] Theorem
⊢ ∀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)
[UPD11_SAME_KEY_AND_BASE] Theorem
⊢ ∀f a b c. ((a =+ b) f = (a =+ c) f) ⇔ (b = c)
[UPDATE_APPLY] Theorem
⊢ (∀a x f. (a =+ x) f a = x) ∧ ∀a b x f. a ≠ b ⇒ ((a =+ x) f b = f b)
[UPDATE_APPLY_ID] Theorem
⊢ ∀f a b. (f a = b) ⇔ ((a =+ b) f = f)
[UPDATE_APPLY_IMP_ID] Theorem
⊢ ∀f b a. (f a = b) ⇒ ((a =+ b) f = f)
[UPDATE_COMMUTES] Theorem
⊢ ∀f a b c d. a ≠ b ⇒ ((a =+ c) ((b =+ d) f) = (b =+ d) ((a =+ c) f))
[UPDATE_EQ] Theorem
⊢ ∀f a b c. (a =+ c) ((a =+ b) f) = (a =+ c) f
[UPD_SAME_KEY_UNWIND] Theorem
⊢ ∀f1 f2 a b c.
((a =+ b) f1 = (a =+ c) f2) ⇒
(b = c) ∧ ∀v. (a =+ v) f1 = (a =+ v) f2
[W_THM] Theorem
⊢ ∀f x. W f x = f x x
[literal_case_FORALL_ELIM] Theorem
⊢ literal_case f v ⇔ $! (S ($==> ∘ Abbrev ∘ combin$C $= 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_THM] Theorem
⊢ ∀f g x. (f ∘ g) x = f (g x)
*)
end
HOL 4, Kananaskis-11