Full-Name: Joshua D. Guttman
Posted-Date: Tue, 30 Jul 91 08:54:36 -0400
Date: Tue, 30 Jul 91 08:54:36 -0400
From: guttman@org.mitre.linus
Message-Id: <9107301254.AA00690@malabar.mitre.org>
To: info-hol@edu.uidaho.cs.ted
In-Reply-To: Mike Gordon's message of Mon, 29 Jul 1991 11:11:17 GM
Subject: Select operator (practical perspective)
Postal-Address: MITRE, Mail Stop A156 \\ Burlington Rd. \\ Bedford, MA 01730

One of the examples that Mike mentions seems like a thicket to me:

> I looked around in my own files and the HOL Library to see what other
> uses of epsilon I could find.
>
> Here is the definition of the inverse of a function:
>
>    define "INVERSE(f:*->**) = \y. @x. f x = y"
>
> This isn't a definite description.

But it's probably not a good definition of inverse either.  For instance
f^{-1}(f(x)) may be defined and different from x, even when f(x) is defined.
Inverse probably needs to be a relation between functions rather than a
functional.

How does HOL treat new_specification?  Do you think of it as changing the
language/theory that you're working in?  The switch to an extended theory would
be justified by the (meta)theorem that any model of the original theory can be
expanded (by enriching its signature) to a model of the new theory.  This is a
stronger property than being a conservative extension, and is sometimes called
being a model conservative extension.

This approach would require that the "loosely defining" property for the
new_specification be a syntactically closed expression.

Probably new_specification is more intuitive (and thus, more reliable) than @.


        Josh