*To*: Andrew Pimlott <andrew at pimlott.net>*Subject*: [isabelle] Re: beginner question: why isn't my lemma applied?*From*: Tjark Weber <tjark.weber at gmx.de>*Date*: Sun, 2 Oct 2005 04:22:55 +0200*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*: KMail/1.8

Andrew, On Saturday 01 October 2005 03:35, Andrew Pimlott wrote: > lemma samekeys: > "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'"; > lemma "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'"; > -- ??? maybe someone else is going to write more about the simplifier, but the following proof should solve your goal: apply (subst samekeys) apply auto done Best regards, Tjark

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

- Previous by Date: Re: [isabelle] beginner question: why isn't my lemma applied?
- 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