Theory: num

Parents

• bool

Types

• num(Arity = 0)

Constants

• 0  :num
• ZERO_REP  :ind
• SUC_REP  :ind -> ind
• REP_num  :num -> ind
• ABS_num  :ind -> num
• SUC  :num -> num
• IS_NUM_REP  :ind -> bool

Definitions

IS_NUM_REP

|- !m. IS_NUM_REP m = !P. P ZERO_REP /\ (!n. P n ==> P (SUC_REP n)) ==> P m

num_ISO_DEF

|- (!a. ABS_num (REP_num a) = a) /\
   !r. IS_NUM_REP r = (REP_num (ABS_num r) = r)

num_TY_DEF

|- ?rep. TYPE_DEFINITION IS_NUM_REP rep

SUC_DEF

|- !m. SUC m = ABS_num (SUC_REP (REP_num m))

SUC_REP_DEF

|- ONE_ONE SUC_REP /\ ~ONTO SUC_REP

ZERO_DEF

|- 0 = ABS_num ZERO_REP

ZERO_REP_DEF

|- !y. ~(ZERO_REP = SUC_REP y)

Theorems

INDUCTION

|- !P. P 0 /\ (!n. P n ==> P (SUC n)) ==> !n. P n

INV_SUC

|- !m n. (SUC m = SUC n) ==> (m = n)

NOT_SUC

|- !n. ~(SUC n = 0)