[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 , 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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and