Re: [isabelle] Instantiation names problems



Hi Jesus,

you are right, type inference is not the main problem here. The issue is that at the end of Enum.thy, unqualified access for enum, enum_all and enum_ex is disabled. So you have to use the names enum_class.enum, etc.; for the declarations in Enum.thy, the short names naturally work.

definition "enum_class.enum = ([] :: 'a bit0 list)"
definition "enum_class.enum_all P = (filter P ([]::'a bit0 list) = [])"
definition "enum_class.enum_ex P = (filter P enum_class.enum ≠ ([] :: 'a bit0 list))"

Best,
Andreas

On 01/29/2013 12:16 PM, Jesus Aransay wrote:
Hi Andreas,

thanks for your hint; I tried to be as exhaustive as I could with type
annotations, but the problem still persists;

instantiation bit0 :: (finite) enum
begin

definition "(enum::'a bit0 list) = ([]::'a bit0 list)"

definition "enum_all P = (filter P ([]::'a bit0 list) = [])"

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

thm enum_def (*This theorem refers to a constant named "local.enum"; I
guess this should not be the case*)
thm enum_bit0_def (*This theorem does not even exist in the context;
the same happens with enum_all and enum_ex*)

instance
proof (default)
show "(UNIV::'a bit0 set) = set enum" (*This show fails because enum
makes reference to "local.enum"*)

Thanks for any other suggestions,

Jesus


On Tue, Jan 29, 2013 at 8:42 AM, Andreas Lochbihler
<andreas.lochbihler at inf.ethz.ch> wrote:
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.