Re: [isabelle] a simplifier question 2



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




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.