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