1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
|
\DOC INTRO_TAC
\TYPE {INTRO_TAC : string -> tactic}
\SYNOPSIS
Breaks down outer quantifiers in goal, introducing variables and named
hypotheses.
\DESCRIBE
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:
\begin{{itemize}}
\item {! fix_pattern} introduces universally quantified variables as with
{FIX_TAC}
\item a destruct pattern introduces and destructs an implication as with
{DESTRUCT_TAC}
\item {#n} selects disjunct {n} in the goal
\end{{itemize}}
Several fix patterns and destruct patterns can be combined sequentially,
separed by semicolons `;'.
\FAILURE
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'`
}
\SEEALSO
DESTRUCT_TAC, DISCH_TAC, FIX_TAC, GEN_TAC, LABEL_TAC, REMOVE_THEN,
STRIP_TAC, USE_THEN.
\ENDDOC
|
