Re: [isabelle] Problems with coercions

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.


> On 3 Oct 2017, at 12:41, Thiemann, Rene <Rene.Thiemann 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Ã

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