1\DOC GEN_REWRITE_CONV 2 3\TYPE {GEN_REWRITE_CONV : ((conv -> conv) -> rewrites -> thm list -> conv)} 4 5\SYNOPSIS 6Rewrites a term, selecting terms according to a user-specified strategy. 7 8\KEYWORDS 9conversion. 10 11\DESCRIBE 12Rewriting in HOL is based on the use of equational theorems as left-to-right 13replacements on the subterms of an object theorem. This replacement is 14mediated by the use of {REWR_CONV}, which finds matches between left-hand 15sides of given equations in a term and applies the substitution. 16 17Equations used in rewriting are obtained from the theorem lists given as 18arguments to the function. These are at first transformed into a form suitable 19for rewriting. Conjunctions are separated into individual rewrites. Theorems 20with conclusions of the form {"~t"} are transformed into the corresponding 21equations {"t = F"}. Theorems {"t"} which are not equations are cast as 22equations of form {"t = T"}. 23 24If a theorem is used to rewrite a term, its assumptions 25are added to the assumptions of the returned theorem. 26The matching involved uses variable instantiation. 27Thus, all free variables are generalized, and 28terms are instantiated before substitution. 29Theorems may have universally quantified variables. 30 31The theorems with which rewriting is done are divided 32into two groups, to facilitate implementing other rewriting tools. 33However, they are considered in an order-independent fashion. (That 34is, the ordering is an implementation detail which is not specified.) 35 36The search strategy for finding matching subterms is the first 37argument to the rule. Matching and substitution may occur at any 38level of the term, according to the specified search strategy: the 39whole term, or starting from any subterm. The search strategy also 40specifies the depth of the search: recursively up to an arbitrary 41depth until no matches occur, once over the selected subterm, or any 42more complex scheme. 43 44\FAILURE 45{GEN_REWRITE_CONV} fails if the search strategy fails. It may also 46cause a non-terminating sequence of rewrites, depending on the search 47strategy used. 48 49\USES 50This conversion is used in the system to implement all other rewritings 51conversions, and may provide a user with a method to fine-tune rewriting of 52terms. 53 54\EXAMPLE 55Suppose we have a term of the form: 56{ 57 "(1 + 2) + 3 = (3 + 1) + 2" 58} 59and we would like to rewrite the left-hand side with the 60theorem {ADD_SYM} without changing the right hand side. This can be 61done by using: 62{ 63 GEN_REWRITE_CONV (RATOR_CONV o ONCE_DEPTH_CONV) empty_rewrites [ADD_SYM] mythm 64} 65Other rules, such as {ONCE_REWRITE_CONV}, would match and 66substitute on both sides, which would not be the desirable result. 67 68As another example, {REWRITE_CONV} could be implemented as 69{ 70 GEN_REWRITE_CONV TOP_DEPTH_CONV (implicit_rewrites()) 71} 72which specifies that matches should be searched recursively 73starting from the whole term of the theorem, and {implicit_rewrites} must 74be added to the user defined set of theorems employed in rewriting. 75 76\SEEALSO 77Rewrite.ONCE_REWRITE_CONV, Rewrite.PURE_REWRITE_CONV, Conv.REWR_CONV, Rewrite.REWRITE_CONV. 78\ENDDOC 79