# Re: [isabelle] a simplifier question 2

Equations added to the simp set are not simplified themselves, so the simplifier will only rewrite "a^(3+3)", but still not "a^6". It might not even rewrite "a^(3+3)" to "a^3 * a^3", because "3+3" might be rewritten to "6" first.
```
Manuel

On 08/06/15 11:20, noam neer wrote:
```
```thanx for the explanation.
however, note that in the third proof I didn't write

```
```    apply (simp add: power_add)
```
```but

```
```    by (simp add:power_add [of a 3 3])
```
```so I'm adding "a^(3+3)=a^3 * a^3" to the simp set.
this doesn't match directly, but why wasn't the simplifier able
to simplify it to "a^6 = a^3 * a^3" ?

On Sun, Jun 7, 2015 at 10:12 AM, Lars Noschinski <noschinl at in.tum.de> wrote:

```
```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
goal.

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

```
```    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:

The [symmetric] reverses the equation.

-- Lars

```
```
```
```

```

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