[opentheory-users] Embedding Z (or other ZFC fragments) in HOL

[Freek Wiedijk]

Dear Roger Jones,

>On the more detailed suggestions, the only functions
>over types, /as such/, are type constructors, which cannot
>take numeric parameters.

Of course there is John Harrison's trick of using a type
as if it were a number, which he uses to define finite
dimensional vectors:

let dimindex = new_definition
  `dimindex(s:A->bool) = if FINITE(:A) then CARD(:A) else 1`;;

let finite_image_tybij =
  new_type_definition "finite_image" ("finite_index","dest_finite_image")
  (prove
   (`?x. x IN 1..dimindex(:A)`,
    EXISTS_TAC `1` THEN REWRITE_TAC[IN_NUMSEG; LE_REFL; DIMINDEX_GE_1]));;

let cart_tybij =
  new_type_definition "cart" ("mk_cart","dest_cart")
   (prove(`?f:(B)finite_image->A. T`,REWRITE_TAC[]));;

After that you can write

  A^N

(as syntax for `:(A,N)cart`), where you can "think" of N
as a natural number.

This is an engineered version of what you wrote after this:
that you can have functions that ignore their argument,
and just return information about the type of the argument
(`dimindex` in this case).

Freek