*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Reasoning about k-fold cartesian products*From*: Michael Norrish <Michael.Norrish at nicta.com.au>*Date*: Mon, 12 May 2008 10:13:23 +1000*Cc*: Denis Bueno <dbueno at gmail.com>*In-reply-to*: <48240A4F.1070006@in.tum.de>*References*: <6dbd4d000805081412v52d6d55dt298c8fa964204c8b@mail.gmail.com> <48240A4F.1070006@in.tum.de>*User-agent*: Thunderbird 2.0.0.14 (Macintosh/20080421)

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.

**Follow-Ups**:**[isabelle] lemmas following from inductive definitions***From:*Jeremy Dawson

**References**:**[isabelle] Reasoning about k-fold cartesian products***From:*Denis Bueno

**Re: [isabelle] Reasoning about k-fold cartesian products***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] quickcheck and error constants
- Next by Date: Re: [isabelle] cannot run sledgehammer
- Previous by Thread: Re: [isabelle] Reasoning about k-fold cartesian products
- Next by Thread: [isabelle] lemmas following from inductive definitions
- Cl-isabelle-users May 2008 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list