*Subject*: Re: [isabelle] beginner question: why isn't my lemma applied?*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Sun, 02 Oct 2005 02:17:50 +1000*Cc*: Isabelle Mailing List <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <20051001013554.GN2194@pimlott.net>*References*: <20051001013554.GN2194@pimlott.net>*User-agent*: Mozilla Thunderbird 1.0.2 (Windows/20050317)

Hi,

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

**References**:**[isabelle] beginner question: why isn't my lemma applied?***From:*Andrew Pimlott

- Previous by Date: [isabelle] want to join with u
- Next by Date: [isabelle] Re: beginner question: why isn't my lemma applied?
- Previous by Thread: [isabelle] beginner question: why isn't my lemma applied?
- Next by Thread: [isabelle] Re: 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