*To*: nipkow at in.tum.de*Subject*: Re: [isabelle] beginner question: why isn't my lemma applied?*From*: Andrew Pimlott <andrew at pimlott.net>*Date*: Mon, 3 Oct 2005 17:49:54 -0700*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <20051002141241.F0FBC42F2A@atbroy30.informatik.tu-muenchen.de>*References*: <20051001013554.GN2194@pimlott.net> <20051002141241.F0FBC42F2A@atbroy30.informatik.tu-muenchen.de>*User-agent*: Mutt/1.5.9i

On Sun, Oct 02, 2005 at 04:12:41PM +0200, nipkow at in.tum.de wrote: > > lemma samekeys: > > "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'"; > > > > However, I could not get samekeys to be used to simplify it. > > The simplifier cannot guess what v' is supposed to be. Hence it cannot be > used as a rewrite rule. Only the more restrictive version > "(haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k') = True"; > is used, which doesn't help here. > > lemma > "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'"; > > This one can be used by the simplifier: although it is equally unclear what v > is supposed to be when the simplifier starts proving the precondition of the > rule, this is a special case: if the precondition is directly present as an > assumption, v is found by matching with that assumption. Thank you to everyone who replied. Continuing along the train that led to my posting, I proved the lemma with implication above, which I called samekeys2. (I can either prove it from the lemma with equality by applying subst, as others suggested, or prove it directly by induction.) I then tried to prove a lemma about a related function, uniquekeys (again, full code is below): lemma samekeys3[simp]: "uniquekeys (ps @ (k,v) # qs) --> uniquekeys (ps @ (k,v') # qs)"; apply (induct_tac ps); apply (auto); At this point, I had: 1. !!a list. [| ~ haskey (list @ (k, v) # qs) a; uniquekeys (list @ (k, v) # qs); uniquekeys (list @ (k, v') # qs); haskey (list @ (k, v') # qs) a |] ==> False This is where I was stuck before, but thanks to your help, I tried applying samekeys2: apply (simp add: samekeys2); I get warnings about exceeding the simplification depth, but eventually "No subgoals!". Probably not ideal, but hopefully I'll be able to reach my destination in this manner, then come back when I'm wiser and find a better way. Andrew theory Assoc = Main: consts haskey :: "('key * 'val)list => 'key => bool" uniquekeys :: "('key * 'val)list => bool"; primrec "haskey [] k = False" "haskey (p#ps) k = (let (k',v') = p in k=k' | haskey ps k)"; primrec "uniquekeys [] = True" "uniquekeys (p#ps) = (let (k,v) = p in ~(haskey ps k) & uniquekeys ps)"; 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 samekeys2: "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'"; apply (subst samekeys); apply (auto); done; lemma samekeys3[simp]: "uniquekeys (ps @ (k,v) # qs) --> uniquekeys (ps @ (k,v') # qs)"; apply (induct_tac ps); apply (auto); apply (simp add: samekeys2); -- goes into a loop, but finally works! done;

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

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

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

- Previous by Date: [isabelle] Isabelle and Automatic Theorem Provers
- Next by Date: Re: [isabelle] beginner question: why isn't my lemma applied?
- Previous by Thread: Re: [isabelle] beginner question: why isn't my lemma applied?
- 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