next up previous contents
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

Conor McBride