1\DOC EVERY_CONJ_CONV 2 3\TYPE {EVERY_CONJ_CONV : conv -> conv} 4 5\SYNOPSIS 6Applies a conversion to every top-level conjunct in a term. 7 8\KEYWORDS 9conversional. 10 11\DESCRIBE 12The term {EVERY_CONJ_CONV c t} takes the conversion {c} and applies 13this to every top-level conjunct within term {t}. A top-level 14conjunct is a sub-term that can be reached from the root of the term 15by breaking apart only conjunctions. The terms affected by {c} are 16those that would be returned by a call to {strip_conj c}. In 17particular, if the term as a whole is not a conjunction, then the 18conversion will be applied to the whole term. 19 20If the result of the application of the conversion to one of the 21conjuncts is one of the constants true or false, then one of two 22standard rewrites is applied, simplifying the resulting term. If one 23of the conjuncts is converted to false, then the conversion will not be 24applied to the remaining conjuncts (the conjuncts are worked on from 25left to right), and the result of the whole application will simply be 26false. Alternatively, conjuncts that are converted to true will not 27appear in the final result at all. 28 29 30 31\FAILURE 32Fails if the conversion argument fails when applied to one of the 33top-level conjuncts in a term. 34 35\EXAMPLE 36{ 37- EVERY_CONJ_CONV BETA_CONV (Term`(\x. x /\ y) p`); 38> val it = |- (\x. x /\ y) p = p /\ y : thm 39- EVERY_CONJ_CONV BETA_CONV (Term`(\y. y /\ p) q /\ (\z. z) r`); 40> val it = |- (\y. y /\ p) q /\ (\z. z) r = (q /\ p) /\ r : thm 41} 42 43 44\USES 45Useful for applying a conversion to all of the ``significant'' 46sub-terms within a term without having to worry about the exact 47structure of its conjunctive skeleton. 48 49\SEEALSO 50Conv.EVERY_DISJ_CONV, Conv.RATOR_CONV, Conv.RAND_CONV, Conv.LAND_CONV. 51\ENDDOC 52