Theory "llist"

Signature

Definitions

lrep_ok_def

|- !f.
     lrep_ok f =
     ?P.
       (!g.
          P g ==>
          (g = (\n. NONE)) \/
          ?h t. P t /\ (g = (\n. (if n = 0 then SOME h else t (n - 1))))) /\
       P f

llist_TY_DEF

|- ?rep. TYPE_DEFINITION lrep_ok rep

llist_absrep

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

LNIL

|- [| |] = llist_abs (\n. NONE)

LCONS

|- !h t.
     h:::t = llist_abs (\n. (if n = 0 then SOME h else llist_rep t (n - 1)))

LHD

|- !ll. LHD ll = llist_rep ll 0

LTL

|- !ll.
     LTL ll =
     case LHD ll of
        NONE -> NONE
     || SOME v -> SOME (llist_abs (\n. llist_rep ll (n + 1)))

LNTH

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

LUNFOLD

|- !f x.
     LUNFOLD f x =
     case f x of NONE -> [| |] || SOME (v1,v2) -> v2:::LUNFOLD f v1

LTAKE

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

LMAP

|- (!f. LMAP f [| |] = [| |]) /\ !f h t. LMAP f (h:::t) = f h:::LMAP f t

LAPPEND

|- (!x. LAPPEND [| |] x = x) /\ !h t x. LAPPEND (h:::t) x = h:::LAPPEND t x

llength_rel

