Re: [isabelle] Instantiation names problems
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
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*)
show "(UNIV::'a bit0 set) = set enum" (*This show fails because enum
makes reference to "local.enum"*)
Thanks for any other suggestions,
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
> definition "(enum :: bit0 list) = "
> show "(UNIV :: bit0 set) = set enum"
> Hope this helps
> 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
>> instantiation bit0 :: (finite) enum
>> definition "enum = "
>> definition "enum_all P = (filter P enum = enum)"
>> definition "enum_ex P = (filter P enum ≠ )"
>> 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,
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