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
|
\DOC ONCE_ASM_REWRITE_TAC
\TYPE {ONCE_ASM_REWRITE_TAC : (thm list -> tactic)}
\SYNOPSIS
Rewrites a goal once including built-in rewrites and the goal's assumptions.
\KEYWORDS
tactic.
\DESCRIBE
{ONCE_ASM_REWRITE_TAC} behaves in the same way as {ASM_REWRITE_TAC},
but makes one pass only through the term of the goal. The order in
which the given theorems are applied is an implementation matter and
the user should not depend on any ordering. See {GEN_REWRITE_TAC} for
more information on rewriting a goal in HOL.
\FAILURE
{ONCE_ASM_REWRITE_TAC} does not fail and, unlike {ASM_REWRITE_TAC},
does not diverge. The resulting tactic may not be valid, if the
rewrites performed add new assumptions to the theorem eventually
proved.
\EXAMPLE
The use of {ONCE_ASM_REWRITE_TAC} to control the amount of rewriting
performed is illustrated below:
{
#ONCE_ASM_REWRITE_TAC []
# (["(a:*) = b"; "(b:*) = c"], "P (a:*): bool") ;;
([(["a = b"; "b = c"], "P b")], -) : subgoals
}
{
#(ONCE_ASM_REWRITE_TAC [] THEN ONCE_ASM_REWRITE_TAC [])
# (["(a:*) = b"; "(b:*) = c"], "P (a:*): bool") ;;
([(["a = b"; "b = c"], "P c")], -) : subgoals
}
\USES
{ONCE_ASM_REWRITE_TAC} can be applied once or iterated as required to
give the effect of {ASM_REWRITE_TAC}, either to avoid divergence or to
save inference steps.
\SEEALSO
basic_rewrites, ASM_REWRITE_TAC, FILTER_ASM_REWRITE_TAC,
FILTER_ONCE_ASM_REWRITE_TAC, GEN_REWRITE_TAC, ONCE_ASM_REWRITE_TAC,
ONCE_REWRITE_TAC, PURE_ASM_REWRITE_TAC, PURE_ONCE_ASM_REWRITE_TAC,
PURE_ONCE_REWRITE_TAC, PURE_REWRITE_TAC, REWRITE_TAC, SUBST_TAC.
\ENDDOC
|
