Re: [isabelle] a simplifier question 2
thanx for the explanation.
however, note that in the third proof I didn't write
> apply (simp add: power_add)
> 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
> 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
I can't see very far,
I must be standing on the shoulders of midgets.
This archive was generated by a fusion of
Pipermail (Mailman edition) and