X_CHOOSE_THEN : term -> thm_tactical

SYNOPSIS

Replaces existentially quantified variable with given witness, and passes it to a theorem-tactic.

DESCRIPTION

X_CHOOSE_THEN expects a variable y, a tactic-generating function ttac, 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 ttac applied to this theorem produces results as follows when applied to a goal (A ?- t):

    A ?- t
   =========  ttac ({w[y/x]} |- w[y/x])
    A ?- t1

then applying (X_CHOOSE_THEN `y` ttac (A1 |- ?x. w)) to the goal (A ?- t) produces the subgoal:

    A ?- t
   =========  X_CHOOSE_THEN `y` ttac (A1 |- ?x. w)
    A ?- t1         (`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

Suppose we have the following goal:

  # g `!m n. m < n ==> m EXP 2 + 2 * m <= n EXP 2`;;

and rewrite with a theorem to get an existential antecedent:

  # e(REPEAT GEN_TAC THEN REWRITE_TAC[LT_EXISTS]);;
  val it : goalstack = 1 subgoal (1 total)

`(?d. n = m + SUC d) ==> m EXP 2 + 2 * m <= n EXP 2`

we may then use X_CHOOSE_THEN to introduce the name e for the existential variable and immediately substitute it in the goal:

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

  `m EXP 2 + 2 * m <= (m + SUC e) EXP 2`

at which point ARITH_TAC will finish it.