[isabelle] Evaluation of List.coset



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.