Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]

Yes, it is exactly that. And the expansion to "%x. (f\<circ>g) x" was
done by the induct - method (no idea why, and why only at some places).
All in all this makes coping with lemmas like list.map_compose rather
counter-intuitive. Are there some general guidelines how one
should/could circumvent stuff like this or do I simply have to live with it.

Many thanks for pointing me to that (I did not even know that terms are
displayed eta-contracted by default)
  Peter Lammich

Lawrence Paulson wrote:
> My guess is that sometimes "(f\<circ>g)" has been eta-expanded and
> sometimes not. That is, sometimes it really is "(f\<circ>g)" and
> sometimes it is "%x. (f\<circ>g) x". The latter term will be rewritten
> using o_apply.
> Try resetting the "Eta Contract" option to make this visible:
>   * unset Isabelle > Settings > Eta Contract in Proof General,
>   * or at the ML level type "reset eta_contract".
> Larry Paulson
> On 7 Nov 2007, at 12:59, Peter Lammich wrote:
>> is there something special to the function composition (op \<circ>)
>> operator built in Isabelle?
>> I have some problems understanding the behaviour of the simplifier in
>> conjunction with the lemma o_apply.
>> A (simp (no_asm_use) only: o_apply) - command gives different results
>> depending on the proof context I use it in. For example,
>> it may but need not happen that a "(f\<circ>g)" is rewritten to
>> "\<lambda>u. f (g u)" by (simp (no_asm_use) only: o_apply) in the same
>> subgoal, depending on where it occurs in a proof.
>> It also happens that only some occurences of "(f\<circ>g)" are rewritten
>> and others not.

Peter Lammich, Institut für Informatik
Raum 715, Einsteinstrasse 62, 48149 Münster
Mail: peter.lammich at
Tel: 0251-83-32749
Mobil: 0163-5310380

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