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.
Tobias On 28/11/2014 14:46, Viorel Preoteasa wrote:
Hello, I have the theory: theory test imports Main begin definition "F = top" lemma A: "F (f o g) (n::nat) = top" apply auto sorry lemma B: "F (f o g) (n::nat) = top" apply (induction n) apply auto sorry end 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
Description: S/MIME Cryptographic Signature