Re: [isabelle] Evaluation of List.coset

Hi Andreas,

thanks for your explanation.

In the Isabelle development version I observed that the file
"Cardinality.thy" has suffered some changes related to the behaviour
of "List.coset"; more concretely, the line 467 in
proves some results about "List.coset" of enumerated types "by eval";

does this means that in the incoming release of Isabelle 2013
"List.coset" will be really evaluated for "enum" types?

Looking forward for Isabelle 2013 ;-),


On Wed, Jan 30, 2013 at 8:18 AM, Andreas Lochbihler
<andreas.lochbihler at> wrote:
> Dear Jesus,
> By default, Isabelle represents sets as the list of its elements
> (constructor set) or of the complement (List.coset). The latter is mainly
> needed for representing UNIV as "List.coset []". Of course, you can
> implement List.coset in terms of set and enum, but then, you can only
> evaluate sets whose element type is an instance of enum - at least with the
> present setup for the code generator.
> If you want this, you must do the following:
> 1. Declare List.set as the only implementation constructor for sets:
> code_datatype set
> 2. Remove all code equations that pattern-match on List.coset, e.g.,
> declare union_coset_filter[code del]
> You can look in List.thy for which code equation pattern-match on
> List.coset, or print the whole code generator setup.
> 3. Implement List.coset as you have already tried. This will pull in the
> enum type class in many of the code equations for sets, so you will be
> restricted to elements of type enum, which excludes, e.g., nat.
> Best,
> Andreas
> On 01/30/2013 12:45 AM, Jesus Aransay wrote:
>> Dear all,
>> I was trying to carry out some experiments on code evaluation over finite
>> types.
>> I was interested in types which are instances of the "enum" type class
>> of the Isabelle library (file "Enum.thy"); this instance demands from
>> the user defining an explicit list representing the universe of the
>> type.
>> Then, I would expect "List.coset" to be capable of "evaluating" the
>> coset of a given list. Instead:
>> value "List.coset [True]"
>> returns its input.
>> I tried to introduce the following lemma:
>> lemma foo [code]: "List.coset (l::'a::enum list) = set
>> (enum_class.enum) - set l"
>>    by (metis Compl_eq_Diff_UNIV coset_def enum_UNIV)
>> But the system complains that "List.coset" is a constructor, and
>> cannot appear in the lhs.
>> Is there a way to get "List.coset" over an "enum" type to evaluate to
>> the complementary list of the underlying set?
>> Thanks for any hint,
>> Jesus

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