# [isabelle] Reasoning about k-fold cartesian products

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
--
Denis

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