Re: [isabelle] Instantiation names problems



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
>>
>



-- 
Jesús María Aransay Azofra
Universidad de La Rioja
Dpto. de Matemáticas y Computación
tlf.: (+34) 941299438 fax: (+34) 941299460
mail: jesus-maria.aransay at unirioja.es ; web: http://www.unirioja.es/cu/jearansa
Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España





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