1\DOC CHANGED_CONV
2
3\TYPE {CHANGED_CONV : (conv -> conv)}
4
5\SYNOPSIS
6Makes a conversion fail if applying it leaves a term unchanged.
7
8\KEYWORDS
9conversional.
10
11\DESCRIBE
12If {c} is a conversion that maps a term {``t``} to a theorem {|- t = t'},
13where {t'} is alpha-equivalent to {t}, or if {c} raises the
14{UNCHANGED} exception when applied to {``t``}, then {CHANGED_CONV c}
15is a conversion that fails when applied to the term {``t``}. If {c}
16maps {``t``} to {|- t = t'}, where {t'} is not alpha-equivalent to
17{t}, then {CHANGED_CONV c} also maps {``t``} to {|- t = t'}. That is,
18{CHANGED_CONV c} is the conversion that behaves exactly like {c},
19except that it fails whenever the conversion {c} would leave its input
20term unchanged (up to alpha-equivalence).
21
22When {CHANGED_CONV c t} fails, it raises an exception {HOL_ERR ...},
23not {UNCHANGED}, since some enclosing functions handle the 
24{UNCHANGED} exception as though {c} had succeeded by returning
25the theorem {|- t = t}.
26
27\FAILURE
28{CHANGED_CONV c ``t``} fails if {c} maps {``t``} to {|- t = t'}, where
29{t'} is alpha-equivalent to {t}, or if {c} raises the {UNCHANGED}
30exception when applied to {``t``}, or if {c} fails when applied to
31{``t``}.  The function returned by {CHANGED_CONV c} may also fail if
32the ML function {c:term->thm} is not, in fact, a conversion (i.e. a
33function that maps a term {t} to a theorem {|- t = t'}).
34
35\USES
36{CHANGED_CONV} is used to transform a conversion that may leave terms
37unchanged, and therefore may cause a nonterminating computation if
38repeated, into one that can safely be repeated until application of it
39fails to substantially modify its input term.
40
41\SEEALSO
42Conv.UNCHANGED, Conv.QCHANGED_CONV.
43
44\ENDDOC
45