Package cl: Combinatory logic example illustrating inductive definitions in HOL4

Information

Files

• Package tarball cl-0.2.tgz
• Theory file cl.thy (included in the package tarball)

Defined Type Operators

• combinatoryLogicExample
  • cl
• Number
  • Natural
    • Number.Natural.natural

Defined Constants

• combinatoryLogicExample
  • #
  • -->
  • -||->
  • confluent
  • diamond
  • normform
  • RTC
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ~
    • F
• Number
  • Natural
    • Number.Natural.suc
  • Numeral
    • Number.Numeral.zero

Axioms

⊦ ∀t. F ⇒ t

⊦ ¬¬p ⇒ p

⊦ ∀t. (λx. t x) = t

⊦ ¬(p ⇒ q) ⇒ p

⊦ ∀t. ¬¬t ⇔ t

⊦ ¬(p ⇒ q) ⇒ ¬q

⊦ ¬(p ∨ q) ⇒ ¬p

⊦ ¬(p ∨ q) ⇒ ¬q

⊦ ∀A. A ⇒ ¬A ⇒ F

⊦ ∀t. ¬t ⇒ t ⇒ F

⊦ ∀t. (t ⇒ F) ⇒ ¬t

⊦ ∀P x. P x ⇒ P ((select) P)

⊦ (¬A ⇒ F) ⇒ (A ⇒ F) ⇒ F

⊦ ∀P t. (∀x. x = t ⇒ P x) ⇒ (∃) P

⊦ ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)

⊦ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)

⊦ ¬(¬A ∨ B) ⇒ F ⇔ A ⇒ ¬B ⇒ F

⊦ ¬(A ∨ B) ⇒ F ⇔ (A ⇒ F) ⇒ ¬B ⇒ F

⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∧ z ⇒ y ∧ w

⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∨ z ⇒ y ∨ w

⊦ (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x

⊦ ∀Fn. ∃f. ∀c i r. f (HOL4.Datatype.CONSTR c i r) = Fn c i r (λn. f (r n))

⊦ (p ⇔ q ⇒ r) ⇔ (p ∨ q) ∧ (p ∨ ¬r) ∧ (¬q ∨ r ∨ ¬p)

⊦ (p ⇔ q ∨ r) ⇔ (p ∨ ¬q) ∧ (p ∨ ¬r) ∧ (q ∨ r ∨ ¬p)

⊦ (∀a f. HOL4.Datatype.FCONS a f Number.Numeral.zero = a) ∧
  ∀a f n. HOL4.Datatype.FCONS a f (Number.Natural.suc n) = f n

⊦ ∀x x' y y'. (x ⇔ x') ∧ (x' ⇒ (y ⇔ y')) ⇒ (x ⇒ y ⇔ x' ⇒ y')

⊦ (p ⇔ q ∧ r) ⇔ (p ∨ ¬q ∨ ¬r) ∧ (q ∨ ¬p) ∧ (r ∨ ¬p)

⊦ HOL4.TYPE_DEFINITION =
  λP rep.
    (∀x' x''. rep x' = rep x'' ⇒ x' = x'') ∧ ∀x. P x ⇔ ∃x'. x = rep x'

⊦ ∀P.
    (∃rep. HOL4.TYPE_DEFINITION P rep) ⇒
    ∃rep abs. (∀a. abs (rep a) = a) ∧ ∀r. P r ⇔ rep (abs r) = r

⊦ (p ⇔ q ⇔ r) ⇔ (p ∨ q ∨ r) ∧ (p ∨ ¬r ∨ ¬q) ∧ (q ∨ ¬r ∨ ¬p) ∧ (r ∨ ¬q ∨ ¬p)

Theorems

⊦ confluent -->

⊦ diamond -||->

⊦ RTC -||-> = RTC -->

⊦ ∀R. confluent R ⇔ diamond (RTC R)

⊦ ∀R. diamond R ⇒ diamond (RTC R)

⊦ ∀x y. -||-> x y ⇒ RTC --> x y

⊦ ∀x y. RTC --> x y ⇒ RTC -||-> x y

⊦ ∀x y. RTC -||-> x y ⇒ RTC --> x y

⊦ ∀R x y z. RTC R x y ∧ RTC R y z ⇒ RTC R x z

⊦ ∀R1 R2. (∀x y. R1 x y ⇒ R2 x y) ⇒ ∀x y. RTC R1 x y ⇒ RTC R2 x y

⊦ ∀x y. RTC --> x y ⇒ ∀z. RTC --> (# x z) (# y z) ∧ RTC --> (# z x) (# z y)

⊦ ∀R. diamond R ⇒ ∀x p. RTC R x p ⇒ ∀z. R x z ⇒ ∃u. RTC R p u ∧ RTC R z u

⊦ ∀R.
    confluent R ⇒
    ∀x y z. RTC R x y ∧ normform R y ∧ RTC R x z ∧ normform R z ⇒ y = z

Input Type Operators

• →
• bool
• HOL4
  • Datatype
    • HOL4.Datatype.recspace

Input Constants

• =
• Data
  • Bool
    • select
• HOL4
  • HOL4.TYPE_DEFINITION
  • Datatype
    • HOL4.Datatype.CONSTR
    • HOL4.Datatype.FCONS