X_CHOOSE_TAC : term -> thm_tactic

SYNOPSIS

Assumes a theorem, with existentially quantified variable replaced by a given witness.

DESCRIPTION

X_CHOOSE_TAC expects a variable y and theorem with an existentially quantified conclusion. When applied to a goal, it adds a new assumption obtained by introducing the variable y as a witness for the object x whose existence is asserted in the theorem.

           A ?- t
   ===================  X_CHOOSE_TAC `y` (A1 |- ?x. w)
    A u {w[y/x]} ?- t         (`y` not free anywhere)

FAILURE CONDITIONS

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:

  # g `(?y. x = y + 2) ==> x < x * x`;;

the following may be applied:

  # e(DISCH_THEN(X_CHOOSE_TAC `d:num`));;
  val it : goalstack = 1 subgoal (1 total)

   0 [`x = d + 2`]

  `x < x * x`

after which the following will finish things:

  # e(ASM_REWRITE_TAC[] THEN ARITH_TAC);;
  val it : goalstack = No subgoals

SEE ALSO

CHOOSE, CHOOSE_THEN, X_CHOOSE_THEN.