Re: [isabelle] expanding function composition after induction

It works if I add "del: comp_apply", but I still do not understand why?
My term does not contain "(f o g) a", so comp_apply does not seem to match
any sub-term. I tried before to remove comp_def which is applicable
to (f o g), but then I got the warning that  comp_def is not a simp rule.

It is also strange that the rule comp_apply becomes applicable only
after induction.


On 11/28/2014 4:25 PM, Tobias Nipkow wrote:
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

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