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



The cheapest approach is to identify tuples with lists and use "listset A", the set of all lists over A. If size matters, you could define your own set former, eg "vector A n = {xs : listset A. size xs = n}".

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.

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






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