- BOTTOM
-
|- BOTTOM = mk_rec ZBOT
- CONSTR
-
|- !c i r. CONSTR c i r = mk_rec (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. FNIL n = @x. T
- INJA
-
|- !a. INJA a = (\n b. b = a)
- INJF
-
|- !f. INJF f = (\n. f (NUMFST n) (NUMSND n))
- INJN
-
|- !m. INJN m = (\n a. n = m)
- INJP
-
|- !f1 f2.
INJP f1 f2 =
(\n a. (if NUMLEFT n then f1 (NUMRIGHT n) a else f2 (NUMRIGHT n) a))
- ISO
-
|- !f g. ISO f g = (!x. f (g x) = x) /\ !y. g (f y) = y
- NUMPAIR
-
|- !x y. NUMPAIR x y = 2 ** x * (2 * y + 1)
- NUMPAIR_DEST
-
|- !x y. (NUMFST (NUMPAIR x y) = x) /\ (NUMSND (NUMPAIR x y) = y)
- NUMSUM
-
|- !b x. NUMSUM b x = (if b then SUC (2 * x) else 2 * x)
- NUMSUM_DEST
-
|- !x y. (NUMLEFT (NUMSUM x y) = x) /\ (NUMRIGHT (NUMSUM x y) = y)
- recspace_repfns
-
|- (!a. mk_rec (dest_rec a) = a) /\
!r. ZRECSPACE r = (dest_rec (mk_rec r) = r)
- recspace_TY_DEF
-
|- ?rep. TYPE_DEFINITION ZRECSPACE rep
- ZBOT
-
|- ZBOT = INJP (INJN 0) @z. T
- ZCONSTR
-
|- !c i r. ZCONSTR c i r = INJP (INJN (SUC c)) (INJP (INJA i) (INJF r))
- ZRECSPACE
-
|- ZRECSPACE =
(\a0.
!ZRECSPACE'.
(!a0.
(a0 = ZBOT) \/
(?c i r. (a0 = ZCONSTR c i r) /\ !n. ZRECSPACE' (r n)) ==>
ZRECSPACE' a0) ==>
ZRECSPACE' a0)
- CONSTR_BOT
-
|- !c i r. ~(CONSTR c i r = BOTTOM)
- CONSTR_IND
-
|- !P. P BOTTOM /\ (!c i r. (!n. P (r n)) ==> P (CONSTR c i r)) ==> !x. P x
- CONSTR_INJ
-
|- !c1 i1 r1 c2 i2 r2.
(CONSTR c1 i1 r1 = CONSTR c2 i2 r2) = (c1 = c2) /\ (i1 = i2) /\ (r1 = r2)
- CONSTR_REC
-
|- !Fn. ?f. !c i r. f (CONSTR c i r) = Fn c i r (\n. f (r n))
- DEST_REC_INJ
-
|- !x y. (dest_rec x = dest_rec y) = (x = y)
- 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)
- INJA_INJ
-
|- !a1 a2. (INJA a1 = INJA a2) = (a1 = a2)
- INJF_INJ
-
|- !f1 f2. (INJF f1 = INJF f2) = (f1 = f2)
- INJN_INJ
-
|- !n1 n2. (INJN n1 = INJN n2) = (n1 = n2)
- INJP_INJ
-
|- !f1 f1' f2 f2'. (INJP f1 f2 = INJP f1' f2') = (f1 = f1') /\ (f2 = f2')
- ISO_FUN
-
|- ISO f f' /\ ISO g g' ==> ISO (\h a'. g (h (f' a'))) (\h a. g' (h (f a)))
- ISO_REFL
-
|- ISO (\x. x) (\x. x)
- ISO_USAGE
-
|- 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)
- MK_REC_INJ
-
|- !x y. (mk_rec x = mk_rec y) ==> ZRECSPACE x /\ ZRECSPACE y ==> (x = y)
- NUMPAIR_INJ
-
|- !x1 y1 x2 y2. (NUMPAIR x1 y1 = NUMPAIR x2 y2) = (x1 = x2) /\ (y1 = y2)
- NUMPAIR_INJ_LEMMA
-
|- !x1 y1 x2 y2. (NUMPAIR x1 y1 = NUMPAIR x2 y2) ==> (x1 = x2)
- NUMSUM_INJ
-
|- !b1 x1 b2 x2. (NUMSUM b1 x1 = NUMSUM b2 x2) = (b1 = b2) /\ (x1 = x2)
- ZCONSTR_ZBOT
-
|- !c i r. ~(ZCONSTR c i r = ZBOT)