# Re: [isabelle] a simplifier question 3

On 20.06.2015 01:19, noam neer wrote:
> lemma "(4::nat) = 1+1+1+1"
> by (simp only : algebra_simps)
This is not solved by the simplifier itself but by one of the arithmetic
solvers employed by the simplifier, I guess "linarith" in this instance.
The algebra_simps are not necessary, the goal is also solved by "simp
only:".
>
> lemma "(x::real) ^ (4::nat) = x ^ (1+1+1+(1::nat))"
> by (simp only : algebra_simps)
The arithmetic solvers cannot deal with powers, so they cannot solve
this goal.
One solution would be to prove "4 = 1+1+1+1" first and feed this fact
into the second equation. If you have longer chains of such reasoning,
have a look into calculational reasoning (chapter 1.2 of the Isar
reference manual). You could also use the rule "arg_cong" to remove the
"x ^ _" on both sides, but this is a rather low-level style of proof.
-- Lars

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