Theory "ind_type"

Parents while numeral

Signature

Type	Arity
recspace	1
Constant	Type
BOTTOM	:α recspace
CONSTR	:num -> α -> (num -> α recspace) -> α recspace
FCONS	:α -> (num -> α) -> num -> α
FNIL	:num -> α
INJA	:α -> num -> α -> bool
INJF	:(num -> num -> α -> bool) -> num -> α -> bool
INJN	:num -> num -> α -> bool
INJP	:(num -> α -> bool) -> (num -> α -> bool) -> num -> α -> bool
ISO	:(α -> β) -> (β -> α) -> bool
NUMFST	:num -> num
NUMLEFT	:num -> bool
NUMPAIR	:num -> num -> num
NUMRIGHT	:num -> num
NUMSND	:num -> num
NUMSUM	:bool -> num -> num
ZBOT	:num -> α -> bool
ZCONSTR	:num -> α -> (num -> num -> α -> bool) -> num -> α -> bool
ZRECSPACE	:(num -> α -> bool) -> bool
dest_rec	:α recspace -> num -> α -> bool
mk_rec	:(num -> α -> bool) -> α recspace

Definitions

ZRECSPACE_def

⊢ ZRECSPACE =
  (λa0.
       ∀ZRECSPACE'.
           (∀a0.
                (a0 = ind_type$ZBOT) ∨
                (∃c i r. (a0 = ind_type$ZCONSTR c i r) ∧ ∀n. ZRECSPACE' (r n)) ⇒
                ZRECSPACE' a0) ⇒
           ZRECSPACE' a0)

ZCONSTR

⊢ ∀c i r.
      ind_type$ZCONSTR c i r =
      ind_type$INJP (ind_type$INJN (SUC c))
        (ind_type$INJP (ind_type$INJA i) (ind_type$INJF r))

ZBOT

⊢ ind_type$ZBOT = ind_type$INJP (ind_type$INJN 0) (@z. T)

recspace_TY_DEF

⊢ ∃rep. TYPE_DEFINITION ZRECSPACE rep

recspace_repfns

⊢ (∀a. mk_rec (dest_rec a) = a) ∧ ∀r. ZRECSPACE r ⇔ (dest_rec (mk_rec r) = r)

NUMSUM_DEST

⊢ ∀x y.
      (NUMLEFT (ind_type$NUMSUM x y) ⇔ x) ∧
      (NUMRIGHT (ind_type$NUMSUM x y) = y)

NUMSUM

⊢ ∀b x. ind_type$NUMSUM b x = if b then SUC (2 * x) else 2 * x

NUMPAIR_DEST

⊢ ∀x y.
      (NUMFST (ind_type$NUMPAIR x y) = x) ∧
      (NUMSND (ind_type$NUMPAIR x y) = y)

NUMPAIR

⊢ ∀x y. ind_type$NUMPAIR x y = 2 ** x * (2 * y + 1)

ISO

⊢ ∀f g. ind_type$ISO f g ⇔ (∀x. f (g x) = x) ∧ ∀y. g (f y) = y

INJP

⊢ ∀f1 f2.
      ind_type$INJP f1 f2 =
      (λn a. if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a)

INJN

⊢ ∀m. ind_type$INJN m = (λn a. n = m)

INJF

⊢ ∀f. ind_type$INJF f = (λn. f (NUMFST n) (NUMSND n))

INJA

⊢ ∀a. ind_type$INJA a = (λn b. b = a)

FNIL

⊢ ∀n. ind_type$FNIL n = ARB

FCONS

⊢ (∀a f. ind_type$FCONS a f 0 = a) ∧ ∀a f n. ind_type$FCONS a f (SUC n) = f n

CONSTR

⊢ ∀c i r.
      ind_type$CONSTR c i r =
      mk_rec (ind_type$ZCONSTR c i (λn. dest_rec (r n)))

BOTTOM

⊢ ind_type$BOTTOM = mk_rec ind_type$ZBOT

Theorems

ZRECSPACE_strongind

⊢ ∀ZRECSPACE'.
      ZRECSPACE' ind_type$ZBOT ∧
      (∀c i r.
           (∀n. ZRECSPACE (r n) ∧ ZRECSPACE' (r n)) ⇒
           ZRECSPACE' (ind_type$ZCONSTR c i r)) ⇒
      ∀a0. ZRECSPACE a0 ⇒ ZRECSPACE' a0

ZRECSPACE_rules

⊢ ZRECSPACE ind_type$ZBOT ∧
  ∀c i r. (∀n. ZRECSPACE (r n)) ⇒ ZRECSPACE (ind_type$ZCONSTR c i r)

ZRECSPACE_ind

⊢ ∀ZRECSPACE'.
      ZRECSPACE' ind_type$ZBOT ∧
      (∀c i r. (∀n. ZRECSPACE' (r n)) ⇒ ZRECSPACE' (ind_type$ZCONSTR c i r)) ⇒
      ∀a0. ZRECSPACE a0 ⇒ ZRECSPACE' a0

ZRECSPACE_cases

⊢ ∀a0.
      ZRECSPACE a0 ⇔
      (a0 = ind_type$ZBOT) ∨
      ∃c i r. (a0 = ind_type$ZCONSTR c i r) ∧ ∀n. ZRECSPACE (r n)

ZCONSTR_ZBOT

⊢ ∀c i r. ind_type$ZCONSTR c i r ≠ ind_type$ZBOT

NUMSUM_INJ

⊢ ∀b1 x1 b2 x2.
      (ind_type$NUMSUM b1 x1 = ind_type$NUMSUM b2 x2) ⇔ (b1 ⇔ b2) ∧ (x1 = x2)

NUMPAIR_INJ_LEMMA

⊢ ∀x1 y1 x2 y2. (ind_type$NUMPAIR x1 y1 = ind_type$NUMPAIR x2 y2) ⇒ (x1 = x2)

NUMPAIR_INJ

⊢ ∀x1 y1 x2 y2.
      (ind_type$NUMPAIR x1 y1 = ind_type$NUMPAIR x2 y2) ⇔
      (x1 = x2) ∧ (y1 = y2)

MK_REC_INJ

⊢ ∀x y. (mk_rec x = mk_rec y) ⇒ ZRECSPACE x ∧ ZRECSPACE y ⇒ (x = y)

ISO_USAGE

⊢ ind_type$ISO f g ⇒
  (∀P. (∀x. P x) ⇔ ∀x. P (g x)) ∧ (∀P. (∃x. P x) ⇔ ∃x. P (g x)) ∧
  ∀a b. (a = g b) ⇔ (f a = b)

ISO_REFL

⊢ ind_type$ISO (λx. x) (λx. x)

ISO_FUN

⊢ ind_type$ISO f f' ∧ ind_type$ISO g g' ⇒
  ind_type$ISO (λh a'. g (h (f' a'))) (λh a. g' (h (f a)))

INJP_INJ

⊢ ∀f1 f1' f2 f2'.
      (ind_type$INJP f1 f2 = ind_type$INJP f1' f2') ⇔ (f1 = f1') ∧ (f2 = f2')

INJN_INJ

⊢ ∀n1 n2. (ind_type$INJN n1 = ind_type$INJN n2) ⇔ (n1 = n2)

INJF_INJ

⊢ ∀f1 f2. (ind_type$INJF f1 = ind_type$INJF f2) ⇔ (f1 = f2)

INJA_INJ

⊢ ∀a1 a2. (ind_type$INJA a1 = ind_type$INJA a2) ⇔ (a1 = a2)

INJ_INVERSE2

⊢ ∀P.
      (∀x1 y1 x2 y2. (P x1 y1 = P x2 y2) ⇔ (x1 = x2) ∧ (y1 = y2)) ⇒
      ∃X Y. ∀x y. (X (P x y) = x) ∧ (Y (P x y) = y)

FCONS_DEST

⊢ ind_type$FCONS a f n = if n = 0 then a else f (n − 1)

DEST_REC_INJ

⊢ ∀x y. (dest_rec x = dest_rec y) ⇔ (x = y)

CONSTR_REC

⊢ ∀Fn. ∃f. ∀c i r. f (ind_type$CONSTR c i r) = Fn c i r (λn. f (r n))

CONSTR_INJ

⊢ ∀c1 i1 r1 c2 i2 r2.
      (ind_type$CONSTR c1 i1 r1 = ind_type$CONSTR c2 i2 r2) ⇔
      (c1 = c2) ∧ (i1 = i2) ∧ (r1 = r2)

CONSTR_IND

⊢ ∀P.
      P ind_type$BOTTOM ∧ (∀c i r. (∀n. P (r n)) ⇒ P (ind_type$CONSTR c i r)) ⇒
      ∀x. P x

CONSTR_BOT

⊢ ∀c i r. ind_type$CONSTR c i r ≠ ind_type$BOTTOM