equal: (2)

A conversion takes a term and
returns an equality theorem
with the term on the lhs (or it fails).

NO_CONV is a conversion which always fails.

# NO_CONV `0`;;
Exception: Failure "NO_CONV".

ALL_CONV is a conversion which always succeeds without changing the term.

# ALL_CONV `a`;;
Warning: inventing type variables
val it : thm = |- a = a

c1 THENC c2 rewrites with c1 then c2.

# (BETA_CONV THENC NUM_ADD_CONV) `(\x. 1+x) 2` ;;
val it : thm = |- (\x. 1 + x) 2 = 3

c1 ORELSEC c2 rewrites with c1;
if it fails, it rewrites with c2 instead.

# (NUM_SUB_CONV ORELSEC NUM_ADD_CONV) `1-1` ;;
val it : thm = |- 1 - 1 = 0
# (NUM_SUB_CONV ORELSEC NUM_ADD_CONV) `1+1` ;;
val it : thm = |- 1 + 1 = 2

FIRST_CONV [c1;...;cn] rewrites with
the first non-failing conversion in the list.
ORELSECのリスト版．

# FIRST_CONV [NUM_SUB_CONV;NUM_MULT_CONV;NUM_ADD_CONV;]`1*1`;;
val it : thm = |- 1 * 1 = 1

EVERY_CONV [c1;...;cn] rewrites with
the first conversion,
then the second, then ... then the last.
THENCのリスト版．

# EVERY_CONV [BETA_CONV;NUM_ADD_CONV]`(\x. x+2) 1`;;
val it : thm = |- (\x. x + 2) 1 = 3

REPEATC c
rewrites with c until it fails
(and returns the result of the
last successful rewrite).

# REPEATC BETA_CONV `(\x. (\y. x+2*y) x ) 1` ;;
val it : thm = |- (\x. (\y. x + 2 * y) x) 1 = 1 + 2 * 1

CHANGED_CONV c rewrites with c,
but fails if the result is
alpha-equivalent to the original term.

# CHANGED_CONV BETA_CONV `(\x. 1+x) 2`;;
val it : thm = |- (\x. 1 + x) 2 = 1 + 2
# CHANGED_CONV (ALPHA_CONV `y:num`) `(\x. 1+x)`;;
Exception: Failure "CHANGED_CONV".

TRY_CONV c rewrites with c;
if it fails, it does not change the term
(and does not fail).

# TRY_CONV BETA_CONV `(\x. 1+x) 2`;;
val it : thm = |- (\x. 1 + x) 2 = 1 + 2
# TRY_CONV BETA_CONV `(\x. 1+x)`;;
val it : thm = |- (\x. 1 + x) = (\x. 1 + x)

RATOR_CONV c uses the conversion
to rewrite the operator of a combination.

# rator `(\x. (\y. x+y) ) 1 2` ;;
val it : term = `(\x y. x + y) 1`
# RATOR_CONV BETA_CONV `(\x. (\y. x+y) ) 1 2` ;;
val it : thm = |- (\x y. x + y) 1 2 = (\y. 1 + y) 2

RAND_CONV c uses the conversion
to rewrite the operand of a combination.

# RAND_CONV NUM_ADD_CONV `(\x. 2*x ) (1+2)` ;;
val it : thm = |- (\x. 2 * x) (1 + 2) = (\x. 2 * x) 3
# RAND_CONV NUM_ADD_CONV `0+3=1+2` ;;
val it : thm = |- 0 + 3 = 1 + 2 <=> 0 + 3 = 3

LAND_CONV c uses the conversion
to rewrite the first argument of a binary function.

# LAND_CONV NUM_ADD_CONV `0+3=1+2` ;;
val it : thm = |- 0 + 3 = 1 + 2 <=> 3 = 1 + 2

COMB2_CONV c1 c2
uses c1 to rewrite the operator
and c2 to rewrite the operand of a combination.

# COMB2_CONV BETA_CONV NUM_ADD_CONV `(\x y. x+y) 1 (2+3)` ;;
val it : thm = |- (\x y. x + y) 1 (2 + 3) = (\y. 1 + y) 5

COMB_CONV c rewrites
both the operator and operand of a combination with c.

# rator `(\x y. x+y) 1 ((\z. 2+z) 3)`;;
val it : term = `(\x y. x + y) 1`
# rand `(\x y. x+y) 1 ((\z. 2+z) 3)`;;
val it : term = `(\z. 2 + z) 3`
# COMB_CONV BETA_CONV `(\x y. x+y) 1 ((\z. 2+z) 3)`;;
val it : thm = |- (\x y. x + y) 1 ((\z. 2 + z) 3) = (\y. 1 + y) (2 + 3)

ABS_CONV c rewrites
the body of an abstraction with c.

# ABS_CONV NUM_REDUCE_CONV `(\x. x+1+2)`;;
val it : thm = |- (\x. x + 1 + 2) = (\x. x + 3)

BINDER_CONV c rewrites
the body of an abstraction or
of a binder/abstraction combination.

# (ONCE_REWRITE_CONV[SWAP_FORALL_THM]) `(!x y z. x+y+z>=0)`;;
val it : thm = |- (!x y z. x + y + z >= 0) <=> (!y x z. x + y + z >= 0)
# BINDER_CONV(ONCE_REWRITE_CONV[SWAP_FORALL_THM]) `(!x y z. x+y+z>=0)`;;
val it : thm = |- (!x y z. x + y + z >= 0) <=> (!x z y. x + y + z >= 0)

SUB_CONV c
either rewrites both parts of a combination,
or the body of an abstraction,
or does nothing (it never fails).

# SUB_CONV NUM_REDUCE_CONV `(\x. x+1+2)`;;
val it : thm = |- (\x. x + 1 + 2) = (\x. x + 3)
# NUM_REDUCE_CONV (rator`0+3=1+2`);;
val it : thm = |- (=) (0 + 3) = (=) 3
# SUB_CONV NUM_REDUCE_CONV `0+3=1+2`;;
val it : thm = |- 0 + 3 = 1 + 2 <=> 3 = 3

BINOP_CONV c rewrites
both arguments of a binary function.

# BINOP_CONV NUM_ADD_CONV `(0+3)*(1+2)`;;
val it : thm = |- (0 + 3) * (1 + 2) = 3 * 3
# BINOP_CONV NUM_ADD_CONV `0+3=1+2`;;
val it : thm = |- 0 + 3 = 1 + 2 <=> 3 = 3