equal: (4)

SYM_CONV rewrites `a = b` to `b = a`

# SYM_CONV `0=1`;;
val it : thm = |- 0 = 1 <=> 1 = 0
# SYM (ARITH_RULE `0+1=1`);;
val it : thm = |- 1 = 0 + 1
# SYM (ARITH_RULE `!m. m*0=0`);;
Exception: Failure "dest_eq".

CONV_RULE c th
uses c to rewrite the conclusion of the theorem
(and return a new theorem).

# CONV_RULE (BINOP_CONV NUM_REDUCE_CONV) (ARITH_RULE`1+2<3+4`);;
val it : thm = |- 3 < 7

SUBS_CONV ths is a conversion. It takes its list of equality theorems and rewrites (anywhere in its argument term) any lhs to its corresponding rhs (matching with alpha-equivalence).

# SUBS_CONV [ARITH_RULE`x+y=y+x`] `x+1`;;
val it : thm = |- x + 1 = x + 1
# ALPHA `x+y+x+y` `x+(y+(x+y))`;;
val it : thm = |- x + y + x + y = x + y + x + y
# SUBS_CONV [ARITH_RULE`x+y=y+x`]`x+y+x+y`;;
val it : thm = |- x + y + x + y = x + y + y + x

BETA_RULE takes a theorem,
does all possible beta reductions,
and returns the new theorem.

# ARITH_RULE`(\x y. 1+x y) (\z. 2+z) 3=6`;;
val it : thm = |- (\x y. 1 + x y) (\z. 2 + z) 3 = 6
# BETA_RULE it;;
val it : thm = |- 1 + 2 + 3 = 6

GSYM applies symmetry on
all outermost equalities in the conclusion of a theorem.

# GSYM (ARITH_RULE`(!n. n*0=0) /\ (!n. n*1=n)`);;
val it : thm = |- (!n. 0 = n * 0) /\ (!n. n = n * 1)

SUBS applies SUBS_CONV
to the conclusion of a theorem.

# SUBS [ARITH_RULE`x+y=y+x:num`] (ARITH_RULE`y+x=0+x+y`);;
val it : thm = |- y + x = 0 + y + x

CACHE_CONV c is equivalent to c,
except that it caches all conversion applications.

# time (DEPTH_CONV(NUM_RED_CONV))
`31 EXP 31 + 31 EXP 31 + 31 EXP 31`;;
CPU time (user): 0.036664
val it : thm =
|- 31 EXP 31 + 31 EXP 31 + 31 EXP 31 =
51207522392169707875831929087177944268134203293
# time (DEPTH_CONV(CACHE_CONV NUM_RED_CONV))
`31 EXP 31 + 31 EXP 31 + 31 EXP 31`;;
CPU time (user): 0.013333
val it : thm =
|- 31 EXP 31 + 31 EXP 31 + 31 EXP 31 =
51207522392169707875831929087177944268134203293