INTRO_TAC : string -> tactic

SYNOPSIS

Breaks down outer quantifiers in goal, introducing variables and named hypotheses.

DESCRIPTION

Given a string s, INTRO_TAC s breaks down outer universal quantifiers and implications in the goal, fixing variables and introducing assumptions with names. It combines several forms of introduction of logical connectives. The introduction pattern uses the following syntax:

! fix_pattern introduces universally quantified variables as with FIX_TAC
a destruct pattern introduces and destructs an implication as with DESTRUCT_TAC
#n selects disjunct n in the goal

Several fix patterns and destruct patterns can be combined sequentially, separed by semicolons `;'.

FAILURE CONDITIONS

Fails if the pattern is ill-formed or does not match the form of the goal.

EXAMPLE

Here we introduce the universally quantified outer variables, assume the antecedent, splitting apart conjunctions and disjunctions:

  # g `!p q r. p \/ (q /\ r) ==> p /\ q \/ p /\ r`;;
  # e (INTRO_TAC "!p q r; p | q r");;
  val it : goalstack = 2 subgoals (2 total)

    0 [`q`] (q)
    1 [`r`] (r)

  `p /\ q \/ p /\ r`

    0 [`p`] (p)

  `p /\ q \/ p /\ r`

Now a further step will select the first disjunct to prove in the top goal:

  # e (INTRO_TAC "#1");;
  val it : goalstack = 1 subgoal (2 total)

    0 [`p`] (p)

  `p /\ q`

In the next example we introduce an alternation of universally quantified variables and antecedents. Along the way we split a disjunction and rename variables x1, x2 into n, n'. All is done in a single tactic invocation.

  # g `!a. ~(a = 0) ==> ONE_ONE (\n. a * n)`;;
  # e (REWRITE_TAC[ONE_ONE; EQ_MULT_LCANCEL]);;
  val it : goalstack = 1 subgoal (1 total)

  `!a. ~(a = 0) ==> (!x1 x2. a = 0 \/ x1 = x2 ==> x1 = x2)`

  # e (INTRO_TAC "!a; anz; ![n] [n']; az | eq");;
  val it : goalstack = 2 subgoals (2 total)

    0 [`~(a = 0)`] (anz)
    1 [`n = n'`] (eq)

  `n = n'`

    0 [`~(a = 0)`] (anz)
    1 [`a = 0`] (az)

  `n = n'`