Re: [isabelle] a simplifier question 2



hi again.your explanation for the first failed proof :

    theory tmp
    imports Complex_Main
    begin
        lemma
          fixes   a::real
          shows   "a^6 = a^3 * a^3"
        using [[simp_trace=true]]
        using power_add
        by simp
    end

sounds reasonable. however, when I give it to Isabelle I don't get an
error message saying it can't match power_add to the goal, I get some
complaint about type unknowns :

    lemma ?a ^ 6 = ?a ^ 3 * ?a ^ 3
    [1]SIMPLIFIER INVOKED ON THE FOLLOWING TERM:
    (âa m n. a ^ (m + n) = a ^ m * a ^ n) â a ^ 6 = a ^ 3 * a ^ 3
    [1]Cannot add premise as rewrite rule because it contains (type) unknowns:
    âa m n. a ^ (m + n) = a ^ m * a ^ n
    Failed to apply initial proof methodâ:
    using this:
      ?a ^ (?m + ?n) = ?a ^ ?m * ?a ^ ?n
    goal (1 subgoal):
     1. a ^ 6 = a ^ 3 * a ^ 3

what does it mean ?


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
>
> 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 MHonArc.