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
> 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:
"_ + _ + _ = _ + (_ + _)"
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.
> Best, Peter
This archive was generated by a fusion of
Pipermail (Mailman edition) and