Re: [isabelle] Instantiation names problems
This looks like type inference gives you too generic types. Try to
explicitly restrict the type like this, for both definitions and goal
definition "(enum :: bit0 list) = "
show "(UNIV :: bit0 set) = set enum"
Hope this helps
On 01/29/2013 07:18 AM, Jesus Aransay wrote:
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
definition "enum = "
definition "enum_all P = (filter P enum = enum)"
definition "enum_ex P = (filter P enum ≠ )"
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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and