Theory "llist"

Signature

Definitions

LAPPEND

⊢ (∀x. LAPPEND [||] x = x) ∧ ∀h t x. LAPPEND (h:::t) x = h:::LAPPEND t x

LCONS

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

LDROP

⊢ (∀ll. LDROP 0 ll = SOME ll) ∧
  ∀n ll. LDROP (SUC n) ll = OPTION_JOIN (OPTION_MAP (LDROP n) (LTL 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))

LFINITE_def

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

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

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

LHD

⊢ ∀ll. LHD ll = llist_rep ll 0

LLENGTH

⊢ ∀ll. LLENGTH ll = if LFINITE ll then SOME (@n. llength_rel ll n) else NONE

LMAP

⊢ (∀f. LMAP f [||] = [||]) ∧ ∀f h t. LMAP f (h:::t) = f h:::LMAP f t

LNIL

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

LNTH

⊢ (∀ll. LNTH 0 ll = LHD ll) ∧
  ∀n ll. LNTH (SUC n) ll = OPTION_JOIN (OPTION_MAP (LNTH n) (LTL ll))

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

LREPEAT_def

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

LSET_def

⊢ ∀l x. LSET l x ⇔ ∃n. LNTH n l = SOME x

LSUFFIX_def

⊢ ∀xs zs. LSUFFIX xs zs ⇔ ∃ys. (xs = LAPPEND (fromList ys) zs) ∨ (zs = [||])

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)

LTL

