Date: Tue, 23 May 1995 21:59:00 +1000
From: Malcolm Newey <Malcolm.Newey@cs.anu.edu.au>
Message-Id: <199505231159.VAA15893@vega.anu.edu.au>
To: qed@mcs.anl.gov
Subject: Re: Undefined terms
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


In John Harrison's recent posting he discussed limits in analysis and his
preferred use of a relation ( --> meaning tends to), instead of the use
of the limit function ( lim: ((real->real)->real) ).  This should have been
labelled as a separate technique for coping with undefined terms:

	[6]	Simply resist the temptation to write a partial function
		using functional notation and, instead, capture the notion
		by means of a relation.  If  F  is a partial function we
		find difficult to deal with in our logic, then we can
		introduce a constant for a corresponding relation F':
			F'(x,y)  iff  F(x) is defined and F(x)=y

This is a technique widely used in the HOL community; in fact, it is common
practice when defining a function to first introduce a relation F' that
expresses the partial function exactly.  Having so done, we can prove that
F' can be extended to a total function.  Depending on how we do it, a
function can then be defined according to technique [1] or [2].