*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] a simplifier question 2*From*: noam neer <noamneer at gmail.com>*Date*: Sat, 13 Jun 2015 16:59:31 +0300*Cc*: "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <5573EED3.8000108@in.tum.de>*References*: <CAGOKs09o8XAiVVm=GdjMAz3ezFQM93uiQVJ_Ugv3Z6Pg9sDxZQ@mail.gmail.com> <5573EED3.8000108@in.tum.de>

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.

**Follow-Ups**:**Re: [isabelle] a simplifier question 2***From:*Lars Noschinski

**References**:**[isabelle] a simplifier question 2***From:*noam neer

**Re: [isabelle] a simplifier question 2***From:*Lars Noschinski

- Previous by Date: Re: [isabelle] Splicing runtime ML values into Isar
- Next by Date: Re: [isabelle] Splicing runtime ML values into Isar
- Previous by Thread: Re: [isabelle] a simplifier question 2
- Next by Thread: Re: [isabelle] a simplifier question 2
- Cl-isabelle-users June 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list