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
|
\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
{
?- m = 0 + m
}
\noindent assuming the clauses for addition with
{STRIP_ASSUME_TAC ADD_CLAUSES} results in the goal
{
{{m + (SUC n) = SUC(m + n), (SUC m) + n = SUC(m + n),
m + 0 = m, 0 + m = m, m = 0 + m}} ?- m = 0 + m
}
\noindent while the same tactic directly solves the goal
{
?- 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 resolution, 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
|
