*To*: Isabelle Mailing List <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] beginner question: why isn't my lemma applied?*From*: Andrew Pimlott <andrew at pimlott.net>*Date*: Fri, 30 Sep 2005 18:35:54 -0700*Cc*:*User-agent*: Mutt/1.5.9i

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'"; -- ???

**Follow-Ups**:**Re: [isabelle] beginner question: why isn't my lemma applied?***From:*Rafal Kolanski

**[isabelle] Re: beginner question: why isn't my lemma applied?***From:*Tjark Weber

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

- Next by Date: [isabelle] want to join with u
- Next by Thread: Re: [isabelle] beginner question: why isn't my lemma applied?
- Cl-isabelle-users October 2005 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list