[isabelle] expanding function composition after induction



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





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