Theory: num

Parents

• bool

Type constants

• num(Arity = 0)

Term constants

• SUC_REP:ind -> ind {fixity = Prefix}
• ZERO_REP:ind {fixity = Prefix}
• IS_NUM_REP:ind -> bool {fixity = Prefix}
• REP_num:num -> ind {fixity = Prefix}
• ABS_num:ind -> num {fixity = Prefix}
• 0:num {fixity = Prefix}
• SUC:num -> num {fixity = Prefix}

Axioms

Definitions

SUC_REP_DEF

|- SUC_REP = (@f. ONE_ONE f /\ ~(ONTO f))

ZERO_REP_DEF

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

IS_NUM_REP

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

num_TY_DEF

|- ?rep. TYPE_DEFINITION IS_NUM_REP rep

num_ISO_DEF

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

ZERO_DEF

|- 0 = ABS_num ZERO_REP

SUC_DEF

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

Theorems

NOT_SUC

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

INV_SUC

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

INDUCTION

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