Re: [isabelle] Why can't auto prove that goal: f (x+(y+z)) = f ((x+y)+z)



On Tue, Aug 31, 2010 at 9:32 AM, Peter Lammich
<peter.lammich at uni-muenster.de> wrote:
> Recently, auto left me a goal of the form
>  f (x+(y+z)) = f ((x+y)+z)
>  x,y,z :: nat
>
> I always thought the simplifier would rewrite the right sum automatically.
> However, when searching for the corresponding theorem, I cannot find it:
>
> find_theorems "_ + (_ + (_::nat)) = _ + _ + _"
>
> searched for:
>
>  "_ + (_ + _) = _ + _ + _"
>
> nothing found in 0.111 secs
>
> What's going on here, how is associativity of + on nats implemented?

Hi Peter,

You didn't find the theorem "add_assoc" because it is oriented the other way:

"(x + y) + z = x + (y + z)"

As far as I know, all associativity theorems (for multiplication,
etc.) in the main libraries are oriented like this.

> btw: I now prove this goal by (rule arg_cong, simp) or by adding "intro:
> arg_cong" to auto's arguments,
>    but I would have much more liked to write: "simp add: add_a" or something

Try "simp add: add_ac", which will rewrite additions to a normal form,
with terms in sorted order and additions grouped to the right.

- Brian





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