/usr/share/hol88-2.02.19940316/help/ENTRIES/CHOOSE.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 | \DOC CHOOSE
\TYPE {CHOOSE : ((term # thm) -> thm -> thm)}
\SYNOPSIS
Eliminates existential quantification using deduction from a
particular witness.
\KEYWORDS
rule, existential.
\DESCRIBE
When applied to a term-theorem pair {(v,A1 |- ?x. s)} and a second
theorem of the form {A2 u {{s[v/x]}} |- t}, the inference rule {CHOOSE}
produces the theorem {A1 u A2 |- t}.
{
A1 |- ?x. s[x] A2 u {{s[v/x]}} |- t
--------------------------------------- CHOOSE ("v",(A1 |- ?x. s))
A1 u A2 |- t
}
\noindent Where {v} is not free in {A2} or {t}.
\FAILURE
Fails unless the terms and theorems correspond as indicated above; in
particular, 1) {v} must be a variable and have the same type as the variable
existentially quantified over, and it must not be free in {A2} or {t};
2) the second theorem must have {s[v/x]} in its assumptions.
\SEEALSO
CHOOSE_TAC, EXISTS, EXISTS_TAC, SELECT_ELIM.
\ENDDOC
|