[Why3-club] Finite vs infinite sets

Stefan Berghofer berghofe at in.tum.de
Thu Nov 7 17:23:41 CET 2013

Dear Why3-Club,

I just stumbled upon the theory set.why declaring a type "set 'a" that, according to the
comment following the declaration, may be either finite or infinite. Later on, there is a
section introduced with the comment (** {2 Finite sets} *) containing axioms that are obviously
not true for infinite sets, such as

   axiom cardinal_remove:
     forall x : 'a. forall s : set 'a.
     mem x s -> cardinal s = 1 + cardinal (remove x s)

I would have expected this axiom to either have an additional assumption such as "finite s",
or to use a different type such as "fset 'a" denoting finite sets. Maybe I am just missing something?


More information about the Why3-club mailing list