Re: [isabelle] partial functions

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"


On 17 Jan 2014, at 11:52, Roger H. <s57076 at> wrote:

> Hi,
> how can i prove
> "the (f a) = b ⟶  ((f |` (- {a}))(a ↦ b)) = f"
> Thank you!

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.