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
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
\DOC X_CHOOSE_THEN
\TYPE {X_CHOOSE_THEN : (term -> thm_tactical)}
\SYNOPSIS
Replaces existentially quantified variable with given witness, and passes it to
a theorem-tactic.
\KEYWORDS
theorem-tactic, quantifier, existential.
\DESCRIBE
{X_CHOOSE_THEN} expects a variable {y}, a tactic-generating function
{f:thm->tactic}, and a theorem of the form {(A1 |- ?x. w)} as
arguments. A new theorem is created by introducing the given variable
{y} as a witness for the object {x} whose existence is asserted in the original
theorem, {(w[y/x] |- w[y/x])}. If the tactic-generating function {f}
applied to this theorem produces results as follows when applied to a
goal {(A ?- t)}:
{
A ?- t
========= f ({{w[y/x]}} |- w[y/x])
A ?- t1
}
\noindent then applying {(X_CHOOSE_THEN "y" f (A1 |- ?x. w))} to the
goal {(A ?- t)} produces the subgoal:
{
A ?- t
========= X_CHOOSE_THEN "y" f (A1 |- ?x. w)
A ?- t1 ("y" not free anywhere)
}
\FAILURE
Fails if the theorem's conclusion is not existentially quantified, or if
the first argument is not a variable. Failures may arise in the
tactic-generating function. An invalid tactic is produced if the
introduced variable is free in {w} or {t}, or if the theorem has any
hypothesis which is not alpha-convertible to an assumption of the
goal.
\EXAMPLE
Given a goal of the form
{
{{n < m}} ?- ?x. m = n + (x + 1)
}
\noindent the following theorem may be applied:
{
th = ["n < m"] |- ?p. m = n + p
}
\noindent by the tactic {(X_CHOOSE_THEN "q:num" SUBST1_TAC th)} giving
the subgoal:
{
{{n < m}} ?- ?x. n + q = n + (x + 1)
}
\SEEALSO
CHOOSE, CHOOSE_THEN, CONJUNCTS_THEN, CONJUNCTS_THEN2, DISJ_CASES_THEN,
DISJ_CASES_THEN2, DISJ_CASES_THENL, STRIP_THM_THEN, X_CHOOSE_TAC.
\ENDDOC
|
