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

```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:
```
```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>.
```
```

```

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