Email Gateway (Aug 17 2022 at 13:27): Email Gateway (Aug 17 2022 at 13:27):From: Tjark Weber <tjark.weber@gmx.de>
Andrew,
maybe someone else is going to write more about the simplifier, but the
following proof should solve your goal:
apply (subst samekeys)
apply auto
done
Best regards,
Tjark
Email Gateway (Aug 17 2022 at 13:27):From: Rafal Kolanski <rafalk@cse.unsw.edu.au>
Hi,
I don't really know what's gotten into simp ... it doesn't feel happy
with add:samekeys or only:samekeys even though it's obvious. Wild guess:
perhaps the fact that samekeys doesn't make things shorter prevents simp
from using it?
If you just want it to work while we await the Isabelle experts to
enlighten us, try this:
theory Assoc = Main:
consts haskey :: "('key * 'val)list => 'key => bool"
primrec
"haskey [] k = False"
"haskey (p#ps) k = (let (k',v') = p in k=k' | haskey ps k)"
lemma samekeys: "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'"
by (induct_tac ps, auto)
lemma "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'"
by (subst samekeys, blast)
Cheers,
Rafal Kolanski.
Andrew Pimlott wrote:
Email Gateway (Aug 17 2022 at 13:27):From: nipkow@in.tum.de
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
Last updated: May 03 2024 at 04:19 UTC