Next: Partial List functions Up: List Previous: List Basics

## List functions with booleans

This file contains list functions and theorems involving the booleans. These include the boolean valued test for nil, test for membership give a boolean-valued equality over the type of elements of the list, list subtraction, universal and existential extensions of a predicate to a list of values.

``` ** Module lib_list_bool Imports lib_list_basics lib_bool_thms
nil_test = ... : {s|Type}(list s)->bool
exist_list = ... : {t|Type}(t->bool)->(list t)->bool
all_list = ... : {t|Type}(t->bool)->(list t)->bool
member = ... : {t|Type}(t->t->bool)->t->(list t)->bool
list_eq = ... : {t|Type}(t->t->bool)->(list t)->(list t)->bool
del_first = ... : {t|Type}(t->t->bool)->t->(list t)->list t
del_all = ... : {t|Type}(t->t->bool)->t->(list t)->list t
list_sub = ... : {A|Type}(Type)->(A->bool)->A->(list A)->list A
exist_list_append_lem = ... :
{t|Type}{P:t->bool}{j,k:list t}
Eq (exist_list P (append j k))
(orelse (exist_list P j) (exist_list P k))
member_append_lem = ... :
{t|Type}{eq_on_t:t->t->bool}{x:t}{j,k:list t}
Eq (member eq_on_t x (append j k))
(orelse (member eq_on_t x j) (member eq_on_t x k))
nil_test_true_equiv_Eq_nil = ... :
{t|Type}{l:list t}iff (Eq (nil_test l) true) (Eq l (nil t))
nil_test_false_equiv_Eq_cons = ... :
{t|Type}{l:list t}
iff (Eq (nil_test l) false)
(Ex ([a:t]Ex ([m:list t]Eq l (cons a m))))
nil_test_on_append = ... :
{t|Type}{l,m:list t}{a:t}Eq (nil_test (append l (cons a m))) false```

Lego
Fri May 24 19:01:27 BST 1996