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