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
|
\DOC GSYM
\TYPE {GSYM : thm -> thm}
\SYNOPSIS
Reverses the first equation(s) encountered in a top-down search.
\KEYWORDS
rule, symmetry, equality.
\DESCRIBE
The inference rule {GSYM} reverses the first equation(s) encountered in a
top-down search of the conclusion of the argument theorem. An equation will be
reversed iff it is not a proper subterm of another equation. If a theorem
contains no equations, it will be returned unchanged.
{
A |- ..(s1 = s2)...(t1 = t2)..
-------------------------------- GSYM
A |- ..(s2 = s1)...(t2 = t1)..
}
\FAILURE
Never fails, and never loops infinitely.
\EXAMPLE
{
# ADD;;
val it : thm = |- (!n. 0 + n = n) /\ (!m n. SUC m + n = SUC (m + n))
# GSYM ADD;;
val it : thm = |- (!n. n = 0 + n) /\ (!m n. SUC (m + n) = SUC m + n)
}
\SEEALSO
REFL, SYM.
\ENDDOC
|
