1\DOC CHOOSE_TAC 2 3\TYPE {CHOOSE_TAC : thm_tactic} 4 5\SYNOPSIS 6Adds the body of an existentially quantified theorem to the assumptions of 7a goal. 8 9\KEYWORDS 10tactic, existential. 11 12\DESCRIBE 13When applied to a theorem {A' |- ?x. t} and a goal, {CHOOSE_TAC} adds 14{t[x'/x]} to the assumptions of the goal, where {x'} is a variant of 15{x} which is not free in the goal or assumption list; normally {x'} is 16just {x}. 17{ 18 A ?- u 19 ==================== CHOOSE_TAC (A' |- ?x. t) 20 A u {t[x'/x]} ?- u 21} 22Unless {A'} is a subset of {A}, this is not a valid tactic. 23 24\FAILURE 25Fails unless the given theorem is existentially quantified. 26 27\EXAMPLE 28Suppose we have a goal asserting that the output of an electrical circuit 29(represented as a boolean-valued function) will become high at some time: 30{ 31 ?- ?t. output(t) 32} 33and we have the following theorems available: 34{ 35 t1 = |- ?t. input(t) 36 t2 = !t. input(t) ==> output(t+1) 37} 38Then the goal can be solved by the application of: 39{ 40 CHOOSE_TAC th1 41 THEN EXISTS_TAC (Term `t+1`) 42 THEN UNDISCH_TAC (Term `input (t:num) :bool`) 43 THEN MATCH_ACCEPT_TAC th2 44} 45 46\COMMENTS 47To do similarly with several existentially quantified variables, use 48{REPEAT_TCL CHOOSE_THEN ASSUME_TAC} in place of {CHOOSE_TAC} 49 50\SEEALSO 51Thm_cont.CHOOSE_THEN, Tactic.X_CHOOSE_TAC, Thm_cont.REPEAT_TCL. 52\ENDDOC 53