Email Gateway (Aug 18 2022 at 11:50): Email Gateway (Aug 18 2022 at 11:50):From: Denis Bueno <dbueno@gmail.com>
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
Email Gateway (Aug 18 2022 at 11:50):From: Tobias Nipkow <nipkow@in.tum.de>
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:
Email Gateway (Aug 18 2022 at 11:51):From: Michael Norrish <Michael.Norrish@nicta.com.au>
Tobias Nipkow wrote:
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.
I have ported this trick to Isabelle in a short theory file, which I
hope to make available. (Not that it's hard to do.)
In fact, the Word library doesn't use this trick. The Word library
allows a type of words of dimension zero, which would be impossible
using the Harrison type.
The Harrison approach is to use the type
'a::finite -> 'b
to represent an "array" of card(Univ::'a set) many 'b values.
The type 'a has to be finite in order to have card make sense. The
type 'a (in common with all HOL types) can't be empty, so you can't
get the singleton value corresponding to a function of empty domain.
(Of course, if you actually wanted infinte cartesian products, you'd
drop the finite-ness requirement.)
HOL4's word library does use Harrison arrays.
In Isabelle's Word library, the representation of an 'a word is
{ 0 ..< 2 ^ len_of TYPE('a::len0) }
where the len0 class requires the len_of function. The cardinality of
the 'a type is thus irrelevant to the construction.
In both systems, syntax is set up so that the array types can be
written
bool[12]
'a[10]
etc.
Michael.
Last updated: May 03 2024 at 08:18 UTC