*To*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Subject*: Re: [isabelle] Instantiation names problems*From*: Jesus Aransay <jesus-maria.aransay at unirioja.es>*Date*: Tue, 29 Jan 2013 12:16:04 +0100*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <51077D49.7090001@inf.ethz.ch>*References*: <CAL0S8BfGK4NY8=27JAEuA4WwsBAkLtMdzsLzEZzSBpHkgnxJeg@mail.gmail.com> <51077D49.7090001@inf.ethz.ch>*Sender*: jmaransay at gmail.com

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

**Follow-Ups**:**Re: [isabelle] Instantiation names problems***From:*Andreas Lochbihler

**References**:**[isabelle] Instantiation names problems***From:*Jesus Aransay

**Re: [isabelle] Instantiation names problems***From:*Andreas Lochbihler

- Previous by Date: Re: [isabelle] Instantiation names problems
- Next by Date: Re: [isabelle] Instantiation names problems
- Previous by Thread: Re: [isabelle] Instantiation names problems
- Next by Thread: Re: [isabelle] Instantiation names problems
- Cl-isabelle-users January 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list