Implementing Constructive Proof Rules for SML in MetaSML

This report describes the use of the MetaSML extension of the SML core language as an implementation medium for a system for the verification of a purely-functional subset of SML programs.

This system has a strong, and non-accidental resemblance to the system for mechanising proofs in Higher Order Logic, HOL. But whereas HOL is a system for proving mathematical theorems, whose domain of interpretation is a universe of infinite sets, and, which, in particular, treats each lambda-expression as denoting a mathematical function, our system deals with the result of evaluating expressions in SML restricted to the functional subset of ML.

As compared with the work of Boyer and Moore, we are providing a proof-checker, not a proof-finder. However, we would anticipate that it would be possible to incorporate HOL-style conversions, tactics and tacticals to ease the process of generating proofs.

As a consequence of our domain being SML, our proof rules are weaker than those of HOL. For example, HOL contains a proof rule that allows the user unconditionally to create the theorem |- t = t for any well-typed term t. Our system puts the interpretation on t=t that, as a conclusion of a theorem, it is a type-correct SML expression that will run to completion yielding the result true under conditions determined by the hypotheses of the theorem in which it occurs. There are two restrictions inherent in this requirement. Firstly if t is a function, then t = t is not well-typed, and so is not a valid inference. Secondly the code must run to completion, so that t=t is only valid if t engenders a computation that terminates normally for all type-correct values of its free variables.

So, for example, if fact is the factorial function as usually defined, fact = fact is not well-typed, and so |- fact=fact is not admissable as a theorem of our system; neither is fact n = fact n unconditionally valid in our system, for it is not the case that the evaluation of fact n will terminate normally for a negative integer argument. In fact, the appropriate theorem is 0<=n |- fact n = fact n

MetaSML

The prover is implemented in MetaSML [Sheard...] which is derived from SML by providing a quasi-quotation mechanism. If e is an SML expression of type t, then <e> is a MetaSML expression of type <t>. Thus the angle brackets <...> act to support a form of quotation, which resembles quasi-quotation in Scheme in that there is a local escape mechanism, using the tilde operator.

Note that MetaSML's handling of variables that are free in an expression but bound in the environment in which the expression was created avoids a variable capture problem arising from a sequence like the following: 

fun twice x = 2*x;

(*
code to create a theorem about twice
*)

fun twice f = f(f x)

(*
code which uses the earlier theorems about twice in the context
of the new definition.
*)
We need to say something about e.g. the status of + in <3 + 4> I've used the term "name" - the "+" is the name of the addition function.

Theorems say things about the result of computation

In our system we adopt the basic idea of HOL, which was due originally to Robin Milner, that a theorem is an abstract data-type of MetaSML whose only constructors are proof-rules; if these rules are sound, it is only possible for the user to construct theorems. So the validity of the theorems depends constructed by the user depends only on whether or not the proof-rules correctly capture the semantics of SML.

Given this repetoire of proof-rules, and given that a user has the ability to discover (but not change) the fine structure of theorems by using selector functions and patterns of MetaSML, it is possible to build systems which can partially automate the process of proof.

The logically significant components of the theorem data-type are a list of hypotheses and a conclusion. The data-type theorem might thus concretely be declared as 

datatype theorem = Thm of <bool> list * <bool> list;
Thus each hypothesis is a MetaSML term of type <bool>, that is to say it is a quoted SML expression, which when evaluated, will yield a truth-value. Likewise a conclusion is also a MetaSML list term of type <bool>.

Notation for theorems

If H is a set of hypotheses, represented as a list (without repetitions) then we use the notation 
            H |- t
for the theorem Theorem(G,t). When writing theorems we will drop the angle-brackets around the hypotheses and conclusions. Incidentally, the hypotheses of a theorem are conceptually a sequence, rather than a set. Certain proof rules operate on the first hypothesis of that sequence.

Consonantly typed environments

By a consonantly-typed environment for an expression is meant a mapping from variables to values whose domain includes the free variables of the expression and in which the image of each variable under the map belongs to the type ascribed to that variable by the SML type inference system.

