Package cl: Combinatory logic example illustrating inductive definitions in HOL4

Information

namecl
version0.5
description Combinatory logic example illustrating inductive definitions in HOL4
authorRamana Kumar <ramana.kumar@gmail.com>
licenseMIT
requiresbase
showData.Bool
cl

Files

Defined Type Operator

Defined Constants

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

cl_size S = Number.Numeral.zero cl_size K = Number.Numeral.zero
  a0 a1.
    cl_size (# a0 a1) =
    Number.Natural.+ (Number.Numeral.bit1 Number.Numeral.zero)
      (Number.Natural.+ (cl_size a0) (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. cl_case v v1 f S = v) (v v1 f. cl_case v v1 f K = v1)
  v v1 f a0 a1. 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 a0a0
                  λ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)
    cl_case v v1 f M = 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

Input Constants

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)