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
|
\DOC STRIP_ASSUME_TAC
\TYPE {STRIP_ASSUME_TAC : thm_tactic}
\SYNOPSIS
Splits a theorem into a list of theorems and then adds them to the assumptions.
\KEYWORDS
tactic.
\DESCRIBE
Given a theorem {th} and a goal {(A,t)}, {STRIP_ASSUME_TAC th} splits {th} into
a list of theorems. This is done by recursively breaking conjunctions into
separate conjuncts, cases-splitting disjunctions, and eliminating existential
quantifiers by choosing arbitrary variables. Schematically, the following
rules are applied:
{
A ?- t
====================== STRIP_ASSUME_TAC (A' |- v1 /\ ... /\ vn)
A u {{v1,...,vn}} ?- t
A ?- t
================================= STRIP_ASSUME_TAC (A' |- v1 \/ ... \/ vn)
A u {{v1}} ?- t ... A u {{vn}} ?- t
A ?- t
==================== STRIP_ASSUME_TAC (A' |- ?x.v)
A u {{v[x'/x]}} ?- t
}
\noindent where {x'} is a variant of {x}.
If the conclusion of {th} is not a conjunction, a disjunction or an
existentially quantified term, the whole theorem {th} is added to the
assumptions.
As assumptions are generated, they are examined to see if they solve the goal
(either by being alpha-equivalent to the conclusion of the goal or by deriving
a contradiction).
The assumptions of the theorem being split are not added to the assumptions of
the goal(s), but they are recorded in the proof. This means that if {A'} is
not a subset of the assumptions {A} of the goal (up to alpha-conversion),
{STRIP_ASSUME_TAC (A' |- v)} results in an invalid tactic.
\FAILURE
Never fails.
\EXAMPLE
When solving the goal
{
# g `m = 0 + m`;;
}
\noindent assuming the clauses for addition with
{STRIP_ASSUME_TAC ADD_CLAUSES} results in the goal
{
# e(STRIP_ASSUME_TAC ADD_CLAUSES);;
val it : goalstack = 1 subgoal (1 total)
0 [`!n. 0 + n = n`]
1 [`!m. m + 0 = m`]
2 [`!m n. SUC m + n = SUC (m + n)`]
3 [`!m n. m + SUC n = SUC (m + n)`]
`m = 0 + m`
}
\noindent while the same tactic directly solves the goal
{
?- !m. 0 + m = m
}
\USES
{STRIP_ASSUME_TAC} is used when applying a previously proved theorem to solve a
goal, or when enriching its assumptions so that rewriting with assumptions and
other operations involving assumptions have more to work with.
\SEEALSO
ASSUME_TAC, CHOOSE_TAC, CHOOSE_THEN, CONJUNCTS_THEN, DISJ_CASES_TAC,
DISJ_CASES_THEN.
\ENDDOC
|
