[ProofPower] Proving Properties of SML functions

[Roger Bishop Jones]

On Tuesday 18 May 2004  2:41 pm, Marcel Oliveira wrote:
> Hello everybody,
>
> I am trying to prove that the result of the application of a
> sml function defined by me is the same for two given
> arguments. By way of illustration, I am sending an example
> attached. In this example, I define two SML functions
> nat_union and itself. The property I want to prove is that for
> all int list xs, I have that nat_union xs xs = itself xs. This
> example is just an abstraction of my real problem, which I
> give a short description at the end of the att. Can anyone
> help me to prove this?

Doesn't look to me like you have a well-formulated
problem yet.
There seems to be some confusion of languages.
You are setting yourself up in a Z language context,
you have defined your function in SML and your "goal"
is in HOL.

You can't really reason about functions defined in SML,
you will have to translate your definition into Z
or HOL to reason about it.  The references to SML names
in your goal will have been interpreted as free variables
in HOL.

Roger Jones

- rbj01 at rbjones.com
   plain text email please (non-executable attachments are OK)