Re: [isabelle] expanding function composition after induction

The culprit is comp_apply: (f ∘ g) a = f (g a) which you can of course remove:

apply(auto simp del: comp_apply)

How to find out? Put "using [[simp_trace_new mode=full]]" in front of your simp/auto command.


On 28/11/2014 14:46, Viorel Preoteasa wrote:

I have the theory:

theory test imports Main
   definition "F = top"

   lemma A: "F (f o g) (n::nat) = top"
     apply auto

   lemma B: "F (f o g) (n::nat) = top"
     apply (induction n)
     apply auto

The question is why in lemma A, auto fails as expected, while in lemma B auto
changes (f o g) into (λa. f (g a)). How can I prevent this change?

Best regards,

Viorel Preoteasa

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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