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.