*To*: Roger H. <s57076 at hotmail.com>*Subject*: Re: [isabelle] partial functions*From*: John Wickerson <johnwickerson at cantab.net>*Date*: Fri, 17 Jan 2014 11:56:37 +0000*Cc*: "isabelle-users at cl.cam.ac.uk" <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <DUB124-W17E042E2DB92B48BFBC9238FB80@phx.gbl>*References*: <DUB124-W17E042E2DB92B48BFBC9238FB80@phx.gbl>

I don't think you can. The fact that "the (f a)" is equal to "b" does not mean that "a" is in the domain of "f". Isabelle functions are always total, even "the". So the fact that "the (f a)" is equal to *something* doesn't actually tell you anything. What you might have more luck with is this: > "f a = Some b ⟶ ((f |` (- {a}))(a ↦ b)) = f" John On 17 Jan 2014, at 11:52, Roger H. <s57076 at hotmail.com> wrote: > Hi, > > how can i prove > > "the (f a) = b ⟶ ((f |` (- {a}))(a ↦ b)) = f" > > Thank you! >

**References**:**[isabelle] partial functions***From:*Roger H .

- Previous by Date: [isabelle] partial functions
- Next by Date: [isabelle] partial functions
- Previous by Thread: [isabelle] partial functions
- Next by Thread: [isabelle] partial functions
- Cl-isabelle-users January 2014 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