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

LFINITE_def

|- LFINITE =
   (λa0.
      ∀LFINITE'.
        (∀a0. (a0 = [||]) ∨ (∃h t. (a0 = h:::t) ∧ LFINITE' t) ⇒ LFINITE' a0) ⇒
        LFINITE' a0)

llength_rel_def

|- 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_def

|- 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))

linear_order_to_list_f_def

|- ∀lo.
     linear_order_to_list_f lo =
     (let min = minimal_elements (domain lo ∪ range lo) lo
      in
        if min = ∅ then NONE
        else SOME (rrestrict lo (domain lo ∪ range lo DIFF min),CHOICE min))

Theorems

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_rules

|- LFINITE [||] ∧ ∀h t. LFINITE t ⇒ LFINITE (h:::t)

LFINITE_ind

|- ∀LFINITE'.
     LFINITE' [||] ∧ (∀h t. LFINITE' t ⇒ LFINITE' (h:::t)) ⇒
     ∀a0. LFINITE a0 ⇒ LFINITE' a0

LFINITE_strongind

|- ∀LFINITE'.
     LFINITE' [||] ∧ (∀h t. LFINITE t ∧ LFINITE' t ⇒ LFINITE' (h:::t)) ⇒
     ∀a0. LFINITE a0 ⇒ LFINITE' a0

LFINITE_cases

|- ∀a0. LFINITE a0 ⇔ (a0 = [||]) ∨ ∃h t. (a0 = h:::t) ∧ LFINITE t

LFINITE_THM

|- (LFINITE [||] ⇔ T) ∧ ∀h t. LFINITE (h:::t) ⇔ LFINITE t

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_strongind

|- ∀llength_rel'.
     llength_rel' [||] 0 ∧
     (∀h n t.
        llength_rel t n ∧ 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_strongind

|- ∀P exists'.
     (∀h t. P h ⇒ exists' (h:::t)) ∧
     (∀h t. exists P 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

exists_strong_ind

|- ∀P Q.
     (∀h t. P h ⇒ Q (h:::t)) ∧ (∀h t. Q t ∧ exists P t ⇒ Q (h:::t)) ⇒
     ∀a0. exists P a0 ⇒ Q a0

exists_LDROP

|- exists P ll ⇔ ∃n a t. (LDROP n ll = SOME (a:::t)) ∧ P a

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

every_strong_coind

|- ∀P Q.
     (∀h t. Q (h:::t) ⇒ P h) ∧ (∀h t. Q (h:::t) ⇒ Q t ∨ every P t) ⇒
     ∀ll. Q ll ⇒ every P ll

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

LUNFOLD_THM

|- ∀f x v1 v2.
     ((f x = NONE) ⇒ (LUNFOLD f x = [||])) ∧
     ((f x = SOME (v1,v2)) ⇒ (LUNFOLD f x = v2:::LUNFOLD f v1))

LLIST_EQ

|- ∀f g.
     (∀x.
        (f x = [||]) ∧ (g x = [||]) ∨
        ∃h y. (f x = h:::f y) ∧ (g x = h:::g y)) ⇒
     ∀x. f x = g x

LUNFOLD_EQ

|- ∀R f s ll.
     R s ll ∧
     (∀s ll.
        R s ll ⇒
        (f s = NONE) ∧ (ll = [||]) ∨
        ∃s' x ll'.
          (f s = SOME (s',x)) ∧ (LHD ll = SOME x) ∧ (LTL ll = SOME ll') ∧
          R s' ll') ⇒
     (LUNFOLD f s = ll)

LMAP_LUNFOLD

|- ∀f g s.
     LMAP f (LUNFOLD g s) = LUNFOLD (λs. OPTION_MAP (λ(x,y). (x,f y)) (g s)) s

LNTH_LDROP

|- ∀n l x. (LNTH n l = SOME x) ⇒ (LHD (THE (LDROP n l)) = SOME x)

LAPPEND_fromList

|- ∀l1 l2. LAPPEND (fromList l1) (fromList l2) = fromList (l1 ++ l2)

LTAKE_LENGTH

|- ∀n ll l. (LTAKE n ll = SOME l) ⇒ (n = LENGTH l)

linear_order_to_llist

|- ∀lo X.
     linear_order lo X ∧ finite_prefixes lo X ⇒
     ∃ll.
       (X = {x | ∃i. LNTH i ll = SOME x}) ∧
       lo ⊆
       {(x,y) | ∃i j. i ≤ j ∧ (LNTH i ll = SOME x) ∧ (LNTH j ll = SOME y)} ∧
       ∀i j x. (LNTH i ll = SOME x) ∧ (LNTH j ll = SOME x) ⇒ (i = j)