prove_constructors_distinct : thm -> thm

SYNOPSIS

Proves that the constructors of an automatically-defined concrete type yield distinct values.

DESCRIPTION

prove_constructors_distinct takes as its argument a primitive recursion theorem, in the form returned by define_type for an automatically-defined concrete type. When applied to such a theorem, prove_constructors_distinct automatically proves and returns a theorem which states that distinct constructors of the concrete type in question yield distinct values of this type.

FAILURE CONDITIONS

Fails if the argument is not a theorem of the form returned by define_type, or if the concrete type in question has only one constructor.

EXAMPLE

The following type definition for labelled binary trees:

  # let ith,rth = define_type "tree = LEAF num | NODE tree tree";;
  val ith : thm =
    |- !P. (!a. P (LEAF a)) /\ (!a0 a1. P a0 /\ P a1 ==> P (NODE a0 a1))
           ==> (!x. P x)
  val rth : thm =
    |- !f0 f1.
           ?fn. (!a. fn (LEAF a) = f0 a) /\
                (!a0 a1. fn (NODE a0 a1) = f1 a0 a1 (fn a0) (fn a1))

returns a recursion theorem rth that can then be fed to prove_constructors_distinct:

  # prove_constructors_distinct rth;;
  val it : thm = |- !a a0' a1'. ~(LEAF a = NODE a0' a1')

This states that leaf nodes are different from internal nodes. When the concrete type in question has more than two constructors, the resulting theorem is just conjunction of inequalities of this kind.

COMMENTS

An easier interface is distinctness "tree"; this function is mainly intended to generate that theorem internally.