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



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

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

Andrew

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


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

declare Let_def[simp];

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

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






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