OR_EL_CONV

listLib.OR_EL_CONV : conv

Computes by inference the result of taking the disjunction of the elements of a boolean list.

For any object language list of the form “[x1;x2;...;xn]”, where x1, x2, …, xn are boolean expressions, the result of evaluating

   OR_EL_CONV “OR_EL [x1;x2;...;xn]”

is the theorem

   |- OR_EL [x1;x2;...;xn] = b

where b is either the boolean constant that denotes the disjunction of the elements of the list, or a disjunction of those xi that are not boolean constants.

Example

> listLib.OR_EL_CONV “OR_EL [T;F;F;T]”;
val it = ⊢ OR_EL [T; F; F; T] ⇔ T: thm

> listLib.OR_EL_CONV “OR_EL [F;F;F]”;
val it = ⊢ OR_EL [F; F; F] ⇔ F: thm

> listLib.OR_EL_CONV “OR_EL [F;x;y]”;
val it = ⊢ OR_EL [F; x; y] ⇔ x ∨ y: thm

> listLib.OR_EL_CONV “OR_EL [x;T;y]”;
val it = ⊢ OR_EL [x; T; y] ⇔ T: thm

Failure

OR_EL_CONV tm fails if tm is not of the form described above.