Re: [isabelle] beginner question: why isn't my lemma applied?

>    lemma samekeys:
>      "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'";
>
> However, I could not get samekeys to be used to simplify it.

The simplifier cannot guess what v' is supposed to be. Hence it cannot be
used as a rewrite rule. Only the more restrictive version
"(haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k') = True";
is used, which doesn't help here.

lemma
"haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'";

This one can be used by the simplifier: although it is equally unclear what v
is supposed to be when the simplifier starts proving the precondition of the
rule, this is a special case: if the precondition is directly present as an
assumption, v is found by matching with that assumption. This is the case in
your example. There is no danger of infinite descent here, because the
simplifier will not attempt to prove a precondition with an unknown (v)
again by rewriting but only by direct instantiation with an assumption.

Tobias

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