Theory "ind_type"

Parents option numeral

Signature

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

Definitions

NUMPAIR

|- !x y. ind_type$NUMPAIR x y = 2 ** x * (2 * y + 1)

NUMPAIR_DEST

|- !x y.
     (NUMFST (ind_type$NUMPAIR x y) = x) /\
     (NUMSND (ind_type$NUMPAIR x y) = y)

NUMSUM

|- !b x. ind_type$NUMSUM b x = (if b then SUC (2 * x) else 2 * x)

NUMSUM_DEST

|- !x y.
     (NUMLEFT (ind_type$NUMSUM x y) = x) /\
     (NUMRIGHT (ind_type$NUMSUM x y) = y)

INJN

|- !m. ind_type$INJN m = (\n a. n = m)

INJA

|- !a. ind_type$INJA a = (\n b. b = a)

INJF

|- !f. ind_type$INJF f = (\n. f (NUMFST n) (NUMSND n))

INJP

|- !f1 f2.
     ind_type$INJP f1 f2 =
     (\n a. (if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a))

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

ZRECSPACE

|- 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)

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)

BOTTOM

|- ind_type$BOTTOM = mk_rec ind_type$ZBOT

CONSTR

|- !c i r.
     ind_type$CONSTR c i r =
     mk_rec (ind_type$ZCONSTR c i (\n. dest_rec (r n)))

FCONS

|- (!a f. FCONS a f 0 = a) /\ !a f n. FCONS a f (SUC n) = f n

FNIL

|- !n. ind_type$FNIL n = @x. T

ISO

|- !f g. ind_type$ISO f g = (!x. f (g x) = x) /\ !y. g (f y) = y

Theorems

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)

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)

NUMSUM_INJ

|- !b1 x1 b2 x2.
     (ind_type$NUMSUM b1 x1 = ind_type$NUMSUM b2 x2) = (b1 = b2) /\ (x1 = x2)

INJN_INJ

|- !n1 n2. (ind_type$INJN n1 = ind_type$INJN n2) = (n1 = n2)

INJA_INJ

|- !a1 a2. (ind_type$INJA a1 = ind_type$INJA a2) = (a1 = a2)

INJF_INJ

|- !f1 f2. (ind_type$INJF f1 = ind_type$INJF f2) = (f1 = f2)

INJP_INJ

|- !f1 f1' f2 f2'.
     (ind_type$INJP f1 f2 = ind_type$INJP f1' f2') = (f1 = f1') /\ (f2 = f2')

ZCONSTR_ZBOT

|- !c i r. ~(ind_type$ZCONSTR c i r = ind_type$ZBOT)

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)

MK_REC_INJ

|- !x y. (mk_rec x = mk_rec y) ==> ZRECSPACE x /\ ZRECSPACE y ==> (x = y)

DEST_REC_INJ

|- !x y. (dest_rec x = dest_rec y) = (x = y)

CONSTR_BOT

|- !c i r. ~(ind_type$CONSTR c i r = ind_type$BOTTOM)

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_REC

|- !Fn. ?f. !c i r. f (ind_type$CONSTR c i r) = Fn c i r (\n. f (r n))

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)))

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)