Re: [isabelle] [Fwd: Something strange with simplifier and (op \<circ>)]
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
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".
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
and others not.
This archive was generated by a fusion of
Pipermail (Mailman edition) and