MK_COMB : thm * thm -> thm

SYNOPSIS

Proves equality of combinations constructed from equal functions and operands.

DESCRIPTION

When applied to theorems A1 |- f = g and A2 |- x = y, the inference rule MK_COMB returns the theorem A1 u A2 |- f x = g y.

    A1 |- f = g   A2 |- x = y
   ---------------------------  MK_COMB
       A1 u A2 |- f x = g y

FAILURE CONDITIONS

Fails unless both theorems are equational and f and g are functions whose domain types are the same as the types of x and y respectively.

EXAMPLE

  # let th1 = ABS `n:num` (ARITH_RULE `SUC n = n + 1`)
    and th2 = NUM_REDUCE_CONV `2 + 2`;;
  val th1 : thm = |- (\n. SUC n) = (\n. n + 1)
  val th2 : thm = |- 2 + 2 = 4
  # let th3 = MK_COMB(th1,th2);;
  val th3 : thm = |- (\n. SUC n) (2 + 2) = (\n. n + 1) 4

  # let th1 = NOT_DEF and th2 = TAUT `p /\ p <=> p`;;
  val th1 : thm = |- (~) = (\p. p ==> F)
  val th2 : thm = |- p /\ p <=> p
  # MK_COMB(th1,th2);;
  val it : thm = |- ~(p /\ p) <=> (\p. p ==> F) p

COMMENTS

This is one of HOL Light's 10 primitive inference rules. It underlies, among other things, the replacement of subterms in rewriting.

SEE ALSO

AP_TERM, AP_THM, BETA_CONV, TRANS.