AND_EL_CONV
listLib.AND_EL_CONV : conv
Computes by inference the result of taking the conjunction 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
AND_EL_CONV “AND_EL [x1;x2;...;xn]”
is the theorem
|- AND_EL [x1;x2;...;xn] = b
where b is either the boolean constant that denotes the conjunction of
the elements of the list, or a conjunction of those xi that are not
boolean constants.
Example
> listLib.AND_EL_CONV “AND_EL [T;F;F;T]”;
val it = ⊢ AND_EL [T; F; F; T] ⇔ F: thm
> listLib.AND_EL_CONV “AND_EL [T;T;T]”;
val it = ⊢ AND_EL [T; T; T] ⇔ T: thm
> listLib.AND_EL_CONV “AND_EL [T;x;y]”;
val it = ⊢ AND_EL [T; x; y] ⇔ x ∧ y: thm
> listLib.AND_EL_CONV “AND_EL [x;F;y]”;
val it = ⊢ AND_EL [x; F; y] ⇔ F: thm
Failure
AND_EL_CONV tm fails if tm is not of the form described above.