*To*: John Munroe <munddr at googlemail.com>*Subject*: Re: [isabelle] Equal on function objects*From*: Rafal Kolanski <rafalk at cse.unsw.edu.au>*Date*: Mon, 22 Feb 2010 19:47:07 +1100*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <e4d7be571002212350x63b3663bpfc6ca9d77ea3db41@mail.gmail.com>*References*: <e4d7be571002212350x63b3663bpfc6ca9d77ea3db41@mail.gmail.com>*User-agent*: Thunderbird 2.0.0.23 (X11/20090817)

John Munroe wrote:

Hi, I'm trying to show that two function objects are equal in the following: theory T1 imports Real begin typedecl T consts func1 :: "T => real" func2 :: "T => real" func3 :: "T => real" locale loc = assumes ax1: "func1 p = func2 p / func3 p" and ax2: "func3 p > 0" lemma (in loc) lem1: "ALL p. func2 p = func1 p * func3 p" using ax1 ax2 by (metis divide_le_eq divide_less_eq order_eq_refl order_less_irrefl xt1(11)) lemma (in loc) lem2: assumes "loc" shows "func2 = (%s. func1 s * func3 s)" using lem1 by auto Does anyone know why having lem1 as a fact is insufficient to complete the proof?

Try rule 'ext', specifically by (auto intro: ext) by (blast intro: ext) also solves it

Sincerely, Rafal Kolanski.

**References**:**[isabelle] Equal on function objects***From:*John Munroe

- Previous by Date: Re: [isabelle] datatype antiquotation
- Next by Date: Re: [isabelle] Why is 'auto' slow here?
- Previous by Thread: [isabelle] Equal on function objects
- Next by Thread: Re: [isabelle] Equal on function objects
- Cl-isabelle-users February 2010 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