[ProofPower] Proving Properties of SML functions

[Roger Bishop Jones]

On Tuesday 18 May 2004  3:40 pm, Marcel Oliveira wrote:

> Do you suggest any better approach to me? I know I am confused
> right now, and I really neeed some light ;-)

There hasn't been a lot of metatheoretic work done in ProofPower
as far as I am aware, and some of the things you would
naturally use for this kind of thing (like recursive datatypes
for abstract syntax) are not well provided for.
That means that you have to be smart in the way you
code these things up.

Fortunately there is one good example provided by Rob Arthan
who did the metatheory for ProofPower HOL in ProofPower HOL.
So I recommend you look at that and see whether the methods
he used will adapt to your problem.

The material is in the ProofPower distribution and
may be found in the five documents spc001 to spc005.

    * HOL Formalised: Language and Overview
    * HOL Formalised: Semantics
    * HOL Formalised: Deductive System
    * HOL Formalised: Proof Development System
    * HOL Formalised: Formal Design of the Logical Kernel

Roger Jones

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