Package cl: Combinatory logic example illustrating inductive definitions in HOL4

Information

Files

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

Defined Type Operator

• combinatoryLogicExample
  • cl

Defined Constants

• combinatoryLogicExample
  • #
  • -->
  • -||->
  • confluent
  • diamond
  • normform
  • RTC

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
• Number
  • Natural
    • Number.Natural.natural

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∨
    • ~
    • select
    • F
    • T
• Function
  • Function.id
• HOL4
  • HOL4.TYPE_DEFINITION
  • Datatype
    • HOL4.Datatype.CONSTR
    • HOL4.Datatype.FCONS
• Number
  • Natural
    • Number.Natural.suc
  • Numeral
    • Number.Numeral.zero

Assumptions

⊦ T

⊦ ∀t. F ⇒ t

⊦ ¬¬p ⇒ p

⊦ ∀x. Function.id x = x

⊦ (~) = λt. t ⇒ F

⊦ (∃) = λP. P ((select) P)

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

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

⊦ (∀) = λP. P = λx. T

⊦ ¬(p ⇒ q) ⇒ p

⊦ ∀x. x = x ⇔ T

⊦ ∀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 q. p ∧ q ⇔ p

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀A B. A ∨ B ⇔ B ∨ A

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

⊦ (∧) = λp q. (λf. f p q) = λf. f T T

⊦ ∀P. ¬(∀x. P x) ⇔ ∃y. ¬P y

⊦ ∀P. ¬(∃x. P x) ⇔ ∀y. ¬P y

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ ∀f g. f = g ⇔ ∀x. f x = g x

⊦ ∀P a. (∃x. x = a ∧ P x) ⇔ P a

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

⊦ (∨) = λt1 t2. ∀t. (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t

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

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

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

⊦ ∀P Q. (∀z. P ⇒ Q z) ⇔ P ⇒ ∀x. Q x

⊦ ∀P Q. (∀y. P ∨ Q y) ⇔ P ∨ ∀x. Q x

⊦ ∀P Q. (∃y. P ∧ Q y) ⇔ P ∧ ∃x. Q x

⊦ ∀P Q. P ∧ (∀x. Q x) ⇔ ∀y. P ∧ Q y

⊦ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃y. P ∨ Q y

⊦ ∀P Q. (∃y. P y ∧ Q) ⇔ (∃x. P x) ∧ Q

⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀y. P y ∧ Q

⊦ ∀P Q. (∃x. P x) ∨ Q ⇔ ∃x. P x ∨ Q

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

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

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

⊦ ∀t1 t2 t3. t1 ∧ t2 ∧ t3 ⇔ (t1 ∧ t2) ∧ t3

⊦ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3

⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C

⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x)

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

⊦ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)

⊦ ∀P Q. (∀x. P x ∧ Q x) ⇔ (∀x. P x) ∧ ∀x. Q x

⊦ ∀P Q. (∃z. P z ∨ Q z) ⇔ (∃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)

⊦ ∀A B. (¬(A ∧ B) ⇔ ¬A ∨ ¬B) ∧ (¬(A ∨ B) ⇔ ¬A ∧ ¬B)

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

⊦ ∀t. ((T ⇔ t) ⇔ t) ∧ ((t ⇔ T) ⇔ t) ∧ ((F ⇔ t) ⇔ ¬t) ∧ ((t ⇔ F) ⇔ ¬t)

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

⊦ ∀t. (T ∧ t ⇔ t) ∧ (t ∧ T ⇔ t) ∧ (F ∧ t ⇔ F) ∧ (t ∧ F ⇔ F) ∧ (t ∧ t ⇔ t)

⊦ ∀t. (T ∨ t ⇔ T) ∧ (t ∨ T ⇔ T) ∧ (F ∨ t ⇔ t) ∧ (t ∨ F ⇔ t) ∧ (t ∨ t ⇔ t)

⊦ ∀t. (T ⇒ t ⇔ t) ∧ (t ⇒ T ⇔ T) ∧ (F ⇒ t ⇔ T) ∧ (t ⇒ t ⇔ T) ∧ (t ⇒ F ⇔ ¬t)

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