1\DOC CHOOSE_THEN 2 3\TYPE {CHOOSE_THEN : thm_tactical} 4 5\SYNOPSIS 6Applies a tactic generated from the body of existentially quantified theorem. 7 8\KEYWORDS 9theorem-tactic, existential. 10 11\DESCRIBE 12When applied to a theorem-tactic {ttac}, an existentially quantified 13theorem {A' |- ?x. t}, and a goal, {CHOOSE_THEN} applies the tactic 14{ttac (t[x'/x] |- t[x'/x])} to the goal, where {x'} is a variant of 15{x} chosen not to be free in the assumption list of the goal. Thus if: 16{ 17 A ?- s1 18 ========= ttac (t[x'/x] |- t[x'/x]) 19 B ?- s2 20} 21then 22{ 23 A ?- s1 24 ========== CHOOSE_THEN ttac (A' |- ?x. t) 25 B ?- s2 26} 27This is invalid unless {A'} is a subset of {A}. 28 29\FAILURE 30Fails unless the given theorem is existentially quantified, or if the 31resulting tactic fails when applied to the goal. 32 33\EXAMPLE 34This theorem-tactical and its relatives are very useful for using existentially 35quantified theorems. For example one might use the inbuilt theorem 36{ 37 LESS_ADD_1 = |- !m n. n < m ==> (?p. m = n + (p + 1)) 38} 39to help solve the goal 40{ 41 ?- x < y ==> 0 < y * y 42} 43by starting with the following tactic 44{ 45 DISCH_THEN (CHOOSE_THEN SUBST1_TAC o MATCH_MP LESS_ADD_1) 46} 47which reduces the goal to 48{ 49 ?- 0 < ((x + (p + 1)) * (x + (p + 1))) 50} 51which can then be finished off quite easily, by, for example: 52{ 53 REWRITE_TAC[ADD_ASSOC, SYM (SPEC_ALL ADD1), 54 MULT_CLAUSES, ADD_CLAUSES, LESS_0] 55} 56 57 58\SEEALSO 59Tactic.CHOOSE_TAC, Thm_cont.X_CHOOSE_THEN. 60\ENDDOC 61