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


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"

"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)


Rafal Kolanski.

Andrew Pimlott wrote:
I just started learning Isabelle, and usually write Haskell, so please
excuse my pidgin HOL.

I have been working through the tutorial "A Proof Assistant for
Higher-Order Logic", and for Exercise 3.4.5, I am proving some
properties of association lists (full code appended).  I proved

    lemma samekeys:
      "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'";

and then tried to use it to prove another theorem.  It looked promising,
because both "haskey (ps @ (k,v) # qs) k'" and "~ haskey (ps @ (k,v') #
qs) k'" showed up in the assumption, a contradiction.  However, I could
not get samekeys to be used to simplify it.  A simpler lemma I cannot
prove using samekeys is

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

When I "apply (simp add: samekeys);", nothing happens.  If I replace the
implication with equality, however, it works.  I also tried applying
various combinations of universal quantification with no success.

Is this happening because either side could be simplified by samekeys?
What can I do?  Do I have to rephrase samekeys to be less symmetric?
Thanks for any hints.

I am using the Linux binary download of Isabelle2004.tar.gz, with smlnj,
and run my code with "isabelle -I".

(A funny thing is that while writing this mail, I really understood what
is meant by the definitional as opposed to axiomatic approach.  I
couldn't just "make up" properties to concoct a minimal example!)


PS. Credit for the joke goes to Paul Steckler <steck at>.

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