*To*: Lawrence Paulson <lp15 at cam.ac.uk>*Subject*: Re: [isabelle] Instantiating to a lambda expression*From*: John Munroe <munddr at gmail.com>*Date*: Sat, 15 Jan 2011 17:58:46 +0000*In-reply-to*: <7A5B48FF-57AD-490E-89FC-8C350D9BF37D@cam.ac.uk>*References*: <AANLkTikbUfcSkSRJNQRVZW4oYbuN8UH5sQEycSxghOg6@mail.gmail.com> <7A5B48FF-57AD-490E-89FC-8C350D9BF37D@cam.ac.uk>*Resent-date*: Sat, 15 Jan 2011 19:26:54 +0000*Resent-from*: Lawrence Paulson <lp15 at cam.ac.uk>*Resent-message-id*: <E1PeBm3-0006L0-FV@ppsw-52.csi.cam.ac.uk>*Resent-to*: isabelle-users <isabelle-users at cl.cam.ac.uk>

On Sat, Jan 15, 2011 at 5:55 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote: > My guess is that this instantiation is possible, but it's asking too much to expect the automation to invent this lambda-expression. > I see. Could you please suggest a way to proceed in this proof? Thanks John > Larry Paulson > > > On 15 Jan 2011, at 15:52, John Munroe wrote: > >> Hi, >> >> If i have >> >> consts >> foo :: "real => real" >> bar :: "real => real" >> >> and an axiom >> >> same_ax: "ALL (g1::real=>real) g2 x y. (y > x & g1 y - g1 x = g2 y - >> g2 x) --> g1 = g2" >> >> I can get a proof quite fine with: >> >> lemma lem1: "foo = bar" >> proof - >> have "ALL x y. y > x --> foo y - foo x = bar y - bar x" >> sorry >> then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar >> r2 - bar r1" >> by auto >> then show ?thesis >> using same_ax >> by auto >> qed >> >> However, if I change the type of bar to: >> >> bar :: "real => real => real", the following won't go through: >> >> lemma lem1: "ALL x. foo x = bar x 3" >> proof - >> have "ALL x y. y > x --> foo y - foo x = bar y 3 - bar x 3" >> sorry >> then obtain r1 r2 where #: "r2 > r1" and ##: "foo r2 - foo r1 = bar >> r2 3 - bar r1 3" >> by auto >> then show ?thesis >> using same_ax >> by auto >> >> How come g1 or g2 can't be instantiated to %x. bar x 3, which is of >> type real=>real? >> >> Thanks >> >> John >> > >

**References**:**[isabelle] Instantiating to a lambda expression***From:*John Munroe

**Re: [isabelle] Instantiating to a lambda expression***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] Instantiating to a lambda expression
- Next by Date: Re: [isabelle] Instantiating to a lambda expression
- Previous by Thread: Re: [isabelle] Instantiating to a lambda expression
- Next by Thread: Re: [isabelle] Instantiating to a lambda expression
- Cl-isabelle-users January 2011 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