*To*: Denis Bueno <dbueno at gmail.com>*Subject*: Re: [isabelle] Reasoning about k-fold cartesian products*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Fri, 09 May 2008 10:24:47 +0200*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <6dbd4d000805081412v52d6d55dt298c8fa964204c8b@mail.gmail.com>*References*: <6dbd4d000805081412v52d6d55dt298c8fa964204c8b@mail.gmail.com>*User-agent*: Thunderbird 1.5.0.7 (X11/20060909)

Tobias Denis Bueno wrote:

I'm an Isabelle newbie trying to verify a proof. The statement of the proof (on paper) involves a natural number parameter k, and the k-fold cartesian product of a set. How would people reasoning in Isabelle approach this? How would you represent the cross product? I saw the <*> operator in Finite_Set, but am not sure how to generalise. The proof is Theorem 2 of a paper on Hyperproperties [0], in case you'd like more detail. I've just begun formalising it, so I don't think it's worth attaching my proof script. [0] http://www.cs.cornell.edu/people/clarkson/papers/clarkson_hyperproperties.pdf

**Follow-Ups**:**Re: [isabelle] Reasoning about k-fold cartesian products***From:*Michael Norrish

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

- Previous by Date: [isabelle] Hiding import of SList
- Next by Date: Re: [isabelle] Hiding import of SList
- Previous by Thread: [isabelle] Reasoning about k-fold cartesian products
- Next by Thread: Re: [isabelle] Reasoning about k-fold cartesian products
- 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