Re: [isabelle] a simplifier question 2

On 07.06.2015 01:30, noam neer wrote:

[simplifier questions]

The simplifier performs (primarily) rewriting. A term t will be
rewritten with an equation s = s' if there is some substitution of the
variables Ï, such that t is syntactically equal to sÏ. Then t is
replaced by s'Ï. The simplifier tries to do this for all subterms of the

Recall, power_add is the theorem: ?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n

Now, for your proof attempts:

>    lemma
>      fixes   a::real
>      shows   "a^6 = a^3 * a^3"
>    using [[simp_trace=true]]
>    using power_add [of a 3 3]
>    by simp 

This works as the simplifier can rewrite "3 + 3" to 6 and can then solve
the goal by rewriting with "a^6 = a^3 * a^3".

>    using power_add

The simplifier cannot rewrite "?m + ?n" to anything. It also does not match the "6" in the goal.

>    apply (simp add: power_add)

Similar. "a^6" does not match "?a ^ (?m + ?n)".

In my opinion, the nicest proof is:

   apply (simp add: power_add[symmetric])

The [symmetric] reverses the equation.

  -- Lars

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