Re: [isabelle] Reasoning about k-fold cartesian products



Tobias Nipkow wrote:

> The problem with iterating <*> is that its result type would depend
> on the value n. Such dependent types can (in general) not be formed
> in HOL.  However, there is a trick due to John Harrison how this can
> be done for A^n after all. I hope somebody else will comment on
> this. The Word library follows this approach already.

I have ported this trick to Isabelle in a short theory file, which I
hope to make available.  (Not that it's hard to do.)

In fact, the Word library doesn't use this trick.  The Word library
allows a type of words of dimension zero, which would be impossible
using the Harrison type.

The Harrison approach is to use the type

  'a::finite -> 'b

to represent an "array" of card(Univ::'a set) many 'b values.

The type 'a has to be finite in order to have card make sense.  The
type 'a (in common with all HOL types) can't be empty, so you can't
get the singleton value corresponding to a function of empty domain.

(Of course, if you actually wanted infinte cartesian products, you'd
drop the finite-ness requirement.)

HOL4's word library does use Harrison arrays.

In Isabelle's Word library, the representation of an 'a word is

  { 0 ..<  2 ^ len_of TYPE('a::len0) }

where the len0 class requires the len_of function.  The cardinality of
the 'a type is thus irrelevant to the construction.

In both systems, syntax is set up so that the array types can be
written

  bool[12]

  'a[10]

etc.

Michael.








This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.