Our proof rules will be sound if they can only generate theorems that satisfy the following data-invariant

The Theorem Invariant

For every consonantly-typed environment in for which each hypothesis of the theorem evaluates to true, the conclusion will also evaluate to true.

We use the notation t1 ==> t2 as an abbreviation for   if t1 then t2 else true, so that t2 is only evaluated if t1 evaluates to true. Thus ==> is not defined as an infix operator in ML, since that would imply a different evaluation rule.

Proof Rules are abstract constructors for theorems

The actual concrete constructor Theorem for theorems is not available to the user of the system. Instead she must employ proof rules. These are MetaSML functions which evaluate to a theorem, or occasionally, to a list of theorems.

We adopt the HOL convention of capitalising the names of the MetaSML functions which implement proof rules.

For exposition it is convenient to adopt the usual notation for proof rules 

     thm1,  thm2 ... thmn
    ______________________

       thm
which expresses the fact that thm is a sound deduction from thm1,thm2...thmn. This captures the basic pattern of deduction, which may be qualified by additional conditions expressed in the text. Further explanation is needed as to how the corresponding MetaSML function is used.

It is a consequence of our concept of soundness that we need more proof rules than HOL. This arises from the fact that the DISCH rule in HOL 

        g, H |- t
    ______________

        H |- g ==> t
is not sound in our system, for g might not halt unconditionally. HOL makes great use of this rule to move terms from the hypotheses to the conclusion, wherein they are transformed and then moved back by the UNDISCH rule. We, by contrast, need rules that will allow us to operate directly on the hypotheses of a theorem.

In addition to the proof-rules there is a set of axioms which are pre-created theorems expressing basic facts about SML, for example that addition over the int type is commutative.

Halting

The concept of halting is central to our system. We define the SML function 
    fun halts t = true;
Clearly, if we have a theorem |- halts e, for some expression e, then under the interpretation rules given above, the eager evaluation of the expression e must always terminate without exception. [In a lazy language, this would not be the case.]

However, this treatment means that we may not apply the usual rules of instantiation. For example, while for any variable x there is a theorem |- halts x , it is not permissable to substitute an arbitrary expression for x. Otherwise, for example, we could "prove" 

 |- halts(fact n)
Thus, in particular, many of our proof-rules will require extra termination conditions as compared with HOL.

The following basic rules are sound for halts:

HALTS_EVAL : term -> theorem 

     _____________

      |-  halts t
provided that t is a term with no free variables which evaluates without exception.

Justification Having no free variables, t evaluates without exception in every consonantly typed environment. From the definition of halts, halts t evaluates to true. Hence halts t is universally valid, and so the rule is sound.

For example 

    HALTS_EVAL <2+3>  =  |- halts 2+3

HALTS_VAR : term -> theorem 

     _______________

        |- halts v
provided that v is a variable.

Justification Any environment whose domain includes v is consonantly typed, and is an environment in which the evaluation of v terminates without exception. From the definition of halts, halts t evaluates to true. Hence halts t is universally valid and so the rule is sound.

Paths, Patterns Substitution and Matching

We use t1[x:=t2] to denote the term t1 with every free occurrence of the variable x replaced by t2, with suitable alpha-renaming to avoid free variable capture. Likewise, we use 

 t[x1..xn := a1..an]
to denote the term t1 with every free occurrence of the variables xi replaced by ai, with suitable alpha-renaming to avoid free variable capture.

We use the concept of a path to identify a particular sub-expression of an expression. 

type path = int list

