[isabelle] Instantiation names problems



Dear all,

based on the examples in "src/HOL/Enum.thy" I was trying to prove the
following instance (where the "[]" should be replaced by a suitable
representation of the universe of the intended type), still in Isabelle2012:

instantiation bit0 :: (finite) enum
begin

definition "enum = []"

definition "enum_all P = (filter P enum = enum)"

definition "enum_ex P = (filter P enum ≠ [])"

instance
proof (default)
show "UNIV = set enum"

-----

Whatever goal I try to state with "show" after the "proof (default)"
command, I always get an error

"Local statement will fail to solve any pending goal"

I can neither refer to definitions "enum_bit0_def",
"enum_all_bit0_def", "enum_ex_bit0_def" in the "instance" proof.

What am I doing wrong? Have I missed some type annotations, or should
I do the definitions names explicit?

Thanks for any ideas,

Jesus





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