Package cl: Combinatory logic example illustrating inductive definitions in HOL4

Information

name	cl
version	0.3
description	Combinatory logic example illustrating inductive definitions in HOL4
author	Ramana Kumar <ramana.kumar@gmail.com>
license	MIT
show	Data.Bool combinatoryLogicExample

Files

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

Defined Type Operator

combinatoryLogicExample
- cl

Defined Constants

combinatoryLogicExample
- #
- -->
- -||->
- confluent
- diamond
- normform
- K
- RTC
- S
- ind_type
  - ind_type.cl_case
  - ind_type.cl_size

Theorems

⊦ confluent -->

⊦ diamond -||->

⊦ HOL4.DATATYPE (cl S K #)

⊦ 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. normform R x ⇔ ∀y. ¬R x y

⊦ ∀x. x = S ∨ x = K ∨ ∃c c0. x = # c c0

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

⊦ ∀a0 a1 a0' a1'. # a0 a1 = # a0' a1' ⇔ a0 = a0' ∧ a1 = a1'

⊦ ∀R a0 a1. RTC R a0 a1 ⇔ a1 = a0 ∨ ∃y. R a0 y ∧ RTC R y a1

⊦ ¬(S = K) ∧ (∀a1 a0. ¬(S = # a0 a1)) ∧ ∀a1 a0. ¬(K = # a0 a1)

⊦ ∀P. P S ∧ P K ∧ (∀a0 a1. P a0 ∧ P a1 ⇒ P (# a0 a1)) ⇒ ∀u. P u

⊦ ∀R. diamond R ⇔ ∀x y z. R x y ∧ R x z ⇒ ∃u. R y u ∧ R z u

⊦ ∀R. (∀x. RTC R x x) ∧ ∀x y z. 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

⊦ ind_type.cl_size S = Number.Numeral.zero ∧
  ind_type.cl_size K = Number.Numeral.zero ∧
  ∀a0 a1.
    ind_type.cl_size (# a0 a1) =
    Number.Natural.+ (Number.Numeral.bit1 Number.Numeral.zero)
      (Number.Natural.+ (ind_type.cl_size a0) (ind_type.cl_size a1))

⊦ ∀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

⊦ RTC =
  λR a0 a1.
    ∀RTC'.
      (∀a0 a1. a1 = a0 ∨ (∃y. R a0 y ∧ RTC' y a1) ⇒ RTC' a0 a1) ⇒
      RTC' a0 a1

⊦ ∀R.
confluent R ⇔ ∀x y z. RTC R x y ∧ RTC R x z ⇒ ∃u. RTC R y 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

⊦ ∀f0 f1 f2.
    ∃fn.
      fn S = f0 ∧ fn K = f1 ∧
      ∀a0 a1. fn (# a0 a1) = f2 a0 a1 (fn a0) (fn a1)

⊦ ∀R RTC'.
(∀x. RTC' x x) ∧ (∀x y z. R x y ∧ RTC' y z ⇒ RTC' x z) ⇒
∀x y. RTC R x y ⇒ RTC' x y

⊦ ∀R RTC'.
(∀x. RTC' x x) ∧ (∀x y z. R x y ∧ RTC R y z ∧ RTC' y z ⇒ RTC' x z) ⇒
∀x y. RTC R x y ⇒ RTC' x y

⊦ (∀v v1 f. ind_type.cl_case v v1 f S = v) ∧
(∀v v1 f. ind_type.cl_case v v1 f K = v1) ∧
∀v v1 f a0 a1. ind_type.cl_case v v1 f (# a0 a1) = f a0 a1

⊦ ∃rep.
    HOL4.TYPE_DEFINITION
      (λa0'.
         ∀'cl'.
           (∀a0'.
              a0' =
              HOL4.Datatype.CONSTR Number.Numeral.zero arb
                (λn. HOL4.Datatype.BOTTOM) ∨
              a0' =
              HOL4.Datatype.CONSTR (Number.Natural.suc Number.Numeral.zero)
                arb (λn. HOL4.Datatype.BOTTOM) ∨
              (∃a0 a1.
                 a0' =
                 (let a0 ← a0 ∈
                  λa1.
                    HOL4.Datatype.CONSTR
                      (Number.Natural.suc
                         (Number.Natural.suc Number.Numeral.zero)) arb
                      (HOL4.Datatype.FCONS a0
                         (HOL4.Datatype.FCONS a1
                            (λn. HOL4.Datatype.BOTTOM)))) a1 ∧ 'cl' a0 ∧
                 'cl' a1) ⇒ 'cl' a0') ⇒ 'cl' a0') rep

⊦ ∀M M' v v1 f.
    M = M' ∧ (M' = S ⇒ v = v') ∧ (M' = K ⇒ v1 = v1') ∧
    (∀a0 a1. M' = # a0 a1 ⇒ f a0 a1 = f' a0 a1) ⇒
    ind_type.cl_case v v1 f M = ind_type.cl_case v' v1' f' M'

⊦ (∀x. -||-> x x) ∧
  (∀x y u v. -||-> x y ∧ -||-> u v ⇒ -||-> (# x u) (# y v)) ∧
  (∀x y. -||-> (# (# K x) y) x) ∧
  ∀f g x. -||-> (# (# (# S f) g) x) (# (# f x) (# g x))

⊦ (∀x y f. --> x y ⇒ --> (# f x) (# f y)) ∧
(∀f g x. --> f g ⇒ --> (# f x) (# g x)) ∧ (∀x y. --> (# (# K x) y) x) ∧
∀f g x. --> (# (# (# S f) g) x) (# (# f x) (# g x))

⊦ ∀a0 a1.
    -||-> a0 a1 ⇔
    a1 = a0 ∨ (∃x y u v. a0 = # x u ∧ a1 = # y v ∧ -||-> x y ∧ -||-> u v) ∨
    (∃y. a0 = # (# K a1) y) ∨
    ∃f g x. a0 = # (# (# S f) g) x ∧ a1 = # (# f x) (# g x)

⊦ ∀-||->'.
    (∀x. -||->' x x) ∧
    (∀x y u v. -||->' x y ∧ -||->' u v ⇒ -||->' (# x u) (# y v)) ∧
    (∀x y. -||->' (# (# K x) y) x) ∧
    (∀f g x. -||->' (# (# (# S f) g) x) (# (# f x) (# g x))) ⇒
    ∀x y. -||-> x y ⇒ -||->' x y

⊦ ∀-->'.
    (∀x y f. -->' x y ⇒ -->' (# f x) (# f y)) ∧
    (∀f g x. -->' f g ⇒ -->' (# f x) (# g x)) ∧
    (∀x y. -->' (# (# K x) y) x) ∧
    (∀f g x. -->' (# (# (# S f) g) x) (# (# f x) (# g x))) ⇒
    ∀a0 a1. --> a0 a1 ⇒ -->' a0 a1

⊦ ∀-||->'.
    (∀x. -||->' x x) ∧
    (∀x y u v.
       -||-> x y ∧ -||->' x y ∧ -||-> u v ∧ -||->' u v ⇒
       -||->' (# x u) (# y v)) ∧ (∀x y. -||->' (# (# K x) y) x) ∧
    (∀f g x. -||->' (# (# (# S f) g) x) (# (# f x) (# g x))) ⇒
    ∀x y. -||-> x y ⇒ -||->' x y

⊦ -||-> =
  λa0 a1.
    ∀-||->'.
      (∀a0 a1.
         a1 = a0 ∨
         (∃x y u v. a0 = # x u ∧ a1 = # y v ∧ -||->' x y ∧ -||->' u v) ∨
         (∃y. a0 = # (# K a1) y) ∨
         (∃f g x. a0 = # (# (# S f) g) x ∧ a1 = # (# f x) (# g x)) ⇒
         -||->' a0 a1) ⇒ -||->' a0 a1

⊦ ∀a0 a1.
    --> a0 a1 ⇔
    (∃x y f. a0 = # f x ∧ a1 = # f y ∧ --> x y) ∨
    (∃f g x. a0 = # f x ∧ a1 = # g x ∧ --> f g) ∨ (∃y. a0 = # (# K a1) y) ∨
    ∃f g x. a0 = # (# (# S f) g) x ∧ a1 = # (# f x) (# g x)

⊦ ∀-->'.
    (∀x y f. --> x y ∧ -->' x y ⇒ -->' (# f x) (# f y)) ∧
    (∀f g x. --> f g ∧ -->' f g ⇒ -->' (# f x) (# g x)) ∧
    (∀x y. -->' (# (# K x) y) x) ∧
    (∀f g x. -->' (# (# (# S f) g) x) (# (# f x) (# g x))) ⇒
    ∀a0 a1. --> a0 a1 ⇒ -->' a0 a1

⊦ --> =
  λa0 a1.
    ∀-->'.
      (∀a0 a1.
         (∃x y f. a0 = # f x ∧ a1 = # f y ∧ -->' x y) ∨
         (∃f g x. a0 = # f x ∧ a1 = # g x ∧ -->' f g) ∨
         (∃y. a0 = # (# K a1) y) ∨
         (∃f g x. a0 = # (# (# S f) g) x ∧ a1 = # (# f x) (# g x)) ⇒
         -->' a0 a1) ⇒ -->' a0 a1

Input Type Operators

→
bool
HOL4
- Datatype
  - HOL4.Datatype.recspace
Number
- Natural
  - Number.Natural.natural

Input Constants

=
Data
- Bool
  - ∀
  - ∧
  - ⇒
  - ∃
  - ∨
  - ~
  - arb
  - select
  - F
  - T
Function
- Function.id
HOL4
- HOL4.DATATYPE
- HOL4.TYPE_DEFINITION
- Datatype
  - HOL4.Datatype.BOTTOM
  - HOL4.Datatype.CONSTR
  - HOL4.Datatype.FCONS
Number
- Natural
  - Number.Natural.+
  - Number.Natural.suc
- Numeral
  - Number.Numeral.bit1
  - Number.Numeral.zero

Assumptions

⊦ T

⊦ ∀t. F ⇒ t

⊦ ¬¬p ⇒ p

⊦ ∀x. Function.id x = x

⊦ ∀x. HOL4.DATATYPE x ⇔ T

⊦ (~) = λ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) ⇔ ∃x. ¬P x

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

⊦ (∃) = λ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. (∀u. P ∨ Q u) ⇔ P ∨ ∀x. Q x

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

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

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

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

⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ 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. (∀u. P u ∧ Q u) ⇔ (∀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)