Re: [isabelle] Instantiation names problems



Dear Jesus,

This looks like type inference gives you too generic types. Try to explicitly restrict the type like this, for both definitions and goal statements.

definition "(enum :: bit0 list) = []"
show "(UNIV :: bit0 set) = set enum"

Hope this helps
Andreas

On 01/29/2013 07:18 AM, Jesus Aransay wrote:
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.