PCHOOSE : term * thm -> thm -> thm

- STRUCTURE
- LIBRARY
- pair
- SYNOPSIS
- Eliminates paired existential quantification using deduction from a particular witness.
- DESCRIPTION
- When applied to a term-theorem pair (q,A1 |- ?p. s) and a second theorem of the form A2 u {s[q/p]} |- t, the inference rule PCHOOSE produces the theorem A1 u A2 |- t.Where no variable in the paired variable structure q is free in A1, A2 or t.
A1 |- ?p. s A2 u {s[q/p]} |- t ------------------------------------ PCHOOSE ("q",(A1 |- ?q. s)) A1 u A2 |- t

- FAILURE
- Fails unless the terms and theorems correspond as indicated above; in particular q must have the same type as the pair existentially quantified over, and must not contain any variable free in A1, A2 or t.
- SEEALSO

HOL Kananaskis-14