CHOOSE : term * thm -> thm -> thm

SYNOPSIS

Eliminates existential quantification using deduction from a particular witness.

DESCRIPTION

When applied to a term-theorem pair (v,A1 |- ?x. s) and a second theorem of the form A2 |- t, the inference rule CHOOSE produces the theorem A1 u (A2 - {s[v/x]}) |- t.

    A1 |- ?x. s[x]    A2 |- t
   -------------------------------  CHOOSE (`v`,(A1 |- ?x. s))
     A1 u (A2 - {s[v/x]}) |- t

Where v is not free in A2 - {s[v/x]}, s or t.

FAILURE CONDITIONS

Fails unless the terms and theorems correspond as indicated above; in particular, v must be a variable and have the same type as the variable existentially quantified over, and it must not be free in A2 - {s[v/x]}, s or t.

COMMENTS

For the special case of simply existentially quantifying an assumption over a variable, SIMPLE_CHOOSE is easier.