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
http://isabelle.in.tum.de/repos/isabelle/file/744934b818c7/src/HOL/Library/Cardinality.thy
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 ;-),

Jesus

On Wed, Jan 30, 2013 at 8:18 AM, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> 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.