Drule.prove_abs_fn_one

prove_abs_fn_one_one : thm -> thm

STRUCTURE

Drule

SYNOPSIS

Proves that a type abstraction function is one-to-one (injective).

DESCRIPTION

If th is a theorem of the form returned by the function define_new_type_bijections:

   |- (!a. abs(rep a) = a) /\ (!r. P r = (rep(abs r) = r))

then prove_abs_fn_one_one th proves from this theorem that the function abs is one-to-one for values that satisfy P, returning the theorem:

   |- !r r'. P r ==> P r' ==> ((abs r = abs r') = (r = r'))

FAILURE

Fails if applied to a theorem not of the form shown above.

SEEALSO

HOL Kananaskis-13