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"

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!
> 		 	   		  





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