Re: [isabelle] expanding function composition after induction



Thank you. This explains it.

Viorel

On 11/28/2014 5:09 PM, Tobias Nipkow wrote:
Terms are eta-contracted before printing and rule application (eg in induction) may eta-expand terms. If you always want to see the uncontracted version:

declare [[eta_contract=false]]

Tobias


On 28/11/2014 15:59, Viorel Preoteasa wrote:
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.

Viorel


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.

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











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