AP_TERM : term -> thm -> thm

SYNOPSIS

Applies a function to both sides of an equational theorem.

DESCRIPTION

When applied to a term f and a theorem A |- x = y, the inference rule AP_TERM returns the theorem A |- f x = f y.

      A |- x = y
   ----------------  AP_TERM `f`
    A |- f x = f y

FAILURE CONDITIONS

Fails unless the theorem is equational and the supplied term is a function whose domain type is the same as the type of both sides of the equation.

EXAMPLE

  # NUM_ADD_CONV `2 + 2`;;
  val it : thm = |- 2 + 2 = 4

  # AP_TERM `(+) 1` it;;
  val it : thm = |- 1 + 2 + 2 = 1 + 4

SEE ALSO

AP_THM, MK_COMB.