1\DOC X_CHOOSE_THEN 2 3\TYPE {X_CHOOSE_THEN : (term -> thm_tactical)} 4 5\SYNOPSIS 6Replaces existentially quantified variable with given witness, and passes it to 7a theorem-tactic. 8 9\KEYWORDS 10theorem-tactic, quantifier, existential. 11 12\DESCRIBE 13{X_CHOOSE_THEN} expects a variable {y}, a tactic-generating function 14{f:thm->tactic}, and a theorem of the form {(A1 |- ?x. w)} as 15arguments. A new theorem is created by introducing the given variable 16{y} as a witness for the object {x} whose existence is asserted in the original 17theorem, {(w[y/x] |- w[y/x])}. If the tactic-generating function {f} 18applied to this theorem produces results as follows when applied to a 19goal {(A ?- t)}: 20{ 21 A ?- t 22 ========= f ({w[y/x]} |- w[y/x]) 23 A ?- t1 24} 25then applying {(X_CHOOSE_THEN "y" f (A1 |- ?x. w))} to the 26goal {(A ?- t)} produces the subgoal: 27{ 28 A ?- t 29 ========= X_CHOOSE_THEN y f (A1 |- ?x. w) 30 A ?- t1 (y not free anywhere) 31} 32 33 34\FAILURE 35Fails if the theorem's conclusion is not existentially quantified, or 36if the first argument is not a variable. Failures may arise in the 37tactic-generating function. An invalid tactic is produced if the 38introduced variable is free in {w}, {t} or {A}, or if the theorem has 39any hypothesis which is not alpha-convertible to an assumption of the 40goal. 41 42\EXAMPLE 43Given a goal of the form 44{ 45 {n < m} ?- ?x. m = n + (x + 1) 46} 47the following theorem may be applied: 48{ 49 th = [n < m] |- ?p. m = n + p 50} 51by the tactic {(X_CHOOSE_THEN (Term`q:num`) SUBST1_TAC th)} giving 52the subgoal: 53{ 54 {n < m} ?- ?x. n + q = n + (x + 1) 55} 56 57 58\SEEALSO 59Thm.CHOOSE, Thm_cont.CHOOSE_THEN, Thm_cont.CONJUNCTS_THEN, Thm_cont.CONJUNCTS_THEN2, Thm_cont.DISJ_CASES_THEN, Thm_cont.DISJ_CASES_THEN2, Thm_cont.DISJ_CASES_THENL, Thm_cont.STRIP_THM_THEN, Tactic.X_CHOOSE_TAC. 60\ENDDOC 61