Re: [isabelle] expanding function composition after induction
Thank you. This explains it.
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
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
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
It is also strange that the rule comp_apply becomes applicable only
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
apply(auto simp del: comp_apply)
How to find out? Put "using [[simp_trace_new mode=full]]" in front
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"
lemma B: "F (f o g) (n::nat) = top"
apply (induction n)
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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and