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 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.






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