Theory "llist"

Signature

Definitions

lrep_ok_def

⊢ lrep_ok =
  (λa0.
       ∃lrep_ok'.
           lrep_ok' a0 ∧
           ∀a0.
               lrep_ok' a0 ⇒
               a0 = (λn. NONE) ∨
               ∃h t.
                   a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧ lrep_ok' t)

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

LTL_HD_def

⊢ ∀ll.
      LTL_HD ll =
      case llist_rep ll 0 of
        NONE => NONE
      | SOME h => SOME (llist_abs (llist_rep ll ∘ SUC),h)

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_def

⊢ ∀f z.
      LUNFOLD f z =
      llist_abs
        (λn.
             OPTION_MAP SND
               (FUNPOW (λm. OPTION_BIND m (UNCURRY (K ∘ f))) n (f z)))

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_def

⊢ 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 ($~ ∘ 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))

LPREFIX_def

⊢ ∀l1 l2.
      LPREFIX l1 l2 ⇔
      case toList l1 of
        NONE => l1 = l2
      | SOME xs =>
        case toList l2 of
          NONE => LTAKE (LENGTH xs) l2 = SOME xs
        | SOME ys => xs ≼ ys

LGENLIST_def

⊢ (∀f. LGENLIST f NONE = LUNFOLD (λn. SOME (n + 1,f n)) 0) ∧
  ∀f lim.
      LGENLIST f (SOME lim) =
      LUNFOLD (λn. if n < lim then SOME (n + 1,f n) else NONE) 0

LREPEAT_def

⊢ ∀l.
      LREPEAT l = if NULL l then [||]
      else LGENLIST (λn. EL (n MOD LENGTH l) l) NONE

Theorems

lrep_ok_rules

⊢ lrep_ok (λn. NONE) ∧
  ∀h t. lrep_ok t ⇒ lrep_ok (λn. if n = 0 then SOME h else t (n − 1))

lrep_ok_coind

