prove_constructors_injective : thm -> thm

SYNOPSIS

Proves that the constructors of an automatically-defined concrete type are injective.

DESCRIPTION

prove_constructors_one_one 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_one_one automatically proves and returns a theorem which states that the constructors of the concrete type in question are injective (one-to-one). The resulting theorem covers only those constructors that take arguments (i.e. that are not just constant values).

FAILURE CONDITIONS

Fails if the argument is not a theorem of the form returned by define_type, or if all the constructors of the concrete type in question are simply constants of that type.

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_injective:

  # prove_constructors_injective rth;;
  val it : thm =
    |- (!a a'. LEAF a = LEAF a' <=> a = a') /\
       (!a0 a1 a0' a1'. NODE a0 a1 = NODE a0' a1' <=> a0 = a0' /\ a1 = a1')

This states that the constructors LEAF and NODE are both injective.

COMMENTS

An easier interface is injectivity "tree"; the present function is mainly intended to generate that theorem internally.