GEN : term -> thm -> thm

SYNOPSIS

Generalizes the conclusion of a theorem.

DESCRIPTION

When applied to a term x and a theorem A |- t, the inference rule GEN returns the theorem A |- !x. t, provided x is a variable not free in any of the assumptions. There is no compulsion that x should be free in t.

      A |- t
   ------------  GEN `x`                [where x is not free in A]
    A |- !x. t

FAILURE CONDITIONS

Fails if x is not a variable, or if it is free in any of the assumptions.

EXAMPLE

This is a basic example:

  # GEN `x:num` (REFL `x:num`);;
  val it : thm = |- !x. x = x

while the following example shows how the above side-condition prevents the derivation of the theorem x <=> T |- !x. x <=> T, which is invalid.

  # let t = ASSUME `x <=> T`;;
  val t : thm = x <=> T |- x <=> T

  # GEN `x:bool` t;;
  Exception: Failure "GEN".