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 GSUBST_TAC
\TYPE {GSUBST_TAC : (((term # term) list -> term -> term) -> thm list -> tactic)}
\SYNOPSIS
Makes term substitutions in a goal using a supplied substitution function.
\KEYWORDS
tactic, genvars.
\DESCRIBE
{GSUBST_TAC} is the basic substitution tactic by means of which other tactics
such as {SUBST_OCCS_TAC} and {SUBST_TAC} are defined. Given a list
{[(v1,w1);...;(vk,wk)]} of pairs of terms and a term {w}, a substitution
function replaces occurrences of {wj} in {w} with {vj} according to a specific
substitution criterion. Such a criterion may be, for example, to substitute all
the occurrences or only some selected ones of each {wj} in {w}.
Given a substitution function {sfn}, {GSUBST_TAC sfn [A1|-t1=u1;...;An|-tn=un]
(A,t)} replaces occurrences of {ti} in {t} with {ui} according to {sfn}.
{
A ?- t
============================= GSUBST_TAC sfn [A1|-t1=u1;...;An|-tn=un]
A ?- t[u1,...,un/t1,...,tn]
}
\noindent The assumptions of the theorems used to substitute with are not added
to the assumptions {A} of the goal, while they are recorded in the proof. If
any {Ai} is not a subset of {A} (up to alpha-conversion), then {GSUBST_TAC sfn
[A1|-t1=u1;...;An|-tn=un]} results in an invalid tactic.
{GSUBST_TAC} automatically renames bound variables to prevent free variables in
{ui} becoming bound after substitution.
\FAILURE
{GSUBST_TAC sfn [th1;...;thn] (A,t)} fails if the conclusion of each theorem in
the list is not an equation. No change is made to the goal if the occurrences
to be substituted according to the substitution function {sfn} do not appear in
{t}.
\USES
{GSUBST_TAC} is used to define substitution tactics such as {SUBST_OCCS_TAC}
and {SUBST_TAC}. It may also provide the user with a tool for tailoring
substitution tactics.
\SEEALSO
SUBST1_TAC, SUBST_OCCS_TAC, SUBST_TAC.
\ENDDOC
|