We write t[p] to mean the sub-term of t addressed by the path p. We write t[p:=t'] to mean the result of replacing the sub-term of t addressed by the path p by t'.

Matching a Pattern against an Expression

We write p[x1..xn] to denote a pattern whose free variables are x1..xn.

Deduction in of our system could be treated by eliminating patterns from the discourse, translating everything into he lambda calculus. While this approach has the virtue of simplicity, it is achieved at the cost of moving the discourse significantly away form the source language, making it harder for the user to follow what is happening, and also making proofs longer.

There are three possible cases which arise if we try to match a pattern p against an expression t.

For example the pattern [] can never match the expression x::l, whereas the pattern 0 can sometimes match the expression n (when n evaluates to 0). TIM HELP!

The idea of a match can then be expressed as 

datatype match = Match of (< var > * < val > list) * <bool> list
Our approach is thus to define a function 
match :  ->  -> match option

fun BETA (x as <(fn #p => ~(f #p) | ~y) ~a>) =
       (case match p a of
          SOME sub => Thm([], < ~x = ~(f a) >)
        | NONE => BETA <~y ~a>)
  | BETA _ = error

p : ('a,X) pattern
f : X substitution -> <'b>
match : ('a,'b) pattern -> <'a> -> 'b substitution
y : <'a -> 'b>

Using Definitions in Proofs

It is a great convenience to allow definitions, made in the core-SML subset of MetaSML, to be used in proofs.

This requires some care, since it is a consequence of our concept of validity that a definition such as 

    fun double x = x*2;
cannot in general be made into the theorem 
    |- double x = x*2
since in general a function won't terminate. Instead, we introduce rules that allow a definition to be used directly in a proof. For the purposes of explication of the definitional rules, we write a definition 
val v = t
as 
  |-DEF  v = t
Since MetaSML keeps a firm hold on the scope of definitions, the following definitional-substitution rule preserves validity.

No problem is raised by recursive definitions. For example 

    fact 0 = 1 | fact n = n*fact(n-1)
is converted into the definition 
    |-DEF fact = fn 0 => 1 | n => n*fact(n-1)
Here the occurrence of fact in the 
fn...
expression is not a free variable but is instead the name of the factorial function.

DEF_RIGHT: path -> theorem -> theorem

DEF_RIGHT allows us to use a definition to replace a defined-name occurring in the conclusion of a theorem by its value. 
        |-DEF  v = t ,  H |- t1
   ___________________________________

            H |-  t1[p:=t]
provided t1[p] = v

As a MetaSML function, we provide DEF_RIGHT with a path to the occurrence of a name that is to be replaced by its definition, and a theorem in whose conclusion the replacement is to be done.

Justification

This rule expresses the fact that in evaluating an expression t1 containing v, the value t of v will be used. Therefore t1 and t1[p:=t] will evaluate to equal values.

In effect, DEF is unfolding the definition of v.

DEF_LEFT : path -> theorem -> theorem 

        |-DEF  v = t ,  g,G |- t1
   ___________________________________

        g[p:=t], H |- t1
provided g[p] = v.

As a MetaSML function we provide DEF_LEFT with a path to the occurrence of a name that is to be replaced by its definition, and a theorem in whose first hypothesis the replacement is to be done.

Justification

Essentially the same as for the previous rule.

The Main Inference Rules

These inference rules differ quite a lot from those of HOL, mostly because of the requirement that the conclusion of a valid theorem must represent a computation that terminates normally when the hypotheses all evaluate to true. The general effect of this is to require more rules.

In particular, we lose the reflexive rule of equality ( |- t = t ). Instead, this has to be proved in every case. It is (perhaps conditionally) true for combinations of the language primitives, but must be proved for user-defined functions.

Moreover, the classical reductio ad absurdam rule does not hold. From 

                not t |- false
we cannot conclude |- t . The first theorem says "whenever t terminates normally, it must evaluate to true", whereas the second says "t always evaluates to true".

Thus we are much more constrained in moving terms from the hypotheses to the conclusions of theorems than we are in HOL. As a consequence, our proof-rules require us to operate on hypotheses as well as conclusions.

The following are our basic rules.

PROMOTE : int -> theorem -> theorem;

PROMOTE serves to select a hypothesis to be operated on by a proof rule. 
g0...gi...gn |- t
__________________________

gi,g0...gi-1 gi+1...gn |- t
Justification Clearly changing the order of the hypotheses of a theorem does not violate its data-invariant.

ASSUME : term -> theorem;


           ________

            t |- t
Justification In any environment in which the hypothesis evaluates to true, the conclusion also evaluates to true

The soundness of this rule depends upon the fact that our terms are restricted to the functional subset of SML, in which the value of an expression is determined solely by the constant objects (including function closures) embodied in it and by the values that its free variables have in the environment in which it is evaluated.

SUBST : path -> term -> thm -> thm 

        H1  |- t1 = t1'          H |- t
        _________________________________________

             H1 union H |- t[p:=t1']
provided the structural identity t[p] = t1 holds.

Justification

The first theorem expresses the fact in any environment in which each expression in H1 evaluates to true, then t1 and t1' evaluate to equal values in the same environment. The second theorem expresses the fact that in any environment in which each expression in H evaluates to true, t also evaluates to true. The rule states that in any environment in which all the hypotheses in H1 and H evaluate to true, the term t with an occurrence of t1 replaced by t1' will also evaluate to true

This rule expresses the fact that objects which SML judges to be equal are indistinguishable by any SML program. It would not apply to a language such as Scheme, where it is possible to distinguish between objects that are structurally equivalent (using equal?) and those which are identical (using eq?).

SUBST_LEFT : path -> term -> thm -> thm

In the light of our discussion about the need for rules that operate on hypotheses, we also need the following: 
        H1  |- t1 = t1'          t2,G |- t3
        _________________________________________

           t2[p:=t1],  H1 union H |- t3
provided t2[p] = t1.

Justification Similar to that for SUBST.

RESOLVE : theorem -> theorem -> theorem 

    H |- t      H' |- t'
___________________________

     (H - t') union H' |- t

Justification Suppose all the terms of 

     (H - t') union H'
evaluate to true. Then t' evaluates to true, by the second input theorem. Therefore all the terms of H evaluate to true. Thus t evaluates to true.

DISCH : term -> theorem ->theorem -> theorem

Discharging an assumption proves to be more complex than it does in HOL, because we have to allow for the possibility of a computation not terminating. 
            H |- t2
_________________________________________

   halts t1,  (H - {t1}) |-  t1 ==> t2

Justification The theorem G |- t2 requires that in any environment in which all the expressions of H evaluate to true, then t2 also evaluates to true.

Now suppose we have an environment in which all the expressions of 

   halts t1 ( H - {t1} )
evaluate to true. In these circumstances we know that t1 halts. There are thus two cases to consider:

MP : theorem -> theorem -> theorem

MP implements the modus ponens rule of logic. 

    H1 |- t1 ==> t2,    H2 |- t1
    __________________________________

        H1 union H2  |-  t2

Justification

In an environment in which all the expressions of H1 union H2 evaluate to true, t1 will evaluate to true. In such an environment, 

    t1 ==> t2
has the same value as t2. But, since all the hypotheses in H1 also evaluate to true, it follows that t1 ==> t2 also evaluates to true, so t2 evaluates to true.

BETA : term -> thm;

Our equivalent of the BETA rule of HOL is complicated by our supporting patterns. 

  ____________________________________________________________

    halts t2 |-  (fn p[x1..xn] => t1|f) t2 = t1[x1..xn := a1..an]
provided 
    match p t2 = SOME(Match([(x1,a1)..(xn,an)],[]))
(that is the match is unconditionally successful) 

  ____________________________________________________________

    halts t2 |-  (fn p[x1..xn] => t1|f) t2 = f t2
provided 
    match p t2 = NONE
(that is the match is unsuccessful) 

  ____________________________________________________________

    halts t2, e1...em |-  (fn p[x1..xn] => t1|f) t2 = t1[x1..xn := a1..an],
    halts t2, not(e1)...not(em) |-  (fn p[x1..xn] => t1|f) t2 = f t2
when 
    match p t2 = SOME(Match([(x1,a1)..(xn,an)],[ e1...em]))

INSTANTIATE variable -> expression -> theorem -> theorem

                H |- t
        ___________________________

        halts e, H[v:=e] |- t[v:=e]
INSTANTIATE allows us to replace a free variable in a theorem by an expression. However we have to add the additional hypothesis that the evaluation of the expression halts.

Justification:

The input theorem says that for any type-correct mapping from its free variables to values under which all expressions of H evaluate to true, the expression t also evaluates to true. Now suppose we have an environment rho under which the expression e terminates normally, so that eval rho e is defined and 

eval rho g[v:=e] = true
Then 
eval rho g[v:=e] = eval rho[v:=eval e rho] g = true
for g in G. Hence 
eval rho t[v:=e] = eval rho[v:=eval e rho] t = true

Axioms

We regard axioms as being pre-defined theorems which express facts about an implementation of SML idealised in the sense that it implements the integers. Note that the axioms of our system are not minimal: rather than taking a reductionist stance, we regard our axioms as a convenient way of characterising how an idealised version of SML behaves.

We will use axioms subject to the instantiate rule, which, as you will recall, introduces a halting requirement when an expression is substituted for a variable.

The axioms for the members of the type int

The members of the type int form a commutative ring with identity

members of int form an abelian group 

I1      |-  x+y = y+x
I2      |-  x+(y+z) = (x+y)+z
I3      |-  x+0 = x
I4      |-  x+ (~x) = 0
I5      |-  x-y = x+(~y)

members of int form an abelian semi-group 

I6      |-  x*y = y*x
I7      |-  x*(y*z) = (x*y)*z
I8      |-  x*1 = x

to complete the ring axioms we have 

I9      |-  x*(y+z) = x*y + x*z
I10     |-  x*0 = 0
Note that I10 follows from the other axioms.

Note also that these ring axioms are not satisfied by any implementation of SML, for each axiom states that a particular computation will terminate normally. However, many implementations of SML will raise an overflow exception when asked, for example, to multiply a million by a million using integer arithmetic. Even implementations of SML such as POPLOG SML will run out of heap in attempting to perform computations on big enough integers.

Our system is complementary to the type-theory of SML. That is sound, but weak. Our system is, in the last analysis, only sound for a mathematically-ideal model of the language, but is logically much more powerful.

The members of the type int form an integral domain

I11   x*y = 0 |- x=0 orelse y=0

The members of the type int form a totally ordered set.

The axioms for them to form a partially-ordered set are: 
I12   x<=y, y<=x   |-   x=y
I13   |- x<=x
I14   |- x<=y, y<=z  |- x<=z
And to obtain total order, we add: 
I15  |- x<=y orelse y<=x

I16  |- x<=x+1

Induction over the integers and structures

Since structural induction can be used to shorten proofs, we support it as well as induction over the integers. The axiom of induction for the natural numbers has to be written as a proof-rule in our system. Now, SML does not have an explicit representation of the natrual numbers. We have two choices: we could construct them as a data-type, or we could regard them as a subset of the integers. Constructing them as a data-type has some advantages: it means that we are free to treat the -int- datatype in the way that most SML implementations treat it, as a fixed-precision representation of a subset of the integers.

However, working with user-defined natural numbers would be clumsy notationally, so we prefer to treat them as a subset of int. With this approach, the axiom of induction becomes: 

INDUCTION_int : (<'a> -> bool) -> theorem -> theorem -> theorem;


        H |- p 0              G, p(n) |- p(n+1)
       ________________________________________________

          0<=n, H |- p(n)
It should be noted that this form admits non-standard models of the integers.

Axioms and rules for lists.

We have a choice available here. Are we to include a structural-induction axiom for lists, or are we going to conduct all proofs about lists in terms of induction over the natural numbers? Structural induction is more convenient for many proofs. Moreover, if we don't have a rule for structural induction we will need an axiom which says that the length function is well-defined.

The list axioms are 

|- halts(x::l)
|- [] <> x::l

WRONG!!!
|- l = [] orelse l = hd(l)::tl(l)
|- hd(x::l) = x
|- tl(x::l) = l
 x1::l1 = x2::l2 |- x1=x2
 x1::l1 = x2::l2 |- l1=l2

INDUCTION_LIST (<list> -> <bool>) -> theorem -> theorem -> theorem 

H |- p []         H',  p l  |-  p x::l
______________________________________

       H union H' |- p l
Where x and l are not free in G.

What we can't talk about

Our system does not allow us to manipulate type expressions. So, for example, there is no way of saying in our system that the integers form a ring, for example: 
    Ring(int)
Neither can say, for example, that addition is commutative 
    commutative(op +)
We could get round this problem by introducing the notion of a generator. A generator g for a type T is a function g:int -> T which always returns an unspecified member of T (though of course, being a function, it always returns the same result for a given argument). With a generator, we could say: 
fun commutative f g
    f(g 1, g 2) = f(g 2, g 1);

The Halting Rules

The interpretation that we put upon halts(e) is that the expression e terminates without raising an exception. This, of course, rules out a treatment of programs which use exceptions "creatively", as a means of specifying what is regarded as the normal flow of control. 
    H |- t1 = t2
_____________________

   H |- halts t1

For f in { +,-,*,'<', '<=', '>', '>=',min,max,sign,sameSign,<> } 

    H1 |- halts(t1)      H2  halts(t2)
   ______________________________________

    H1 union H2 |-  halts f(t1,t2)



   H |- t2<>0     H1 |- halts(t1)       H2 |- halts(t2)
   _______________________________________________________

   H union H1 union H2 |-  halts t1 rem t2

Some Examples 

fun length [] = 0 | length(x::l) = 1 + length l;

Theorem

|- halts length l 
halts length [] |- halts length []                            ASSUME

halts (fn [] => 0
        | x::l => 1+length l) []      |- halts length []      LEFTDEF

|- halts []                                                   EVAL

halts [] |- (fn [] => 0 | x::l => 1+length l) [] = 0          BETA


 |- (fn [] => 0 | x::l => 1+length l) [] = 0                  MP


halts 0 |- halts length []                                    SUBST_LEFT

|- halts 0                                                    EVAL

|- halts length []                                            MP
Concluding the base case. 
halts(length(x::l)) |- halts(length(x::l))                    ASSUME

|- halts (x::l)                                               AXIOM

halts(x::l) |-  (fn [] = 0 | x::l => 1+length l) (x::l)
                    = 1+length l                              BETA

|-  (fn x::l => 1+length l) (x::l) = 1+length l               MP

halts (fn [] =>  0
        | (fn x::l => 1+length l) (x::l))
                |- halts(length (x::l))                       LEFTDEF


halts(1 + length l) |- halts(length(x::l))                    SUBST_LEFT

|- halts 1                                                    EVAL

|- halts (1+y)                                                SUBST

halts length l |- halts length l                              ASSUME

halts length l |- halts(1 + length l)                         SUBST

halts l |- halts(length(x::l))                                MP

|- halts l                                                    INDUCE_LIST
Quid Erat Demonstrandum

Theorem halts(a@b)

Proof: Base Case. We must try and show that halts([]@b). So let's assume it, and see if we can rid ourselves of the hypothesis. 

halts([]@b) |- halts([]@b)                                  ASSUME    (1)
If we unfold the halts on the left, we may be able to massage the resulting expression out of existence. 
halts(fn ([],b) => b
      | (a::l,b) => a::(l@b) ([],b) |- halts([]@b)          DEF_LEFT  (2)

halts ([],b) |-
    fn ([],b) => b | (a::l,b) => a::(l@b) ([],b) = b        BETA      (3)
So now we have to show that the expression ([],b) halts for every variable b. 
|- halts []                                                 EVAL_HALTS (4)

|- halts b                                                  HALTS_VAR  (5)

|- halts ([],b)                                             HALTS_PAIR (6)
We can now get rid of our halting condition by resolution with (3) 
|- (fn ([],b) => b | (a::l,b) => a::(l@b)) ([],b) = b       RESOLVE (7)
So let's use this equation to simplify the hypothesis of (2). 
halts b |- halts([]@b)                                      SUBST_LEFT (8)
And now we can trundle (5) into use, to obtain 
|- halts([]@b)                                                RESOLVE (9)
Which concludes our base case.

Inductive Step

We proceed in much the same way, assume what we want to prove, and try to massage the hypothesis, by unfolding it. 
halts(x::l@b) |- halts(x::l@b)                                ASSUME  (10)


halts(
  (fn ([],b) => b
      | (a::l,b) => a::(l@b))(x::l,b))
                    |- halts(x::l@b)                         DEF_LEFT (11)
And, as before, we'll apply BETA and get rid of the halting condition. 
halts(x::l,b) |-
    (fn ([],b) => b
      | (a::l,b) => a::(l@b)) (x::l,b) = x::(l@b)             BETA    (12)
But it's a rather more complicated halting condition. No matter, we can use the halting rules for cons and pair-creation. 
|- halts x                                                 HALTS_VAR (13)

|- halts l                                                 HALTS_VAR (14)

|- halts (x::l)                                            HALTS_CONS (15)

|- halts b                                                 HALTS_VAR  (16)

|- halts (x::l,b)                                          HALTS_PAIR (17)
Whence, resolution with (12) gets us: 
|- (fn ([],b) => b
      | (a::l,b) => a::(l@b)) (x::l,b) = x::(l@b)          RESOLVE (18)
We can now substitute back in (11), obtaining 
halts(x::(l@b)) |- halts(x::l@b)                           SUBST_LEFT (19)
And use the fact that list-construction halts 
halts(l@b) |- halts(l@b)                                   ASSUME (20)

|- halts x                                                 HALTS_VAR (21)

halts(l@b) |- halts(x::(l@b))                              HALTS_CONS (22)
Resolution now gains us what we need for structural induction: 
halts(l@b) |- halts((x::l)@b)                              RESOLVE (23)
So, finally, from induction on (9) and (23) we conclude: 
|- halts(l@b)                                              INDUCE_LIST (24)

Theorem

length(a@b) = length(a)+length(b)

Proof 

halts([]@b) |- length([]@b) = length([]@b)                 SYMMETRIC  (26)
By resolution with (9) above 
   |- length([]@b) = length([]@b)                          REDUCE (27)
Unfolding the right-hand call of @ 
   |- length([]@b) = length(fn ([],b) => b |
        (a::l,b) => a::(l@b)) ([],b))
.... Theorem length l = 0 ==> l = [] Proof Base Case [] = [] length [] = 0 sorted a, sorted b |- sorted(merge a b) length(a) + length(b) = 0 |- a = [] |- length(a)>=0 length(a) + length(b) = 0 |- length a + length b = 0 a>c, b>=d |- a+b>c+d x+y = 0, x>=0, y>=0 |- x=0 x>=0 |- x=0 orelse x>0

HOL Rules not Treated

Note that the Abstraction rule of HOL is not present in our system, because it introduces equality between functions, and this is not well typed in SML. We could introduce function-equality as a meta-construct like halts, but since we can always express f=g by saying that f x1...xn = g x1...xn we see no need to introduce this particular meta-construct.

The status of the INST_TYPE rule is not clear.

Type Correctness of Our Rules

Discussion

The axioms could be weaker.

Using patterns would make life a lot easier. 

bnd = matches patt arg, halts arg |-  (fn patt => e | rest)arg =  e[bnd]
matches p1 e1 [] = b1, matches p2 e2 b1 = b2 |- matches p1::p2 e1::e2 b2 NOTE The HOL manual has simultaneous substitution, of multiple variables, and I need to check the Meyer paper re. models of the lambda calculus on this matter.