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