PROVE_HYP : thm -> thm -> thm

SYNOPSIS

Eliminates a provable assumption from a theorem.

DESCRIPTION

When applied to two theorems, PROVE_HYP gives a new theorem with the conclusion of the second and the union of the assumption list minus the conclusion of the first theorem.

     A1 |- t1     A2 |- t2
   -------------------------  PROVE_HYP
     A1 u (A2 - {t1}) |- t2

If t1 does not occurr in A2 then the function simply returns the second theorem A2 |- t2 unchanged without including the assumptions A1.

FAILURE CONDITIONS

Never fails.

EXAMPLE

  # let th1 = CONJUNCT2(ASSUME `p /\ q /\ r`)
    and th2 = CONJUNCT2(ASSUME `q /\ r`);;
  val th1 : thm = p /\ q /\ r |- q /\ r
  val th2 : thm = q /\ r |- r

  # PROVE_HYP th1 th2;;
  val it : thm = p /\ q /\ r |- r

COMMENTS

This is sometimes known as the Cut rule. Although it is not necessary for the conclusion of the first theorem to be the same as an assumption of the second, PROVE_HYP is otherwise of doubtful value.