*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] a simplifier question 2*From*: Lars Noschinski <noschinl at in.tum.de>*Date*: Mon, 15 Jun 2015 10:08:46 +0200*In-reply-to*: <CAGOKs0_g--XmvZS0u46-oRWc8h3HDJ2_nVjHzwSJtJV69CoVZA@mail.gmail.com>*References*: <CAGOKs09o8XAiVVm=GdjMAz3ezFQM93uiQVJ_Ugv3Z6Pg9sDxZQ@mail.gmail.com> <5573EED3.8000108@in.tum.de> <CAGOKs0_g--XmvZS0u46-oRWc8h3HDJ2_nVjHzwSJtJV69CoVZA@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Icedove/31.7.0

On 13.06.2015 15:59, noam neer wrote: > 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, You wouldn't get an error message about this -- an equation not matching the goal is the rule, not the exception ;) > 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 ? This means that that the simplifier falls over even earlier than I thought: Isabelle/HOL cannot quantify over types, so polymorphic rules (like power_add) are expressed by schematic type variables. If you do lemma fixes a::real shows "a^6 = a^3 * a^3" using power_add apply - you see that the schematic variables in power_add have been replaced by universally quantified variables. However, if you Ctrl+Hover over the bound variable "a", you see that it still has a schematic type. To use it for rewriting, these variables must be instantiated. The simplifier does not instantiate type variables (except in a few circumstances), so it rejects this rule. For your experiments, you can instantiate the type variables in the lemma by writing using power_add[where 'a=real] instead. -- Lars

**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: [isabelle] PeaCoq: web-based frontend for Coq
- Next by Date: Re: [isabelle] libisabelle: embedding on ML-side
- Previous by Thread: Re: [isabelle] a simplifier question 2
- Next by Thread: [isabelle] AVoCS 2015: Extended Paper Deadline
- 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