Theory: llist

Parents

Types

llist(Arity = 1)

Constants

llist_rep :'a llist -> 'a list -> 'a option
lbuildn_rep :('a -> ('a # 'b) option) -> 'a -> num -> ('b list # 'a) option
LTAKE :num -> 'a llist -> 'a list option
LFLATTEN :'a llist llist -> 'a llist
lbuild_rep :('a -> ('a # 'b) option) -> 'a -> 'b list -> 'b option
toList :'a llist -> 'a list option
LFINITE :'a llist -> bool
LFILTER :('a -> bool) -> 'a llist -> 'a llist
LMAP :('a -> 'b) -> 'a llist -> 'b llist
LNIL :'a llist
lrep_ok :('a list -> 'a option) -> bool
ldest_rep :('a list -> 'a option) -> ('a # ('a list -> 'a option)) option
LNTH :num -> 'a llist -> 'a option
lrep_take :('a list -> 'a option) -> num -> 'a list option
lnil_rep :'a -> 'b option
LL_ALL :('a -> bool) -> 'a llist -> bool
never :('a -> bool) -> 'a llist -> bool
LAPPEND :'a llist -> 'a llist -> 'a llist
LDEST :'a llist -> ('a # 'a llist) option
LCONS :'a -> 'a llist -> 'a llist
firstPelemAt :('a -> bool) -> num -> 'a llist -> bool
LLENGTH :'a llist -> num option
LDROP :num -> 'a llist -> 'a llist option
LHD :'a llist -> 'a option
LTL :'a llist -> 'a llist option
lcons_rep :'a -> ('a list -> 'a option) -> 'a list -> 'a option
llist_abs :('a list -> 'a option) -> 'a llist
fromList :'a list -> 'a llist

Definitions

firstPelemAt

|- !P n ll.
     firstPelemAt P n ll =
     option_case F P (LNTH n ll) /\
     !m. m < n ==> (option_APPLY P (LNTH m ll) = SOME F)

fromList

|- (fromList [] = LNIL) /\ !h t. fromList (h::t) = LCONS h (fromList t)

LAPPEND

|- (!x. LAPPEND LNIL x = x) /\
   !h t x. LAPPEND (LCONS h t) x = LCONS h (LAPPEND t x)

lbuild_rep

|- !f x.
     lbuild_rep f x =
     (\pfx.
        option_case NONE
          (\(pfx',nthseed).
             (if pfx' = pfx then option_APPLY SND (f nthseed) else NONE))
          (lbuildn_rep f x (LENGTH pfx)))

lbuildn_rep

|- (!f x. lbuildn_rep f x 0 = SOME ([],x)) /\
   !f x n.
     lbuildn_rep f x (SUC n) =
     option_case NONE
       (\(pfx,x').
          option_case NONE (\(x'',last). SOME (APPEND pfx [last],x'')) (f x'))
       (lbuildn_rep f x n)

LCONS

|- !h t. LCONS h t = llist_abs (lcons_rep h (llist_rep t))

lcons_rep

|- !h t.
     lcons_rep h t =
     (\l. (if l = [] then SOME h else (if HD l = h then t (TL l) else NONE)))

LDEST

|- !ll.
     LDEST ll =
     option_case NONE (\p. SOME (FST p,llist_abs (SND p)))
       (ldest_rep (llist_rep ll))

ldest_rep

|- !f. ldest_rep f = option_case NONE (\x. SOME (x,(\l. f (x::l)))) (f [])

LDROP

|- (!ll. LDROP 0 ll = SOME ll) /\
   !n ll. LDROP (SUC n) ll = option_JOIN (option_APPLY (LDROP n) (LTL ll))

LFILTER

|- !P ll.
     LFILTER P ll =
     (if never P ll then
        LNIL
      else
        (if P (THE (LHD ll)) then
           LCONS (THE (LHD ll)) (LFILTER P (THE (LTL ll)))
         else
           LFILTER P (THE (LTL ll))))

LFINITE

|- !ll. LFINITE ll = ?n. LTAKE n ll = NONE

LFLATTEN

|- !ll.
     LFLATTEN ll =
     (if LL_ALL ($= LNIL) ll then
        LNIL
      else
        (if THE (LHD ll) = LNIL then
           LFLATTEN (THE (LTL ll))
         else
           LCONS (THE (LHD (THE (LHD ll))))
             (LFLATTEN (LCONS (THE (LTL (THE (LHD ll)))) (THE (LTL ll))))))

LHD

|- !ll. LHD ll = option_APPLY FST (ldest_rep (llist_rep ll))

LL_ALL

|- !P ll. LL_ALL P ll = never ($~ o P) ll

LLENGTH

|- !ll.
     LLENGTH ll =
     (if LFINITE ll then
        SOME
          ((@n.
              (LTAKE n ll = NONE) /\
              !m. m < n ==> ?ll'. LTAKE m ll = SOME ll') - 1)
      else
        NONE)

llist_absrep

|- (!a. llist_abs (llist_rep a) = a) /\
   !r. lrep_ok r = (llist_rep (llist_abs r) = r)

llist_TY_DEF

|- ?rep. TYPE_DEFINITION lrep_ok rep

LMAP

|- (!f. LMAP f LNIL = LNIL) /\
   !f h t. LMAP f (LCONS h t) = LCONS (f h) (LMAP f t)

LNIL

|- LNIL = llist_abs lnil_rep

lnil_rep

|- lnil_rep = (\l. NONE)

LNTH

|- (!ll. LNTH 0 ll = LHD ll) /\
   !n ll. LNTH (SUC n) ll = option_JOIN (option_APPLY (LNTH n) (LTL ll))

lrep_ok

|- !f. lrep_ok f = !l x. (f l = SOME x) ==> ?n. lrep_take f n = SOME l

lrep_take

|- (!f. lrep_take f 0 = SOME []) /\
   !f n.
     lrep_take f (SUC n) =
     option_case NONE
       (\pfx. option_case NONE (\a. SOME (APPEND pfx [a])) (f pfx))
       (lrep_take f n)

LTAKE

|- (!ll. LTAKE 0 ll = SOME []) /\
   !n ll.
     LTAKE (SUC n) ll =
     option_case NONE
       (\hd. option_case NONE (\tl. SOME (hd::tl)) (LTAKE n (THE (LTL ll))))
       (LHD ll)

LTL

|- !ll. LTL ll = option_APPLY (llist_abs o SND) (ldest_rep (llist_rep ll))

never

|- !P ll. never P ll = !n. ~firstPelemAt P n ll

toList

|- !ll. toList ll = (if LFINITE ll then LTAKE (THE (LLENGTH ll)) ll else NONE)

Theorems

firstPelemAt_CONS

|- !P n h t.
     firstPelemAt P n (LCONS h t) =
     (n = 0) /\ P h \/ ?m. (n = SUC m) /\ firstPelemAt P m t /\ ~P h

firstPelemAt_SUC

|- !P n h t. firstPelemAt P (SUC n) (LCONS h t) ==> firstPelemAt P n t

from_toList

|- !l. toList (fromList l) = SOME l

LAPPEND_ASSOC

|- !ll1 ll2 ll3. LAPPEND (LAPPEND ll1 ll2) ll3 = LAPPEND ll1 (LAPPEND ll2 ll3)

LAPPEND_NIL_2ND

|- !ll. LAPPEND ll LNIL = ll

LCONS_11

|- !h1 t1 h2 t2. (LCONS h1 t1 = LCONS h2 t2) = (h1 = h2) /\ (t1 = t2)

LCONS_NOT_NIL

|- !h t. ~(LCONS h t = LNIL) /\ ~(LNIL = LCONS h t)

LDROP1_THM

|- LDROP 1 = LTL

LDROP_THM

|- (!ll. LDROP 0 ll = SOME ll) /\ (!n. LDROP (SUC n) LNIL = NONE) /\
   !n h t. LDROP (SUC n) (LCONS h t) = LDROP n t

LFILTER_APPEND

|- !P ll1 ll2.
     LFINITE ll1 ==>
     (LFILTER P (LAPPEND ll1 ll2) = LAPPEND (LFILTER P ll1) (LFILTER P ll2))

LFILTER_NIL

|- !P ll. LL_ALL ($~ o P) ll ==> (LFILTER P ll = LNIL)

LFILTER_THM

|- (!P. LFILTER P LNIL = LNIL) /\
   !P h t.
     LFILTER P (LCONS h t) =
     (if P h then LCONS h (LFILTER P t) else LFILTER P t)

LFINITE_APPEND

|- !ll1 ll2. LFINITE (LAPPEND ll1 ll2) = LFINITE ll1 /\ LFINITE ll2

LFINITE_DROP

|- !n ll. LFINITE ll /\ n <= THE (LLENGTH ll) ==> ?y. LDROP n ll = SOME y

LFINITE_fromList

|- !l. LFINITE (fromList l)

LFINITE_HAS_LENGTH

|- !ll. LFINITE ll ==> ?n. LLENGTH ll = SOME n

LFINITE_INDUCTION

|- !P. P LNIL /\ (!t. P t ==> !h. P (LCONS h t)) ==> !ll. LFINITE ll ==> P ll

LFINITE_MAP

|- !f ll. LFINITE (LMAP f ll) = LFINITE ll

LFINITE_STRONG_INDUCTION

|- P LNIL /\ (!t. LFINITE t /\ P t ==> !h. P (LCONS h t)) ==>
   !ll. LFINITE ll ==> P ll

LFINITE_TAKE

|- !n ll. LFINITE ll /\ n <= THE (LLENGTH ll) ==> ?y. LTAKE n ll = SOME y

LFINITE_THM

|- (LFINITE LNIL = T) /\ !h t. LFINITE (LCONS h t) = LFINITE t

LFINITE_toList

|- !ll. LFINITE ll ==> ?l. toList ll = SOME l

LFLATTEN_APPEND

|- !h t. LFLATTEN (LCONS h t) = LAPPEND h (LFLATTEN t)

LFLATTEN_EQ_NIL

|- !ll. (LFLATTEN ll = LNIL) = LL_ALL ($= LNIL) ll

LFLATTEN_SINGLETON

|- !h. LFLATTEN (LCONS h LNIL) = h

LFLATTEN_THM

|- (LFLATTEN LNIL = LNIL) /\ (!tl. LFLATTEN (LCONS LNIL t) = LFLATTEN t) /\
   !h t tl. LFLATTEN (LCONS (LCONS h t) tl) = LCONS h (LFLATTEN (LCONS t tl))

LHD_EQ_NONE

|- !ll. (LHD ll = NONE) = (ll = LNIL)

LHD_THM

|- (LHD LNIL = NONE) /\ !h t. LHD (LCONS h t) = SOME h

LHDTL_CONS_THM

|- !h t. (LHD (LCONS h t) = SOME h) /\ (LTL (LCONS h t) = SOME t)

LHDTL_EQ_SOME

|- !h t ll. (ll = LCONS h t) = (LHD ll = SOME h) /\ (LTL ll = SOME t)

LL_ALL_THM

|- (!P. LL_ALL P LNIL = T) /\ !P h t. LL_ALL P (LCONS h t) = P h /\ LL_ALL P t

LLENGTH_APPEND

|- !ll1 ll2.
     LLENGTH (LAPPEND ll1 ll2) =
     (if LFINITE ll1 /\ LFINITE ll2 then
        SOME (THE (LLENGTH ll1) + THE (LLENGTH ll2))
      else
        NONE)

LLENGTH_fromList

|- !l. LLENGTH (fromList l) = SOME (LENGTH l)

LLENGTH_MAP

|- !ll f. LLENGTH (LMAP f ll) = LLENGTH ll

LLENGTH_THM

|- (LLENGTH LNIL = SOME 0) /\
   !h t. LLENGTH (LCONS h t) = option_APPLY SUC (LLENGTH t)

llist_Axiom

|- !f.
     ?g.
       (!x. LHD (g x) = option_APPLY SND (f x)) /\
       !x. LTL (g x) = option_APPLY (g o FST) (f x)

LLIST_BISIMULATION

|- !ll1 ll2.
     (ll1 = ll2) =
     ?R.
       R ll1 ll2 /\
       !ll3 ll4.
         R ll3 ll4 ==>
         (ll3 = LNIL) /\ (ll4 = LNIL) \/
         (LHD ll3 = LHD ll4) /\ R (THE (LTL ll3)) (THE (LTL ll4))

llist_CASES

|- !l. (l = LNIL) \/ ?h t. l = LCONS h t

LMAP_APPEND

|- !f ll1 ll2. LMAP f (LAPPEND ll1 ll2) = LAPPEND (LMAP f ll1) (LMAP f ll2)

LMAP_MAP

|- !f g ll. LMAP f (LMAP g ll) = LMAP (f o g) ll

LNTH_THM

|- (!n. LNTH n LNIL = NONE) /\ (!h t. LNTH 0 (LCONS h t) = SOME h) /\
   !n h t. LNTH (SUC n) (LCONS h t) = LNTH n t

LTAKE_CONS_EQ_NONE

|- !m h t.
     (LTAKE m (LCONS h t) = NONE) = ?n. (m = SUC n) /\ (LTAKE n t = NONE)

LTAKE_CONS_EQ_SOME

|- !m h t l.
     (LTAKE m (LCONS h t) = SOME l) =
     (m = 0) /\ (l = []) \/
     ?n l'. (m = SUC n) /\ (LTAKE n t = SOME l') /\ (l = h::l')

LTAKE_DROP

|- (!n ll.
      ~LFINITE ll ==>
      (LAPPEND (fromList (THE (LTAKE n ll))) (THE (LDROP n ll)) = ll)) /\
   !n ll.
     LFINITE ll /\ n <= THE (LLENGTH ll) ==>
     (LAPPEND (fromList (THE (LTAKE n ll))) (THE (LDROP n ll)) = ll)

LTAKE_EQ

|- !ll1 ll2. (ll1 = ll2) = !n. LTAKE n ll1 = LTAKE n ll2

LTAKE_EQ_NONE

|- !ll n. (LTAKE n ll = NONE) ==> 0 < n

LTAKE_EQ_SOME_CONS

|- !n l x. (LTAKE n l = SOME x) ==> !h. ?y. LTAKE n (LCONS h l) = SOME y

LTAKE_fromList

|- !l. LTAKE (LENGTH l) (fromList l) = SOME l

LTAKE_NIL_EQ_NONE

|- !m. (LTAKE m LNIL = NONE) = 0 < m

LTAKE_NIL_EQ_SOME

|- !l m. (LTAKE m LNIL = SOME l) = (m = 0) /\ (l = [])

LTAKE_THM

|- (!l. LTAKE 0 l = SOME []) /\ (!n. LTAKE (SUC n) LNIL = NONE) /\
   !n h t. LTAKE (SUC n) (LCONS h t) = option_APPLY (CONS h) (LTAKE n t)

LTL_EQ_NONE

|- !ll. (LTL ll = NONE) = (ll = LNIL)

LTL_THM

|- (LTL LNIL = NONE) /\ !h t. LTL (LCONS h t) = SOME t

never_THM

|- (!P. never P LNIL = T) /\ !P h t. never P (LCONS h t) = ~P h /\ never P t

NOT_LFINITE_APPEND

|- !ll1 ll2. ~LFINITE ll1 ==> (LAPPEND ll1 ll2 = ll1)

NOT_LFINITE_DROP

|- !ll. ~LFINITE ll ==> !n. ?y. LDROP n ll = SOME y

NOT_LFINITE_NO_LENGTH

|- !ll. ~LFINITE ll ==> (LLENGTH ll = NONE)

NOT_LFINITE_TAKE

|- !ll. ~LFINITE ll ==> !n. ?y. LTAKE n ll = SOME y

to_fromList

|- !ll. LFINITE ll ==> (fromList (THE (toList ll)) = ll)

toList_THM

|- (toList LNIL = SOME []) /\
   !h t. toList (LCONS h t) = option_APPLY (CONS h) (toList t)