Delivery-Date: 
Sender: info-hol-request@edu.uidaho.cs.ted
Errors-To: info-hol-request@edu.uidaho.cs.ted
Precedence: bulk
From: David Shepherd <des@uk.co.inmos>
Message-Id: <21048.9209090846@frogland.inmos.co.uk>
Subject: Re: new_recursive_definition question
To: rachel@au.edu.anu.dubhe (Rachel Onate)
Date: Wed, 9 Sep 92 9:46:49 BST
Cc: info-hol@edu.uidaho.cs.ted
In-Reply-To: <9209090039.AA23235@cs.anu.edu.au>; from "Rachel Onate" at Sep 9, 92 10:39 am

Rachel Onate has said:
> I would like to know how the new_recursive_definition was implemented 
> with respect to a user's partial specification of a value of a function 
> defined on a concrete type, by allowing defining equations for some of 
> the constructors to be omitted.  The example given in the HOL System 
> description manual (1988, p179) was the definition of "Label" of the 
> leaves of the tree:
> 
> #let Label =
> # new_recursive_definition false btree_Axiom `Label`
> #  "Label (LEAF (x:*)) = x";;
> Label = |- !x. Label (LEAF x) = x
> 
> Here, an internal node does not have label, so it was left unspecified.

i assume that it uses the HOL loose specification mechanism. basically
a theorem is proved that a function with this specification exists
and then from that a constant can be defined. the existence proof 
will use a "witness" function that returns some arbitrary value on
constructors not in the clauses of the specification.

> More questions:
> (1) Doesn't HOL implement total functions only?

correct

> (2) What happens if a user try to access "Label (Node t1 t2)"?

no problem ... "Label" is a *total* function so "Label (Node t1 t2)"
does have a defined value ... its just that the defining theorem
doesn't tell you what it is and you could rewrite it to anything.

basically we have partial specifications of total functions so here
we can't infer anything about

	"Label (Node t1 t2)"

but we can prove

	|- (Label (Node t1 t2)) = (Label (Node t1 t2))


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk or des@inmos.com    tel: 0454-616616 x 625
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
                1992: celebrate the quincentenary of columbus getting lost