Re: [isabelle] Evaluation of List.coset



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.