|- llength_rel =
   (\a0 a1.
      !llength_rel'.
        (!a0 a1.
           (a0 = [| |]) /\ (a1 = 0) \/
           (?h n t. (a0 = h:::t) /\ (a1 = SUC n) /\ llength_rel' t n) ==>
           llength_rel' a0 a1) ==>
        llength_rel' a0 a1)

LLENGTH

|- !ll. LLENGTH ll = (if LFINITE ll then SOME @n. llength_rel ll n else NONE)

toList

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

fromList

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

LDROP

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

exists

|- exists =
   (\P a0.
      !exists'.
        (!a0.
           (?h t. (a0 = h:::t) /\ P h) \/
           (?h t. (a0 = h:::t) /\ exists' t) ==>
           exists' a0) ==>
        exists' a0)

every_def

|- !P ll. every P ll = ~exists ($~ o P) ll

LFILTER

|- !P ll.
     LFILTER P ll =
     (if ~exists P ll then
        [| |]
      else
        (if P (THE (LHD ll)) then
           THE (LHD ll):::LFILTER P (THE (LTL ll))
         else
           LFILTER P (THE (LTL ll))))

LFLATTEN

|- !ll.
     LFLATTEN ll =
     (if every ($= [| |]) ll then
        [| |]
      else
        (if THE (LHD ll) = [| |] then
           LFLATTEN (THE (LTL ll))
         else
           THE (LHD (THE (LHD ll))):::
               LFLATTEN (THE (LTL (THE (LHD ll))):::THE (LTL ll))))

LZIP_THM

|- (!l1. LZIP (l1,[| |]) = [| |]) /\ (!l2. LZIP ([| |],l2) = [| |]) /\
   !h1 h2 t1 t2. LZIP (h1:::t1,h2:::t2) = (h1,h2):::LZIP (t1,t2)

LUNZIP_THM

|- (LUNZIP [| |] = ([| |],[| |])) /\
   !x y t.
     LUNZIP ((x,y):::t) = (let (ll1,ll2) = LUNZIP t in (x:::ll1,y:::ll2))

Theorems

LFINITE_THM

|- (LFINITE [| |] = T) /\ !h t. LFINITE (h:::t) = LFINITE t

LFINITE_cases

|- !a0. LFINITE a0 = (a0 = [| |]) \/ ?h t. (a0 = h:::t) /\ LFINITE t

LFINITE_ind

|- !LFINITE'.
     LFINITE' [| |] /\ (!h t. LFINITE' t ==> LFINITE' (h:::t)) ==>
     !a0. LFINITE a0 ==> LFINITE' a0

LFINITE_rules

|- LFINITE [| |] /\ !h t. LFINITE t ==> LFINITE (h:::t)

llist_rep_LCONS

|- llist_rep (h:::t) = (\n. (if n = 0 then SOME h else llist_rep t (n - 1)))

LHD_LCONS

|- LHD (h:::t) = SOME h

LTL_LCONS

|- LTL (h:::t) = SOME t

LHDTL_CONS_THM

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

llist_CASES

|- !l. (l = [| |]) \/ ?h t. l = h:::t

LHD_THM

|- (LHD [| |] = NONE) /\ !h t. LHD (h:::t) = SOME h

LTL_THM

|- (LTL [| |] = NONE) /\ !h t. LTL (h:::t) = SOME t

LCONS_NOT_NIL

|- !h t. ~(h:::t = [| |]) /\ ~([| |] = h:::t)

LCONS_11

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

LHD_EQ_NONE

|- !ll. ((LHD ll = NONE) = (ll = [| |])) /\ ((NONE = LHD ll) = (ll = [| |]))

LTL_EQ_NONE

|- !ll. ((LTL ll = NONE) = (ll = [| |])) /\ ((NONE = LTL ll) = (ll = [| |]))

LHDTL_EQ_SOME

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

LNTH_THM

|- (!n. LNTH n [| |] = NONE) /\ (!h t. LNTH 0 (h:::t) = SOME h) /\
   !n h t. LNTH (SUC n) (h:::t) = LNTH n t

llist_ue_Axiom

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

llist_Axiom

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

llist_Axiom_1

|- !f. ?g. !x. g x = case f x of NONE -> [| |] || SOME (a,b) -> b:::g a

llist_Axiom_1ue

|- !f. ?!g. !x. g x = case f x of NONE -> [| |] || SOME (a,b) -> b:::g a

LLIST_BISIMULATION0

|- !ll1 ll2.
     (ll1 = ll2) =
     ?R.
       R ll1 ll2 /\
       !ll3 ll4.
         R ll3 ll4 ==>
         (ll3 = [| |]) /\ (ll4 = [| |]) \/
         ?h t1 t2. (ll3 = h:::t1) /\ (ll4 = h:::t2) /\ R t1 t2

LLIST_BISIMULATION

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

LLIST_STRONG_BISIMULATION

|- !ll1 ll2.
     (ll1 = ll2) =
     ?R.
       R ll1 ll2 /\
       !ll3 ll4.
         R ll3 ll4 ==>
         (ll3 = ll4) \/ ?h t1 t2. (ll3 = h:::t1) /\ (ll4 = h:::t2) /\ R t1 t2

LNTH_EQ

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

LTAKE_THM

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

LTAKE_SNOC_LNTH

|- !n ll.
     LTAKE (SUC n) ll =
     case LTAKE n ll of
        NONE -> NONE
     || SOME l -> case LNTH n ll of NONE -> NONE || SOME e -> SOME (l ++ [e])

LTAKE_LNTH

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

LTAKE_NIL_EQ_SOME

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

LTAKE_NIL_EQ_NONE

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

LTAKE_EQ

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

LTAKE_CONS_EQ_NONE

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

LTAKE_CONS_EQ_SOME

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

LTAKE_EQ_SOME_CONS

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

LMAP_APPEND

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

LAPPEND_EQ_LNIL

|- (LAPPEND l1 l2 = [| |]) = (l1 = [| |]) /\ (l2 = [| |])

LAPPEND_ASSOC

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

LMAP_MAP

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

LAPPEND_NIL_2ND

|- !ll. LAPPEND ll [| |] = ll

LFINITE

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

llength_rel_rules

|- llength_rel [| |] 0 /\
   !h n t. llength_rel t n ==> llength_rel (h:::t) (SUC n)

llength_rel_ind

|- !llength_rel'.
     llength_rel' [| |] 0 /\
     (!h n t. llength_rel' t n ==> llength_rel' (h:::t) (SUC n)) ==>
     !a0 a1. llength_rel a0 a1 ==> llength_rel' a0 a1

llength_rel_cases

|- !a0 a1.
     llength_rel a0 a1 =
     (a0 = [| |]) /\ (a1 = 0) \/
     ?h n t. (a0 = h:::t) /\ (a1 = SUC n) /\ llength_rel t n

LLENGTH_THM

|- (LLENGTH [| |] = SOME 0) /\
   !h t. LLENGTH (h:::t) = OPTION_MAP SUC (LLENGTH t)

LFINITE_HAS_LENGTH

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

NOT_LFINITE_NO_LENGTH

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

LFINITE_INDUCTION

|- !P. P [| |] /\ (!h t. P t ==> P (h:::t)) ==> !a0. LFINITE a0 ==> P a0

LFINITE_STRONG_INDUCTION

|- P [| |] /\ (!h t. LFINITE t /\ P t ==> P (h:::t)) ==>
   !a0. LFINITE a0 ==> P a0

LFINITE_MAP

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

LFINITE_APPEND

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

NOT_LFINITE_APPEND

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

LLENGTH_MAP

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

LLENGTH_APPEND

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

toList_THM

|- (toList [| |] = SOME []) /\
   !h t. toList (h:::t) = OPTION_MAP (CONS h) (toList t)

LFINITE_fromList

|- !l. LFINITE (fromList l)

LLENGTH_fromList

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

LTAKE_fromList

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

from_toList

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

LFINITE_toList

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

to_fromList

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

LDROP_THM

|- (!ll. LDROP 0 ll = SOME ll) /\ (!n. LDROP (SUC n) [| |] = NONE) /\
   !n h t. LDROP (SUC n) (h:::t) = LDROP n t

LDROP1_THM

|- LDROP 1 = LTL

NOT_LFINITE_TAKE

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

LFINITE_TAKE

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

NOT_LFINITE_DROP

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

LFINITE_DROP

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

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)

exists_rules

|- !P.
     (!h t. P h ==> exists P (h:::t)) /\ !h t. exists P t ==> exists P (h:::t)

exists_ind

|- !P exists'.
     (!h t. P h ==> exists' (h:::t)) /\
     (!h t. exists' t ==> exists' (h:::t)) ==>
     !a0. exists P a0 ==> exists' a0

exists_cases

|- !P a0.
     exists P a0 =
     (?h t. (a0 = h:::t) /\ P h) \/ ?h t. (a0 = h:::t) /\ exists P t

exists_thm

|- (exists P [| |] = F) /\ (exists P (h:::t) = P h \/ exists P t)

exists_LNTH

|- !l. exists P l = ?n e. (SOME e = LNTH n l) /\ P e

MONO_exists

|- (!x. P x ==> Q x) ==> exists P l ==> exists Q l

every_coind

|- !P Q. (!h t. Q (h:::t) ==> P h /\ Q t) ==> !ll. Q ll ==> every P ll

every_thm

|- (every P [| |] = T) /\ (every P (h:::t) = P h /\ every P t)

LL_ALL_THM

|- (every P [| |] = T) /\ (every P (h:::t) = P h /\ every P t)

MONO_every

|- (!x. P x ==> Q x) ==> every P l ==> every Q l

LFILTER_THM

|- (!P. LFILTER P [| |] = [| |]) /\
   !P h t. LFILTER P (h:::t) = (if P h then h:::LFILTER P t else LFILTER P t)

LFILTER_NIL

|- !P ll. every ($~ o P) ll ==> (LFILTER P ll = [| |])

LFILTER_EQ_NIL

|- !ll. (LFILTER P ll = [| |]) = every ($~ o P) ll

LFILTER_APPEND

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

LFLATTEN_THM

|- (LFLATTEN [| |] = [| |]) /\ (!tl. LFLATTEN ([| |]:::t) = LFLATTEN t) /\
   !h t tl. LFLATTEN ((h:::t):::tl) = h:::LFLATTEN (t:::tl)

LFLATTEN_APPEND

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

LFLATTEN_EQ_NIL

|- !ll. (LFLATTEN ll = [| |]) = every ($= [| |]) ll

LFLATTEN_SINGLETON

|- !h. LFLATTEN [|h|] = h

LZIP_LUNZIP

|- !ll. LZIP (LUNZIP ll) = ll