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