[isabelle] Evaluation of List.coset
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
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and