⊢ ∀ll.
    LTL ll =
    case LHD ll of
      NONE => NONE
    | SOME v => SOME (llist_abs (λn. llist_rep ll (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)

LUNFOLD_def

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

LUNZIP_THM

⊢ (LUNZIP [||] = ([||],[||])) ∧
  ∀x y t. LUNZIP ((x,y):::t) = (let (ll1,ll2) = LUNZIP t in (x:::ll1,y:::ll2))

LZIP_THM

⊢ (∀l1. LZIP (l1,[||]) = [||]) ∧ (∀l2. LZIP ([||],l2) = [||]) ∧
  ∀h1 h2 t1 t2. LZIP (h1:::t1,h2:::t2) = (h1,h2):::LZIP (t1,t2)

always_def

⊢ always =
  (λP a0.
       ∃always'.
         always' a0 ∧
         ∀a0. always' a0 ⇒ ∃h t. (a0 = h:::t) ∧ P (h:::t) ∧ always' t)

eventually_def

⊢ eventually =
  (λP a0.
       ∀eventually'.
         (∀a0. P a0 ∨ (∃h t. (a0 = h:::t) ∧ eventually' t) ⇒ eventually' a0) ⇒
         eventually' a0)

every_def

⊢ ∀P ll. every P ll ⇔ ¬exists ($¬ ∘ P) 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)

fromList_def

⊢ (fromList [] = [||]) ∧ ∀h t. fromList (h::t) = h:::fromList t

fromSeq_def

⊢ ∀f. fromSeq f = LUNFOLD (λx. SOME (SUC x,f x)) 0

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

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)

llist_CASE_def

⊢ ∀ll b f.
    llist_CASE ll b f =
    case LTL_HD ll of NONE => b | SOME (ltl,lhd) => f lhd ltl

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)

llist_rel_def

⊢ ∀R l1 l2.
    llist_rel R l1 l2 ⇔
    (LLENGTH l1 = LLENGTH l2) ∧
    ∀i x y. (LNTH i l1 = SOME x) ∧ (LNTH i l2 = SOME y) ⇒ R x y

llist_upto_def

⊢ llist_upto =
  (λR a0 a1.
       ∀llist_upto'.
         (∀a0 a1.
            (a1 = a0) ∨ R a0 a1 ∨ (∃y. llist_upto' a0 y ∧ llist_upto' y a1) ∨
            (∃x y z. (a0 = LAPPEND z x) ∧ (a1 = LAPPEND z y) ∧ llist_upto' x y) ⇒
            llist_upto' a0 a1) ⇒
         llist_upto' a0 a1)

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)

toList

⊢ ∀ll. toList ll = if LFINITE ll then LTAKE (THE (LLENGTH ll)) ll else NONE

until_def

⊢ until =
  (λP Q a0.
       ∀until'.
         (∀a0. Q a0 ∨ (∃h t. (a0 = h:::t) ∧ P (h:::t) ∧ until' t) ⇒ until' a0) ⇒
         until' a0)

Theorems

LAPPEND_ASSOC

⊢ ∀ll1 ll2 ll3. LAPPEND (LAPPEND ll1 ll2) ll3 = LAPPEND ll1 (LAPPEND ll2 ll3)

LAPPEND_EQ_LNIL

⊢ (LAPPEND l1 l2 = [||]) ⇔ (l1 = [||]) ∧ (l2 = [||])

LAPPEND_NIL_2ND

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

LAPPEND_fromList

⊢ ∀l1 l2. LAPPEND (fromList l1) (fromList l2) = fromList (l1 ++ l2)

LAPPEND_fromSeq

⊢ (∀f ll. LAPPEND (fromSeq f) ll = fromSeq f) ∧
  ∀l f.
    LAPPEND (fromList l) (fromSeq f) =
    fromSeq (λn. if n < LENGTH l then EL n l else f (n − LENGTH l))

LCONS_11

⊢ ∀h1 t1 h2 t2. (h1:::t1 = h2:::t2) ⇔ (h1 = h2) ∧ (t1 = t2)

LCONS_NOT_NIL

⊢ ∀h t. h:::t ≠ [||] ∧ [||] ≠ h:::t

LDROP1_THM

⊢ LDROP 1 = LTL

LDROP_1

⊢ LDROP 1 (h:::t) = SOME t

LDROP_ADD

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

LDROP_APPEND1

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

LDROP_EQ_LNIL

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

LDROP_FUNPOW

⊢ ∀n ll. LDROP n ll = FUNPOW (λm. OPTION_BIND m LTL) n (SOME ll)

LDROP_LDROP

⊢ ∀ll k1 k2.
    ¬LFINITE ll ⇒
    (THE (LDROP k2 (THE (LDROP k1 ll))) = THE (LDROP k1 (THE (LDROP k2 ll))))

LDROP_NONE_LFINITE

⊢ (LDROP k l = NONE) ⇒ LFINITE l

LDROP_SOME_LLENGTH

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

LDROP_SUC

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

LDROP_THM

⊢ (∀ll. LDROP 0 ll = SOME ll) ∧ (∀n. LDROP (SUC n) [||] = NONE) ∧
  ∀n h t. LDROP (SUC n) (h:::t) = LDROP n t

LDROP_fromList

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

LDROP_fromSeq

⊢ ∀n f. LDROP n (fromSeq f) = SOME (fromSeq (f ∘ $+ n))

LFILTER_APPEND

⊢ ∀P ll1 ll2.
    LFINITE ll1 ⇒
    (LFILTER P (LAPPEND ll1 ll2) = LAPPEND (LFILTER P ll1) (LFILTER P ll2))

LFILTER_EQ_CONS

⊢ (LFILTER P ll = h:::t) ⇒
  ∃l ll'.
    (ll = LAPPEND (fromList l) (h:::ll')) ∧ EVERY ($¬ ∘ P) l ∧ P h ∧
    (LFILTER P ll' = t)

LFILTER_EQ_NIL

⊢ ∀ll. (LFILTER P ll = [||]) ⇔ every ($¬ ∘ P) ll

LFILTER_NIL

⊢ ∀P ll. every ($¬ ∘ P) ll ⇒ (LFILTER 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_fromList

⊢ ∀p l. LFILTER p (fromList l) = fromList (FILTER p l)

LFILTER_fromSeq

⊢ ∀p f.
    LFILTER p (fromSeq f) =
    if ∀i. ¬p (f i) then [||]
    else if p (f 0) then f 0:::LFILTER p (fromSeq (f ∘ SUC))
    else LFILTER p (fromSeq (f ∘ SUC))

LFINITE

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

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_HAS_LENGTH

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

LFINITE_IMP_fromList

⊢ ∀ll. LFINITE ll ⇒ ∃l. ll = fromList l

LFINITE_INDUCTION

⊢ ∀P. P [||] ∧ (∀h t. P t ⇒ P (h:::t)) ⇒ ∀a0. LFINITE a0 ⇒ P a0

LFINITE_LAPPEND_IMP_NIL

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

LFINITE_LFLATTEN

⊢ ∀lll.
    every (λll. LFINITE ll ∧ ll ≠ [||]) lll ⇒
    (LFINITE (LFLATTEN lll) ⇔ LFINITE lll)

LFINITE_LGENLIST

⊢ LFINITE (LGENLIST f n) ⇔ n ≠ NONE

LFINITE_LLENGTH

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

LFINITE_LNTH_NONE

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

LFINITE_MAP

⊢ ∀f ll. LFINITE (LMAP f ll) ⇔ LFINITE ll

LFINITE_STRONG_INDUCTION

⊢ P [||] ∧ (∀h t. LFINITE t ∧ P t ⇒ P (h:::t)) ⇒ ∀a0. LFINITE a0 ⇒ P a0

LFINITE_TAKE

⊢ ∀n ll. LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒ ∃y. LTAKE n ll = SOME y

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_fromList

⊢ ∀l. LFINITE (fromList l)

LFINITE_fromSeq

⊢ ∀f. ¬LFINITE (fromSeq f)

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)

LFINITE_strongind

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

LFINITE_toList

⊢ ∀ll. LFINITE ll ⇒ ∃l. toList ll = SOME l

LFINITE_toList_SOME

⊢ LFINITE ll ⇔ IS_SOME (toList ll)

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

LFLATTEN_THM

⊢ (LFLATTEN [||] = [||]) ∧ (∀tl. LFLATTEN ([||]:::t) = LFLATTEN t) ∧
  ∀h t tl. LFLATTEN ((h:::t):::tl) = h:::LFLATTEN (t:::tl)

LFLATTEN_fromList

⊢ ∀l. LFLATTEN (fromList (MAP fromList l)) = fromList (FLAT l)

LGENLIST_CHUNK_GENLIST

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

LGENLIST_EQ_CONS

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

LGENLIST_EQ_LNIL

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

LGENLIST_EQ_fromList

⊢ ∀f k. LGENLIST f (SOME k) = fromList (GENLIST f k)

LGENLIST_EQ_fromSeq

⊢ ∀f. LGENLIST f NONE = fromSeq f

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

LHDTL_CONS_THM

⊢ ∀h t. (LHD (h:::t) = SOME h) ∧ (LTL (h:::t) = SOME t)

LHDTL_EQ_SOME

⊢ ∀h t ll. (ll = h:::t) ⇔ (LHD ll = SOME h) ∧ (LTL ll = SOME t)

LHD_EQ_NONE

⊢ ∀ll. ((LHD ll = NONE) ⇔ (ll = [||])) ∧ ((NONE = LHD ll) ⇔ (ll = [||]))

LHD_LAPPEND

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

LHD_LCONS

⊢ LHD (h:::t) = SOME h

LHD_LGENLIST

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

LHD_LREPEAT

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

LHD_LUNFOLD

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

LHD_THM

⊢ (LHD [||] = NONE) ∧ ∀h t. LHD (h:::t) = SOME h

LHD_fromList

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

LHD_fromSeq

⊢ ∀f. LHD (fromSeq f) = SOME (f 0)

LLENGTH_0

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

LLENGTH_APPEND

⊢ ∀ll1 ll2.
    LLENGTH (LAPPEND ll1 ll2) =
    if LFINITE ll1 ∧ LFINITE ll2 then
      SOME (THE (LLENGTH ll1) + THE (LLENGTH ll2))
    else NONE

LLENGTH_LGENLIST

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

LLENGTH_LREPEAT

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

LLENGTH_MAP

⊢ ∀ll f. LLENGTH (LMAP f ll) = LLENGTH ll

LLENGTH_THM

⊢ (LLENGTH [||] = SOME 0) ∧ ∀h t. LLENGTH (h:::t) = OPTION_MAP SUC (LLENGTH t)

LLENGTH_fromList

⊢ ∀l. LLENGTH (fromList l) = SOME (LENGTH l)

LLENGTH_fromSeq

⊢ ∀f. LLENGTH (fromSeq f) = NONE

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_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_I

⊢ ∀ll2 ll1.
    (∃R. R ll1 ll2 ∧
         ∀ll3 ll4.
           R ll3 ll4 ⇒
           (ll3 = [||]) ∧ (ll4 = [||]) ∨
           (LHD ll3 = LHD ll4) ∧ R (THE (LTL ll3)) (THE (LTL ll4))) ⇒
    (ll1 = ll2)

LLIST_BISIM_UPTO

⊢ ∀ll1 ll2 R.
    R ll1 ll2 ∧
    (∀ll3 ll4.
       R ll3 ll4 ⇒
       (ll3 = [||]) ∧ (ll4 = [||]) ∨
       (LHD ll3 = LHD ll4) ∧ llist_upto R (THE (LTL ll3)) (THE (LTL ll4))) ⇒
    (ll1 = ll2)

LLIST_CASE_CONG

⊢ ∀M M' v f.
    (M = M') ∧ ((M' = [||]) ⇒ (v = v')) ∧
    (∀a0 a1. (M' = a0:::a1) ⇒ (f a0 a1 = f' a0 a1)) ⇒
    (llist_CASE M v f = llist_CASE M' v' f')

LLIST_CASE_EQ

⊢ (llist_CASE x v f = v') ⇔
  (x = [||]) ∧ (v = v') ∨ ∃a l. (x = a:::l) ∧ (f a l = v')

LLIST_DISTINCT

⊢ ∀a1 a0. [||] ≠ a0:::a1

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

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

LL_ALL_THM

⊢ (every P [||] ⇔ T) ∧ (every P (h:::t) ⇔ P h ∧ every P t)

LMAP_APPEND

⊢ ∀f ll1 ll2. LMAP f (LAPPEND ll1 ll2) = LAPPEND (LMAP f ll1) (LMAP f ll2)

LMAP_LGENLIST

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

LMAP_LUNFOLD

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

LMAP_MAP

⊢ ∀f g ll. LMAP f (LMAP g ll) = LMAP (f ∘ g) ll

LMAP_fromList

⊢ LMAP f (fromList l) = fromList (MAP f l)

LMAP_fromSeq

⊢ ∀f g. LMAP f (fromSeq g) = fromSeq (f ∘ g)

LNTH_ADD

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

LNTH_EQ

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

LNTH_HD_LDROP

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

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_LDROP

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

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_LLENGTH_NONE

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

LNTH_LMAP

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

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)

LNTH_NONE_MONO

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

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_fromList

⊢ ∀n xs. LNTH n (fromList xs) = if n < LENGTH xs then SOME (EL n xs) else NONE

LNTH_fromSeq

⊢ ∀n f. LNTH n (fromSeq f) = SOME (f n)

LNTH_rep

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

LPREFIX_ANTISYM

⊢ LPREFIX l1 l2 ∧ LPREFIX l2 l1 ⇒ (l1 = l2)

LPREFIX_APPEND

⊢ LPREFIX l1 l2 ⇔ ∃ll. l2 = LAPPEND l1 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_LNIL

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

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_NTH

⊢ LPREFIX l1 l2 ⇔ ∀i v. (LNTH i l1 = SOME v) ⇒ (LNTH i l2 = SOME v)

LPREFIX_REFL

⊢ LPREFIX ll ll

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

LREPEAT_EQ_LNIL

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

LREPEAT_NIL

⊢ LREPEAT [] = [||]

LREPEAT_thm

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

LSET

⊢ (LSET [||] = ∅) ∧ (LSET (x:::xs) = x INSERT LSET xs)

LSUFFIX

⊢ (LSUFFIX l [||] ⇔ T) ∧ (LSUFFIX [||] (y:::ys) ⇔ F) ∧
  (LSUFFIX (x:::xs) l ⇔ (x:::xs = l) ∨ LSUFFIX xs l)

LSUFFIX_ANTISYM

⊢ ∀x y. LSUFFIX x y ∧ LSUFFIX y x ∧ LFINITE x ⇒ (x = y)

LSUFFIX_REFL

⊢ ∀s. LSUFFIX s s

LSUFFIX_TRANS

⊢ ∀x y z. LSUFFIX x y ∧ LSUFFIX y z ⇒ LSUFFIX x z

LSUFFIX_fromList

⊢ ∀xs ys. LSUFFIX (fromList xs) (fromList ys) ⇔ IS_SUFFIX xs ys

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_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_LNTH

⊢ ∀n ll. (LTAKE n ll = NONE) ⇒ (LNTH n ll = NONE)

LTAKE_EQ_SOME_CONS

⊢ ∀n l x. (LTAKE n l = SOME x) ⇒ ∀h. ∃y. LTAKE n (h:::l) = SOME y

LTAKE_IMP_LDROP

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

LTAKE_LAPPEND1

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

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

LTAKE_LAPPEND_fromList

⊢ ∀ll l n.
    LTAKE (n + LENGTH l) (LAPPEND (fromList l) ll) =
    OPTION_MAP ($++ l) (LTAKE n ll)

LTAKE_LENGTH

⊢ ∀n ll l. (LTAKE n ll = SOME l) ⇒ (n = LENGTH 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)

LTAKE_LMAP

⊢ ∀n f ll. LTAKE n (LMAP f ll) = OPTION_MAP (MAP f) (LTAKE n ll)

LTAKE_LNTH_EL

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

LTAKE_LPREFIX

⊢ ∀x ll. ¬LFINITE ll ⇒ ∃l. (LTAKE x ll = SOME l) ∧ LPREFIX (fromList l) ll

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_NIL_EQ_NONE

⊢ ∀m. (LTAKE m [||] = NONE) ⇔ 0 < m

LTAKE_NIL_EQ_SOME

⊢ ∀l m. (LTAKE m [||] = SOME l) ⇔ (m = 0) ∧ (l = [])

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_TAKE_LESS

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

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_fromList

⊢ ∀l. LTAKE (LENGTH l) (fromList l) = SOME l

LTAKE_fromSeq

⊢ ∀n f. LTAKE n (fromSeq f) = SOME (GENLIST f n)

LTL_EQ_NONE

⊢ ∀ll. ((LTL ll = NONE) ⇔ (ll = [||])) ∧ ((NONE = LTL ll) ⇔ (ll = [||]))

LTL_HD_11

⊢ (LTL_HD ll1 = LTL_HD ll2) ⇒ (ll1 = ll2)

LTL_HD_HD

⊢ LHD ll = OPTION_MAP SND (LTL_HD ll)

LTL_HD_LCONS

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

LTL_HD_LNIL

⊢ LTL_HD [||] = NONE

LTL_HD_LTL_LHD

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

LTL_HD_LUNFOLD

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

LTL_HD_TL

⊢ LTL ll = OPTION_MAP FST (LTL_HD ll)

LTL_HD_iff

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

LTL_LAPPEND

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

LTL_LCONS

⊢ LTL (h:::t) = SOME t

LTL_LGENLIST

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

LTL_LREPEAT

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

LTL_LUNFOLD

⊢ LTL (LUNFOLD f x) = OPTION_MAP (LUNFOLD f ∘ FST) (f x)

LTL_THM

⊢ (LTL [||] = NONE) ∧ ∀h t. LTL (h:::t) = SOME t

LTL_fromList

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

LTL_fromSeq

⊢ ∀f. LTL (fromSeq f) = SOME (fromSeq (f ∘ SUC))

LUNFOLD

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

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

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)

LUNFOLD_LTL_HD

⊢ LUNFOLD LTL_HD 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))

LUNFOLD_UNIQUE

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

LZIP_LUNZIP

⊢ ∀ll. LZIP (LUNZIP ll) = ll

MONO_every

⊢ (∀x. P x ⇒ Q x) ⇒ every P l ⇒ every Q l

MONO_exists

⊢ (∀x. P x ⇒ Q x) ⇒ exists P l ⇒ exists Q l

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_DROP_LFINITE

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

NOT_LFINITE_IMP_fromSeq

⊢ ∀ll. ¬LFINITE ll ⇒ ∃f. ll = fromSeq f

NOT_LFINITE_NO_LENGTH

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

NOT_LFINITE_TAKE

⊢ ∀ll. ¬LFINITE ll ⇒ ∀n. ∃y. LTAKE n ll = SOME y

always_DROP

⊢ ∀ll. always P ll ⇒ always P (THE (LDROP k ll))

always_cases

⊢ ∀P a0. always P a0 ⇔ ∃h t. (a0 = h:::t) ∧ P (h:::t) ∧ always P t

always_coind

⊢ ∀P always'.
    (∀a0. always' a0 ⇒ ∃h t. (a0 = h:::t) ∧ P (h:::t) ∧ always' t) ⇒
    ∀a0. always' a0 ⇒ always P a0

always_conj_l

⊢ ∀ll. always (λx. P x ∧ Q x) ll ⇒ always P ll

always_eventually_ind

⊢ (∀ll. P ll ∨ ¬P ll ∧ Q (THE (LTL ll)) ⇒ Q ll) ⇒
  ∀ll. ll ≠ [||] ⇒ always (eventually P) ll ⇒ Q ll

always_rules

⊢ ∀P h t. P (h:::t) ∧ always P t ⇒ always P (h:::t)

always_thm

⊢ (always P [||] ⇔ F) ∧ ∀h t. always P (h:::t) ⇔ P (h:::t) ∧ always P t

eventually_cases

⊢ ∀P a0. eventually P a0 ⇔ P a0 ∨ ∃h t. (a0 = h:::t) ∧ eventually P t

eventually_ind

⊢ ∀P eventually'.
    (∀ll. P ll ⇒ eventually' ll) ∧ (∀h t. eventually' t ⇒ eventually' (h:::t)) ⇒
    ∀a0. eventually P a0 ⇒ eventually' a0

eventually_rules

⊢ ∀P. (∀ll. P ll ⇒ eventually P ll) ∧
      ∀h t. eventually P t ⇒ eventually P (h:::t)

eventually_strongind

⊢ ∀P eventually'.
    (∀ll. P ll ⇒ eventually' ll) ∧
    (∀h t. eventually P t ∧ eventually' t ⇒ eventually' (h:::t)) ⇒
    ∀a0. eventually P a0 ⇒ eventually' a0

eventually_thm

⊢ (eventually P [||] ⇔ P [||]) ∧
  (eventually P (h:::t) ⇔ P (h:::t) ∨ eventually P t)

eventually_until_EQN

⊢ eventually P = until (K T) P

every_LAPPEND1

⊢ ∀P ll1 ll2. every P (LAPPEND ll1 ll2) ⇒ every P ll1

every_LAPPEND2_LFINITE

⊢ ∀l P ll. LFINITE l ∧ every P (LAPPEND l ll) ⇒ every P ll

every_LDROP

⊢ ∀f i ll1 ll2. every f ll1 ∧ (LDROP i ll1 = SOME ll2) ⇒ every f ll2

every_LFILTER

⊢ ∀ll P. every P (LFILTER P ll)

every_LFILTER_imp

⊢ ∀Q P ll. every Q ll ⇒ every Q (LFILTER P ll)

every_LNTH

⊢ ∀P ll. every P ll ⇔ ∀n e. (LNTH n ll = SOME e) ⇒ P e

every_coind

⊢ ∀P Q. (∀h t. Q (h:::t) ⇒ P h ∧ Q t) ⇒ ∀ll. Q ll ⇒ every P ll

every_fromList_EVERY

⊢ ∀l P. every P (fromList l) ⇔ EVERY P l

every_fromSeq

⊢ ∀p f. every p (fromSeq f) ⇔ ∀i. p (f i)

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

every_thm

⊢ (every P [||] ⇔ T) ∧ (every P (h:::t) ⇔ P h ∧ every P t)

exists_LDROP

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

exists_LNTH

⊢ ∀l. exists P l ⇔ ∃n e. (SOME e = LNTH n l) ∧ P e

exists_cases

⊢ ∀P a0.
    exists P a0 ⇔ (∃h t. (a0 = h:::t) ∧ P h) ∨ ∃h t. (a0 = h:::t) ∧ exists P t

exists_fromSeq

⊢ ∀p f. exists p (fromSeq f) ⇔ ∃i. p (f i)

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_rules

⊢ ∀P. (∀h t. P h ⇒ exists P (h:::t)) ∧ ∀h t. exists P t ⇒ exists P (h:::t)

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_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_thm

⊢ (exists P [||] ⇔ F) ∧ (exists P (h:::t) ⇔ P h ∨ exists P t)

exists_thm_strong

⊢ exists P ll ⇔
  ∃n a t l.
    (LDROP n ll = SOME (a:::t)) ∧ P a ∧ (LTAKE n ll = SOME l) ∧
    EVERY ($¬ ∘ P) l

fromList_11

⊢ ∀xs ys. (fromList xs = fromList ys) ⇔ (xs = ys)

fromList_EQ_LNIL

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

fromList_NEQ_fromSeq

⊢ ∀l f. fromList l ≠ fromSeq f

fromList_fromSeq

⊢ ∀ll. (∃l. ll = fromList l) ∨ ∃f. ll = fromSeq f

fromSeq_11

⊢ ∀f g. (fromSeq f = fromSeq g) ⇔ (f = g)

fromSeq_LCONS

⊢ fromSeq f = f 0:::fromSeq (f ∘ SUC)

from_toList

⊢ ∀l. toList (fromList l) = SOME l

infinite_lnth_some

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

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)

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)

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_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_rules

⊢ llength_rel [||] 0 ∧ ∀h n t. llength_rel t n ⇒ llength_rel (h:::t) (SUC n)

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

llist_Axiom

⊢ ∀f. ∃g.
    (∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
    ∀x. LTL (g x) = OPTION_MAP (g ∘ 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_CASES

⊢ ∀l. (l = [||]) ∨ ∃h t. l = h:::t

llist_CASE_compute

⊢ (llist_CASE [||] b f = b) ∧ (llist_CASE (x:::ll) b f = f x ll)

llist_forall_split

⊢ ∀P. (∀ll. P ll) ⇔ (∀l. P (fromList l)) ∧ ∀f. P (fromSeq f)

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)

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_upto_cases

⊢ ∀R a0 a1.
    llist_upto R a0 a1 ⇔
    (a1 = a0) ∨ R a0 a1 ∨ (∃y. llist_upto R a0 y ∧ llist_upto R y a1) ∨
    ∃x y z. (a0 = LAPPEND z x) ∧ (a1 = LAPPEND z y) ∧ llist_upto R x y

llist_upto_context

⊢ ∀R x y z. llist_upto R x y ⇒ llist_upto R (LAPPEND z x) (LAPPEND z y)

llist_upto_eq

⊢ ∀R x. llist_upto R x x

llist_upto_ind

⊢ ∀R llist_upto'.
    (∀x. llist_upto' x x) ∧ (∀x y. R x y ⇒ llist_upto' x y) ∧
    (∀x y z. llist_upto' x y ∧ llist_upto' y z ⇒ llist_upto' x z) ∧
    (∀x y z. llist_upto' x y ⇒ llist_upto' (LAPPEND z x) (LAPPEND z y)) ⇒
    ∀a0 a1. llist_upto R a0 a1 ⇒ llist_upto' a0 a1

llist_upto_rel

⊢ ∀R x y. R x y ⇒ llist_upto R x y

llist_upto_rules

⊢ ∀R. (∀x. llist_upto R x x) ∧ (∀x y. R x y ⇒ llist_upto R x y) ∧
      (∀x y z. llist_upto R x y ∧ llist_upto R y z ⇒ llist_upto R x z) ∧
      ∀x y z. llist_upto R x y ⇒ llist_upto R (LAPPEND z x) (LAPPEND z y)

llist_upto_strongind

⊢ ∀R llist_upto'.
    (∀x. llist_upto' x x) ∧ (∀x y. R x y ⇒ llist_upto' x y) ∧
    (∀x y z.
       llist_upto R x y ∧ llist_upto' x y ∧ llist_upto R y z ∧ llist_upto' y z ⇒
       llist_upto' x z) ∧
    (∀x y z.
       llist_upto R x y ∧ llist_upto' x y ⇒
       llist_upto' (LAPPEND z x) (LAPPEND z y)) ⇒
    ∀a0 a1. llist_upto R a0 a1 ⇒ llist_upto' a0 a1

llist_upto_trans

⊢ ∀R x y z. llist_upto R x y ∧ llist_upto R y z ⇒ llist_upto R x z

lnth_fromList_some

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

lnth_some_down_closed

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

lrep_ok_FUNPOW_BIND

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

lrep_ok_MAP

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

lrep_ok_alt

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

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_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_rules

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

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)

prefixes_lprefix_total

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

toList_LAPPEND_APPEND

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

toList_THM

⊢ (toList [||] = SOME []) ∧
  ∀h t. toList (h:::t) = OPTION_MAP (CONS h) (toList t)

to_fromList

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

until_cases

⊢ ∀P Q a0. until P Q a0 ⇔ Q a0 ∨ ∃h t. (a0 = h:::t) ∧ P (h:::t) ∧ until P Q t

until_ind

⊢ ∀P Q until'.
    (∀ll. Q ll ⇒ until' ll) ∧ (∀h t. P (h:::t) ∧ until' t ⇒ until' (h:::t)) ⇒
    ∀a0. until P Q a0 ⇒ until' a0

until_rules

⊢ ∀P Q.
    (∀ll. Q ll ⇒ until P Q ll) ∧
    ∀h t. P (h:::t) ∧ until P Q t ⇒ until P Q (h:::t)

until_strongind

⊢ ∀P Q until'.
    (∀ll. Q ll ⇒ until' ll) ∧
    (∀h t. P (h:::t) ∧ until P Q t ∧ until' t ⇒ until' (h:::t)) ⇒
    ∀a0. until P Q a0 ⇒ until' a0