⊢ ∀lrep_ok'.
      (∀a0.
           lrep_ok' a0 ⇒
           a0 = (λn. NONE) ∨
           ∃h t. a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧ lrep_ok' t) ⇒
      ∀a0. lrep_ok' a0 ⇒ lrep_ok a0

lrep_ok_cases

⊢ ∀a0.
      lrep_ok a0 ⇔
      a0 = (λn. NONE) ∨
      ∃h t. a0 = (λn. if n = 0 then SOME h else t (n − 1)) ∧ lrep_ok t

lrep_ok_alt

⊢ lrep_ok f ⇔ ∀n. IS_SOME (f (SUC n)) ⇒ IS_SOME (f n)

lrep_ok_MAP

⊢ lrep_ok (λn. OPTION_MAP f (g n)) ⇔ lrep_ok g

lrep_ok_FUNPOW_BIND

⊢ lrep_ok (λn. FUNPOW (λm. OPTION_BIND m g) n fz)

llist_rep_LCONS

⊢ llist_rep (h:::t) = (λn. if n = 0 then SOME h else llist_rep t (n − 1))

llist_rep_LNIL

⊢ llist_rep [||] = (λn. NONE)

LTL_HD_LNIL

⊢ LTL_HD [||] = NONE

LTL_HD_LCONS

⊢ LTL_HD (h:::t) = SOME (t,h)

LTL_HD_HD

⊢ LHD ll = OPTION_MAP SND (LTL_HD ll)

LTL_HD_TL

⊢ LTL ll = OPTION_MAP FST (LTL_HD ll)

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

LTL_HD_11

⊢ LTL_HD ll1 = LTL_HD ll2 ⇒ ll1 = ll2

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

LTL_HD_iff

⊢ (LTL_HD x = SOME (t,h) ⇔ x = h:::t) ∧ (LTL_HD x = NONE ⇔ x = [||])

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

LNTH_rep

⊢ ∀i ll. LNTH i ll = llist_rep ll i

LNTH_EQ

⊢ ∀ll1 ll2. ll1 = ll2 ⇔ ∀n. LNTH n ll1 = LNTH n ll2

LUNFOLD

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

LUNFOLD_UNIQUE

⊢ ∀f g.
      (∀x. g x = case f x of NONE => [||] | SOME (v1,v2) => v2:::g v1) ⇒
      ∀y. g y = LUNFOLD f y

LUNFOLD_LTL_HD

⊢ LUNFOLD LTL_HD ll = ll

LTL_HD_LUNFOLD

⊢ LTL_HD (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ## I) (f x)

LNTH_LUNFOLD

⊢ LNTH 0 (LUNFOLD f x) = OPTION_MAP SND (f x) ∧
  LNTH (SUC n) (LUNFOLD f x) =
  case f x of NONE => NONE | SOME (tx,hx) => LNTH n (LUNFOLD f tx)

LNTH_LUNFOLD_compute

⊢ LNTH 0 (LUNFOLD f x) = OPTION_MAP SND (f x) ∧
  (∀n.
       LNTH (NUMERAL (BIT1 n)) (LUNFOLD f x) =
       case f x of
         NONE => NONE
       | SOME (tx,hx) => LNTH (NUMERAL (BIT1 n) − 1) (LUNFOLD f tx)) ∧
  ∀n.
      LNTH (NUMERAL (BIT2 n)) (LUNFOLD f x) =
      case f x of
        NONE => NONE
      | SOME (tx,hx) => LNTH (NUMERAL (BIT1 n)) (LUNFOLD f tx)

LHD_LUNFOLD

⊢ LHD (LUNFOLD f x) = OPTION_MAP SND (f x)

LTL_LUNFOLD

⊢ LTL (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ∘ 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_ue_Axiom

⊢ ∀f.
      ∃!g.
          (∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
          ∀x. LTL (g x) = OPTION_MAP (g ∘ FST) (f x)

llist_Axiom

⊢ ∀f.
      ∃g.
          (∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
          ∀x. LTL (g x) = OPTION_MAP (g ∘ FST) (f x)

LUNFOLD_BISIMULATION

⊢ ∀f1 f2 x1 x2.
      LUNFOLD f1 x1 = LUNFOLD f2 x2 ⇔
      ∃R.
          R x1 x2 ∧
          ∀y1 y2.
              R y1 y2 ⇒
              f1 y1 = NONE ∧ f2 y2 = NONE ∨
              ∃h t1 t2. f1 y1 = SOME (t1,h) ∧ f2 y2 = SOME (t2,h) ∧ R t1 t2

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

LTAKE_LUNFOLD

⊢ LTAKE 0 (LUNFOLD f x) = SOME [] ∧
  LTAKE (SUC n) (LUNFOLD f x) =
  case f x of
    NONE => NONE
  | SOME (tx,hx) => OPTION_MAP (CONS hx) (LTAKE n (LUNFOLD f tx))

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_EQ_NONE_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 ∘ g) ll

LAPPEND_NIL_2ND

⊢ ∀ll. LAPPEND ll [||] = ll

LHD_LAPPEND

⊢ LHD (LAPPEND l1 l2) = if l1 = [||] then LHD l2 else LHD l1

LTL_LAPPEND

⊢ LTL (LAPPEND l1 l2) = if l1 = [||] then LTL l2
  else SOME (LAPPEND (THE (LTL l1)) l2)

LTAKE_LAPPEND1

⊢ ∀n l1 l2. IS_SOME (LTAKE n l1) ⇒ LTAKE n (LAPPEND l1 l2) = LTAKE n l1

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)

LLENGTH_0

⊢ LLENGTH x = SOME 0 ⇔ x = [||]

LFINITE_HAS_LENGTH

⊢ ∀ll. LFINITE ll ⇒ ∃n. LLENGTH ll = SOME n

NOT_LFINITE_NO_LENGTH

⊢ ∀ll. ¬LFINITE ll ⇒ LLENGTH ll = NONE

LFINITE_LLENGTH

⊢ LFINITE ll ⇔ ∃n. LLENGTH ll = SOME n

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

LTAKE_LNTH_EL

⊢ ∀n ll m l. LTAKE n ll = SOME l ∧ m < n ⇒ LNTH m ll = SOME (EL m l)

NOT_LFINITE_APPEND

⊢ ∀ll1 ll2. ¬LFINITE ll1 ⇒ LAPPEND ll1 ll2 = ll1

LFINITE_LAPPEND_IMP_NIL

⊢ ∀ll. LFINITE ll ⇒ ∀l2. LAPPEND ll l2 = ll ⇒ l2 = [||]

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)

fromList_EQ_LNIL

⊢ fromList l = [||] ⇔ l = []

LHD_fromList

⊢ LHD (fromList l) = if NULL l then NONE else SOME (HD l)

LTL_fromList

⊢ LTL (fromList l) = if NULL l then NONE else SOME (fromList (TL l))

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

LFINITE_toList_SOME

⊢ LFINITE ll ⇔ IS_SOME (toList ll)

to_fromList

⊢ ∀ll. LFINITE ll ⇒ fromList (THE (toList ll)) = ll

LTAKE_LAPPEND2

⊢ ∀n l1 l2.
      LTAKE n l1 = NONE ⇒
      LTAKE n (LAPPEND l1 l2) =
      OPTION_MAP ($++ (THE (toList l1))) (LTAKE (n − THE (LLENGTH l1)) l2)

LNTH_fromList

⊢ LNTH n (fromList l) = if n < LENGTH l then SOME (EL n l) else NONE

lnth_fromList_some

⊢ ∀n l. n < LENGTH l ⇔ LNTH n (fromList l) = SOME (EL n l)

LDROP_FUNPOW

⊢ ∀n ll. LDROP n ll = FUNPOW (λm. OPTION_BIND m LTL) n (SOME 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

LNTH_HD_LDROP

⊢ ∀n ll. LNTH n ll = OPTION_BIND (LDROP n ll) LHD

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

LDROP_ADD

⊢ ∀k1 k2 x.
      LDROP (k1 + k2) x =
      case LDROP k1 x of NONE => NONE | SOME ll => LDROP k2 ll

LDROP_SOME_LLENGTH

⊢ LDROP n ll = SOME l ∧ LLENGTH ll = SOME m ⇒ n ≤ m ∧ LLENGTH l = SOME (m − n)

LFINITE_LNTH_NONE

⊢ LFINITE ll ⇔ ∃n. LNTH n ll = NONE

infinite_lnth_some

⊢ ∀ll. ¬LFINITE ll ⇔ ∀n. ∃x. LNTH n ll = SOME x

LNTH_LAPPEND

⊢ LNTH n (LAPPEND l1 l2) =
  case LLENGTH l1 of
    NONE => LNTH n l1
  | SOME m => if n < m then LNTH n l1 else LNTH (n − m) l2

LNTH_ADD

⊢ ∀a b ll. LNTH (a + b) ll = OPTION_BIND (LDROP a ll) (LNTH b)

lnth_some_down_closed

⊢ ∀ll x n1 n2. LNTH n1 ll = SOME x ∧ n2 ≤ n1 ⇒ ∃y. LNTH n2 ll = SOME y

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 ($~ ∘ P) ll ⇒ LFILTER P ll = [||]

LFILTER_EQ_NIL

⊢ ∀ll. LFILTER P ll = [||] ⇔ every ($~ ∘ 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

LTAKE_TAKE_LESS

⊢ LTAKE n ll = SOME l ∧ m ≤ n ⇒ LTAKE m ll = SOME (TAKE m l)

LTAKE_LLENGTH_NONE

⊢ LLENGTH ll = SOME n ∧ n < m ⇒ LTAKE m ll = NONE

LTAKE_LLENGTH_SOME

⊢ LLENGTH ll = SOME n ⇒ ∃l. LTAKE n ll = SOME l ∧ toList ll = SOME l

toList_LAPPEND_APPEND

⊢ toList (LAPPEND l1 l2) = SOME x ⇒ x = THE (toList l1) ++ THE (toList l2)

LNTH_LLENGTH_NONE

⊢ LLENGTH l = SOME x ∧ x ≤ n ⇒ LNTH n l = NONE

LNTH_NONE_MONO

⊢ ∀m n l. LNTH m l = NONE ∧ m ≤ n ⇒ LNTH n l = NONE

linear_order_to_llist_eq

⊢ ∀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

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

LPREFIX_LNIL

⊢ LPREFIX [||] ll ∧ (LPREFIX ll [||] ⇔ ll = [||])

LPREFIX_LCONS

⊢ (∀ll h t. LPREFIX ll (h:::t) ⇔ ll = [||] ∨ ∃l. ll = h:::l ∧ LPREFIX l t) ∧
  ∀h t ll. LPREFIX (h:::t) ll ⇔ ∃l. ll = h:::l ∧ LPREFIX t l

LPREFIX_LUNFOLD

⊢ LPREFIX ll (LUNFOLD f n) ⇔
  case f n of
    NONE => ll = [||]
  | SOME (n,x) => ∀h t. ll = h:::t ⇒ h = x ∧ LPREFIX t (LUNFOLD f n)

LPREFIX_REFL

⊢ LPREFIX ll ll

LPREFIX_ANTISYM

⊢ LPREFIX l1 l2 ∧ LPREFIX l2 l1 ⇒ l1 = l2

LPREFIX_TRANS

⊢ LPREFIX l1 l2 ∧ LPREFIX l2 l3 ⇒ LPREFIX l1 l3

LPREFIX_fromList

⊢ ∀l ll.
      LPREFIX (fromList l) ll ⇔
      case toList ll of
        NONE => LTAKE (LENGTH l) ll = SOME l
      | SOME ys => l ≼ ys

prefixes_lprefix_total

⊢ ∀ll l1 l2. LPREFIX l1 ll ∧ LPREFIX l2 ll ⇒ LPREFIX l1 l2 ∨ LPREFIX l2 l1

LTAKE_IMP_LDROP

⊢ ∀n ll l1.
      LTAKE n ll = SOME l1 ⇒
      ∃l2. LDROP n ll = SOME l2 ∧ LAPPEND (fromList l1) l2 = ll

LDROP_EQ_LNIL

⊢ LDROP n ll = SOME [||] ⇔ LLENGTH ll = SOME n

LPREFIX_APPEND

⊢ LPREFIX l1 l2 ⇔ ∃ll. l2 = LAPPEND l1 ll

NOT_LFINITE_DROP_LFINITE

⊢ ∀n l t. ¬LFINITE l ∧ LDROP n l = SOME t ⇒ ¬LFINITE t

LDROP_APPEND1

⊢ LDROP n l1 = SOME l ⇒ LDROP n (LAPPEND l1 l2) = SOME (LAPPEND l l2)

LDROP_fromList

⊢ ∀ls n.
      LDROP n (fromList ls) =
      if n ≤ LENGTH ls then SOME (fromList (DROP n ls)) else NONE

LDROP_SUC

⊢ LDROP (SUC n) ls = OPTION_BIND (LDROP n ls) LTL

LHD_LGENLIST

⊢ LHD (LGENLIST f limopt) = if limopt = SOME 0 then NONE else SOME (f 0)

LTL_LGENLIST

⊢ LTL (LGENLIST f limopt) = if limopt = SOME 0 then NONE
  else SOME (LGENLIST (f ∘ SUC) (OPTION_MAP PRE limopt))

numopt_BISIMULATION

⊢ ∀mopt nopt.
      mopt = nopt ⇔
      ∃R.
          R mopt nopt ∧
          ∀m n.
              R m n ⇒
              m = SOME 0 ∧ n = SOME 0 ∨
              m ≠ SOME 0 ∧ n ≠ SOME 0 ∧
              R (OPTION_MAP PRE m) (OPTION_MAP PRE n)

LGENLIST_EQ_LNIL

⊢ (LGENLIST f n = [||] ⇔ n = SOME 0) ∧ ([||] = LGENLIST f n ⇔ n = SOME 0)

LFINITE_LGENLIST

⊢ LFINITE (LGENLIST f n) ⇔ n ≠ NONE

LTL_HD_LTL_LHD

⊢ LTL_HD l = OPTION_BIND (LHD l) (λh. OPTION_BIND (LTL l) (λt. SOME (t,h)))

LGENLIST_SOME

⊢ LGENLIST f (SOME 0) = [||] ∧
  ∀n. LGENLIST f (SOME (SUC n)) = f 0:::LGENLIST (f ∘ SUC) (SOME n)

LGENLIST_SOME_compute

⊢ LGENLIST f (SOME 0) = [||] ∧
  (∀n.
       LGENLIST f (SOME (NUMERAL (BIT1 n))) =
       f 0:::LGENLIST (f ∘ SUC) (SOME (NUMERAL (BIT1 n) − 1))) ∧
  ∀n.
      LGENLIST f (SOME (NUMERAL (BIT2 n))) =
      f 0:::LGENLIST (f ∘ SUC) (SOME (NUMERAL (BIT1 n)))

LNTH_LGENLIST

⊢ ∀n f lim.
      LNTH n (LGENLIST f lim) =
      case lim of
        NONE => SOME (f n)
      | SOME lim0 => if n < lim0 then SOME (f n) else NONE

LNTH_LMAP

⊢ ∀n f l. LNTH n (LMAP f l) = OPTION_MAP f (LNTH n l)

LLENGTH_LGENLIST

⊢ ∀f. LLENGTH (LGENLIST f limopt) = limopt

LMAP_LGENLIST

⊢ LMAP f (LGENLIST g limopt) = LGENLIST (f ∘ g) limopt

LGENLIST_EQ_CONS

⊢ LGENLIST f NONE = h:::t ⇔ h = f 0 ∧ t = LGENLIST (f ∘ $+ 1) NONE

LGENLIST_CHUNK_GENLIST

⊢ LGENLIST f NONE =
  LAPPEND (fromList (GENLIST f n)) (LGENLIST (f ∘ $+ n) NONE)

LREPEAT_thm

⊢ LREPEAT l = LAPPEND (fromList l) (LREPEAT l)

LREPEAT_NIL

⊢ LREPEAT [] = [||]

LREPEAT_EQ_LNIL

⊢ (LREPEAT l = [||] ⇔ l = []) ∧ ([||] = LREPEAT l ⇔ l = [])

LHD_LREPEAT

⊢ LHD (LREPEAT l) = LHD (fromList l)

LTL_LREPEAT

⊢ LTL (LREPEAT l) = OPTION_MAP (λt. LAPPEND t (LREPEAT l)) (LTL (fromList l))

LLENGTH_LREPEAT

⊢ LLENGTH (LREPEAT l) = if NULL l then SOME 0 else NONE