*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] a simplifier question 2*From*: Manuel Eberl <eberlm at in.tum.de>*Date*: Mon, 08 Jun 2015 11:42:33 +0200*In-reply-to*: <CAGOKs08ESWyN7NRq_wyMrOzz-EtbnEGJf-n2VkWwBPB4fSXnag@mail.gmail.com>*References*: <CAGOKs09o8XAiVVm=GdjMAz3ezFQM93uiQVJ_Ugv3Z6Pg9sDxZQ@mail.gmail.com> <5573EED3.8000108@in.tum.de> <CAGOKs08ESWyN7NRq_wyMrOzz-EtbnEGJf-n2VkWwBPB4fSXnag@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Manuel On 08/06/15 11:20, noam neer wrote:

thanx for the explanation. however, note that in the third proof I didn't writeapply (simp add: power_add)butby (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 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 simpThis 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_addThe 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

**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

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

- Previous by Date: Re: [isabelle] a simplifier question 2
- Next by Date: Re: [isabelle] a simplifier question 2
- 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