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



Peter Lammich schrieb:
> 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.

No, it does not normalize with associativity or communtativity
automatically.

> However, when searching for the corresponding theorem, I cannot find it:
> 
> find_theorems "_ + (_ + (_::nat)) = _ + _ + _"
> 
> searched for:
> 
>   "_ + (_ + _) = _ + _ + _"
> 
> nothing found in 0.111 secs

Associativity happens to be oriented the other way around:

searched for:
   "_ + _ + _ = _ + (_ + _)"

found 1 theorem(s) in 0.080 secs:

Nat.nat_add_assoc: ?m + ?n + ?k = ?m + (?n + ?k)


> What's going on here, how is associativity of + on nats implemented?
> 
> 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 like this

In such situations do

(simp add: algebra_simps)

The list algebra_simps contains all simp rules like AC that are not
included by default and covers many algebraic structures.

Tobias


> 
> Best, Peter





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