Theory: setlist

Parents

• list
• pred_set

Types

Constants

• LIST2SET  :'a list -> 'a -> bool
• SET2LIST  :('a -> bool) -> 'a list

Definitions

LIST2SET_def

|- (LIST2SET [] = {}) /\ !h t. LIST2SET (h::t) = h INSERT LIST2SET t

set2list_primitive_def

|- SET2LIST =
   WFREC (@R. WF R /\ !s. FINITE s /\ ~(s = {}) ==> R (REST s) s)
     (\SET2LIST' a.
        (if FINITE a then
           (if a = {} then [] else CHOICE a::SET2LIST' (REST a))
         else
           ARB))

Theorems

SET2LIST_CARD

|- !s. FINITE s ==> (LENGTH (SET2LIST s) = CARD s)

SET2LIST_IN_MEM

|- !s. FINITE s ==> !x. x IN s = MEM x (SET2LIST s)

SET2LIST_IND

|- !P. (!s. (FINITE s /\ ~(s = {}) ==> P (REST s)) ==> P s) ==> !v. P v

SET2LIST_INV

|- !s. FINITE s ==> (LIST2SET (SET2LIST s) = s)

SET2LIST_THM

|- FINITE s ==>
   (SET2LIST s = (if s = {} then [] else CHOICE s::SET2LIST (REST s)))