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
|
\DOC CLAIM_TAC
\TYPE {CLAIM_TAC : string -> term -> tactic}
\SYNOPSIS
Breaks down and labels an intermediate claim in a proof.
\DESCRIBE
Given a Boolean term {t} and a string {s} of the form expected by
{DESTRUCT_TAC} indicating how to break down and label that assertion,
{CLAIM_TAC s t} breaks the current goal into two or more subgoals. One of
these is to establish {t} using the current context and the others are to
establish the original goal with the broken-down form of {t} as additional
assumptions.
\FAILURE
Fails if the term is not Boolean or the pattern is ill-formed or does not match
the form of the theorem.
\EXAMPLE
Here we show how we can attack a propositional goal (admittedly trivial with
{TAUT}).
{
# g `(p <=> q) ==> p \/ ~q`;;
val it : goalstack = 1 subgoal (1 total)
`(p <=> q) ==> p \/ ~q`
# e DISCH_TAC;;
val it : goalstack = 1 subgoal (1 total)
0 [`p <=> q`]
`p \/ ~q`
}
We establish the intermediate goal {p /\ q \/ ~p /\ ~q}, the disjunction being
in turn broken down into two labelled hypotheses {yes} and {no}:
{
# e(CLAIM_TAC "yes|no" `p /\ q \/ ~p /\ ~q`);;
val it : goalstack = 3 subgoals (3 total)
0 [`p <=> q`]
1 [`~p /\ ~q`] (no)
`p \/ ~q`
0 [`p <=> q`]
1 [`p /\ q`] (yes)
`p \/ ~q`
0 [`p <=> q`]
`p /\ q \/ ~p /\ ~q`
}
\SEEALSO
DESTRUCT_TAC, SUBGOAL_TAC, SUBGOAL_THEN.
\ENDDOC
|
