[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.