# let th = prove(`?x. x < 7`,EXISTS_TAC `0` THEN ARITH_TAC);;
val th : thm = |- ?x. x < 7
# let tybij = new_type_definition "7" ("mk_7","dest_7") th;;
val tybij : thm =
|- (!a. mk_7 (dest_7 a) = a) /\ (!r. r < 7 <=> dest_7 (mk_7 r) = r)
and here is a declaration of a type of finite sets over a base type,
a unary type constructor:
# let th = MESON[FINITE_RULES] `?s:A->bool. FINITE s`;;
0..0..solved at 2
CPU time (user): 0.
val th : thm = |- ?s. FINITE s
# let tybij = new_type_definition "finiteset" ("mk_fin","dest_fin") th;;
val tybij : thm =
|- (!a. mk_fin (dest_fin a) = a) /\
(!r. FINITE r <=> dest_fin (mk_fin r) = r)
so now types like