*To*: Dmitriy Traytel <traytel at inf.ethz.ch>*Subject*: Re: [isabelle] Problems with coercions*From*: "Yamada, Akihisa" <Akihisa.Yamada at uibk.ac.at>*Date*: Tue, 3 Oct 2017 15:58:46 +0000*Accept-language*: en-US, de-AT*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>, "Thiemann, Rene" <Rene.Thiemann at uibk.ac.at>*In-reply-to*: <C18A86EE-7E2A-47F5-B7A4-A456E0AC7879@inf.ethz.ch>*References*: <763020B0-6928-4F48-BDDE-FE7FDDF142F4@exchange.uibk.ac.at> <C18A86EE-7E2A-47F5-B7A4-A456E0AC7879@inf.ethz.ch>*Thread-index*: AQHTPDQyEewr7suJR0ecRtbpw67ZcKLR3pCAgABIfQA=*Thread-topic*: [isabelle] Problems with coercions

Dear Dmitriy, thanks for the explanation. If it sees "sr :: real" in the lemma statement but not in the proof, why does the following fail? lemma "{x. cmod x = sr} = range (op * sr)" proof - show "{x. cmod x = (sr :: real)} = range (op * (sr::real))" oops If I further annotate the lemma statement, it will work. Anyway, if it's not a surprising outcome of the design, I'll be surprised by the design. Cheers, Akihisa > On 3 Oct 2017, at 13:39, Dmitriy Traytel <traytel at inf.ethz.ch> wrote: > > Hi RenÃ, > > interesting observation, but not really surprising. > > After parsing (and inserting coercions into) the lemma statement, sr gets declared in the context (as a real). Coercion inference must respect such declarations. To do so, instead of a free variable sr, it will now see "sr :: real". I.e., the term that the constraint inference sees at "show" is not the same as the one at "lemma". This influences the internal constraint solving and affects the end result in this case. > > A workaround is to fix the type of sr in the context using the long goal format, before the lemma's statement is parsed. > > Cheers, > Dmitriy > >> On 3 Oct 2017, at 12:41, Thiemann, Rene <Rene.Thiemann at uibk.ac.at> wrote: >> >> Dear All, >> >> consider the following theory >> >> theory Test >> imports HOL.Complex >> begin >> >> lemma "{x. cmod x = sr} = range (op * sr)" >> proof - >> show "{x. cmod x = sr} = range (op * sr)" >> (* failed to refine any pending goal *) >> text âproof line is parsed as @{term "{x. cmod (complex_of_real x) = sr} = range (op * sr)"}â >> text âgoal is parsed as @{term "{x. cmod x = sr} = range (op * (complex_of_real sr))"}â >> oops >> >> end >> >> >> Here, the same formula is parsed differently in the lemma-statement and in the proof, >> which at least I found quite confusing. >> >> The effect appears in both Isabelle 2017-RC3 as well as in c90fb8bee1dd. >> >> Cheers, >> RenÃ > >

**Follow-Ups**:**Re: [isabelle] Problems with coercions***From:*Dmitriy Traytel

**References**:**[isabelle] Problems with coercions***From:*Thiemann, Rene

**Re: [isabelle] Problems with coercions***From:*Dmitriy Traytel

- Previous by Date: [isabelle] Isabelle2017-RC3 and Sledgehammer
- Next by Date: Re: [isabelle] Problems with coercions
- Previous by Thread: Re: [isabelle] Problems with coercions
- Next by Thread: Re: [isabelle] Problems with coercions
- Cl-isabelle-users October 2017 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