Package lazy-list: Lazy lists/colists/streams

Information

Files

• Package tarball lazy-list-0.3.tgz
• Theory file lazy-list.thy (included in the package tarball)

Defined Type Operator

• llist
  • llist.llist

Defined Constants

• llist
  • llist.every
  • llist.exists
  • llist.fromList
  • llist.linear_order_to_list_f
  • llist.llength_rel
  • llist.llist_abs
  • llist.llist_rep
  • llist.lrep_ok
  • llist.toList
  • llist.LAPPEND
  • llist.LCONS
  • llist.LDROP
  • llist.LFILTER
  • llist.LFINITE
  • llist.LFLATTEN
  • llist.LHD
  • llist.LLENGTH
  • llist.LMAP
  • llist.LNIL
  • llist.LNTH
  • llist.LTAKE
  • llist.LTL
  • llist.LUNFOLD
  • llist.LUNZIP
  • llist.LZIP

Theorems

⊦ ∀l. llist.LFINITE (llist.fromList l)

⊦ ∃rep. HOL4.TYPE_DEFINITION llist.lrep_ok rep

⊦ llist.LNIL = llist.llist_abs (λn. Data.Option.NONE)

⊦ llist.LDROP (Number.Numeral.bit1 Number.Numeral.zero) = llist.LTL

⊦ ∀ll. llist.LAPPEND ll llist.LNIL = ll

⊦ ∀ll. llist.LZIP (llist.LUNZIP ll) = ll

⊦ llist.LHD (llist.LCONS h t) = Data.Option.SOME h

⊦ llist.LTL (llist.LCONS h t) = Data.Option.SOME t

⊦ ∀ll. llist.LHD ll = llist.llist_rep ll Number.Numeral.zero

⊦ ∀h. llist.LFLATTEN (llist.LCONS h llist.LNIL) = h

⊦ ∀l. llist.toList (llist.fromList l) = Data.Option.SOME l

⊦ ∀l.
    llist.LLENGTH (llist.fromList l) =
    Data.Option.SOME (Data.List.length l)

⊦ ∀ll. ¬llist.LFINITE ll ⇒ llist.LLENGTH ll = Data.Option.NONE

⊦ ∀l.
    llist.LTAKE (Data.List.length l) (llist.fromList l) =
    Data.Option.SOME l

⊦ llist.LFINITE ll ⇔ ∃n. llist.LTAKE n ll = Data.Option.NONE

⊦ ∀ll f. llist.LLENGTH (llist.LMAP f ll) = llist.LLENGTH ll

⊦ ∀f ll. llist.LFINITE (llist.LMAP f ll) ⇔ llist.LFINITE ll

⊦ ∀m.
    llist.LTAKE m llist.LNIL = Data.Option.NONE ⇔
    Number.Natural.< Number.Numeral.zero m

⊦ ∀ll.
    llist.LFINITE ll ⇒
    llist.fromList (Data.Option.the (llist.toList ll)) = ll

⊦ ∀ll. llist.LFLATTEN ll = llist.LNIL ⇔ llist.every ((=) llist.LNIL) ll

⊦ ∀ll. llist.LFINITE ll ⇒ ∃n. llist.LLENGTH ll = Data.Option.SOME n

⊦ ∀ll. llist.LFINITE ll ⇒ ∃l. llist.toList ll = Data.Option.SOME l

⊦ ∀ll1 ll2. ¬llist.LFINITE ll1 ⇒ llist.LAPPEND ll1 ll2 = ll1

⊦ ∀h t.
    llist.LFLATTEN (llist.LCONS h t) = llist.LAPPEND h (llist.LFLATTEN t)

⊦ ∀ll. llist.LFILTER P ll = llist.LNIL ⇔ llist.every (Function.∘ (¬) P) ll

⊦ ∀ll1 ll2.
    llist.LFINITE (llist.LAPPEND ll1 ll2) ⇔
    llist.LFINITE ll1 ∧ llist.LFINITE ll2

⊦ ∀l1 l2.
    llist.LAPPEND (llist.fromList l1) (llist.fromList l2) =
    llist.fromList (Data.List.@ l1 l2)

⊦ ∀P ll. llist.every P ll ⇔ ¬llist.exists (Function.∘ (¬) P) ll

⊦ llist.LFINITE llist.LNIL ∧
  ∀h t. llist.LFINITE t ⇒ llist.LFINITE (llist.LCONS h t)

⊦ llist.LAPPEND l1 l2 = llist.LNIL ⇔ l1 = llist.LNIL ∧ l2 = llist.LNIL

⊦ ∀ll.
    llist.toList ll =
    if llist.LFINITE ll then
      llist.LTAKE (Data.Option.the (llist.LLENGTH ll)) ll
    else Data.Option.NONE

⊦ ∀l. l = llist.LNIL ∨ ∃h t. l = llist.LCONS h t

⊦ ∀n ll.
    llist.LTAKE n ll = Data.Option.NONE ⇒
    llist.LNTH n ll = Data.Option.NONE

⊦ ∀ll.
    llist.LLENGTH ll =
    if llist.LFINITE ll then
      Data.Option.SOME (select n. llist.llength_rel ll n)
    else Data.Option.NONE

⊦ ∀P ll.
    llist.every (Function.∘ (¬) P) ll ⇒ llist.LFILTER P ll = llist.LNIL

⊦ ∀ll. ¬llist.LFINITE ll ⇒ ∀n. ∃y. llist.LDROP n ll = Data.Option.SOME y

⊦ ∀ll. ¬llist.LFINITE ll ⇒ ∀n. ∃y. llist.LTAKE n ll = Data.Option.SOME y

⊦ (∀x. P x ⇒ Q x) ⇒ llist.every P l ⇒ llist.every Q l

⊦ (∀x. P x ⇒ Q x) ⇒ llist.exists P l ⇒ llist.exists Q l

⊦ (llist.LFINITE llist.LNIL ⇔ T) ∧
  ∀h t. llist.LFINITE (llist.LCONS h t) ⇔ llist.LFINITE t

⊦ llist.LHD llist.LNIL = Data.Option.NONE ∧
  ∀h t. llist.LHD (llist.LCONS h t) = Data.Option.SOME h

⊦ llist.LTL llist.LNIL = Data.Option.NONE ∧
  ∀h t. llist.LTL (llist.LCONS h t) = Data.Option.SOME t

⊦ ∀n ll l. llist.LTAKE n ll = Data.Option.SOME l ⇒ n = Data.List.length l

⊦ ∀ll1 ll2 ll3.
    llist.LAPPEND (llist.LAPPEND ll1 ll2) ll3 =
    llist.LAPPEND ll1 (llist.LAPPEND ll2 ll3)

⊦ ∀ll1 ll2. ll1 = ll2 ⇔ ∀n. llist.LNTH n ll1 = llist.LNTH n ll2

⊦ ∀ll1 ll2. ll1 = ll2 ⇔ ∀n. llist.LTAKE n ll1 = llist.LTAKE n ll2

⊦ ∀f g ll. llist.LMAP f (llist.LMAP g ll) = llist.LMAP (Function.∘ f g) ll

⊦ ∀h t. ¬(llist.LCONS h t = llist.LNIL) ∧ ¬(llist.LNIL = llist.LCONS h t)

⊦ ∀l m.
    llist.LTAKE m llist.LNIL = Data.Option.SOME l ⇔
    m = Number.Numeral.zero ∧ l = Data.List.[]

⊦ llist.fromList Data.List.[] = llist.LNIL ∧
  ∀h t.
    llist.fromList (Data.List.:: h t) = llist.LCONS h (llist.fromList t)

⊦ (∀a. llist.llist_abs (llist.llist_rep a) = a) ∧
  ∀r. llist.lrep_ok r ⇔ llist.llist_rep (llist.llist_abs r) = r

⊦ ∀ll.
    llist.LTL ll =
    Data.Option.case Data.Option.NONE
      (λv.
         Data.Option.SOME
           (llist.llist_abs
              (λn.
                 llist.llist_rep ll
                   (Number.Natural.+ n
                      (Number.Numeral.bit1 Number.Numeral.zero)))))
      (llist.LHD ll)

⊦ ∀l. llist.exists P l ⇔ ∃n e. Data.Option.SOME e = llist.LNTH n l ∧ P e

⊦ ∀f ll1 ll2.
    llist.LMAP f (llist.LAPPEND ll1 ll2) =
    llist.LAPPEND (llist.LMAP f ll1) (llist.LMAP f ll2)

⊦ llist.llist_rep (llist.LCONS h t) =
  λn.
    if n = Number.Numeral.zero then Data.Option.SOME h
    else
      llist.llist_rep t
        (Number.Natural.- n (Number.Numeral.bit1 Number.Numeral.zero))

⊦ ∀h t.
    llist.LHD (llist.LCONS h t) = Data.Option.SOME h ∧
    llist.LTL (llist.LCONS h t) = Data.Option.SOME t

⊦ llist.LLENGTH llist.LNIL = Data.Option.SOME Number.Numeral.zero ∧
  ∀h t.
    llist.LLENGTH (llist.LCONS h t) =
    Data.Option.map Number.Natural.suc (llist.LLENGTH t)

⊦ (llist.every P llist.LNIL ⇔ T) ∧
  (llist.every P (llist.LCONS h t) ⇔ P h ∧ llist.every P t)

⊦ (llist.exists P llist.LNIL ⇔ F) ∧
  (llist.exists P (llist.LCONS h t) ⇔ P h ∨ llist.exists P t)

⊦ ∀ll.
    (llist.LHD ll = Data.Option.NONE ⇔ ll = llist.LNIL) ∧
    (Data.Option.NONE = llist.LHD ll ⇔ ll = llist.LNIL)

⊦ ∀ll.
    (llist.LTL ll = Data.Option.NONE ⇔ ll = llist.LNIL) ∧
    (Data.Option.NONE = llist.LTL ll ⇔ ll = llist.LNIL)

⊦ llist.llength_rel llist.LNIL Number.Numeral.zero ∧
  ∀h n t.
    llist.llength_rel t n ⇒
    llist.llength_rel (llist.LCONS h t) (Number.Natural.suc n)

⊦ ∀f.
    ∃g.
      ∀x.
        g x =
        Data.Option.case llist.LNIL
          (λv. Data.Pair.case (λa b. llist.LCONS b (g a)) v) (f x)

⊦ ∀f.
    ∃!g.
      ∀x.
        g x =
        Data.Option.case llist.LNIL
          (λv. Data.Pair.case (λa b. llist.LCONS b (g a)) v) (f x)

⊦ llist.toList llist.LNIL = Data.Option.SOME Data.List.[] ∧
  ∀h t.
    llist.toList (llist.LCONS h t) =
    Data.Option.map (Data.List.:: h) (llist.toList t)

⊦ ∀n l x.
    llist.LNTH n l = Data.Option.SOME x ⇒
    llist.LHD (Data.Option.the (llist.LDROP n l)) = Data.Option.SOME x

⊦ ∀n ll.
    llist.LFINITE ll ∧
    Number.Natural.≤ n (Data.Option.the (llist.LLENGTH ll)) ⇒
    ∃y. llist.LDROP n ll = Data.Option.SOME y

⊦ ∀n ll.
    llist.LFINITE ll ∧
    Number.Natural.≤ n (Data.Option.the (llist.LLENGTH ll)) ⇒
    ∃y. llist.LTAKE n ll = Data.Option.SOME y

⊦ ∀a0.
    llist.LFINITE a0 ⇔
    a0 = llist.LNIL ∨ ∃h t. a0 = llist.LCONS h t ∧ llist.LFINITE t

⊦ ∀f x.
    llist.LUNFOLD f x =
    Data.Option.case llist.LNIL
      (λv. Data.Pair.case (λv1 v2. llist.LCONS v2 (llist.LUNFOLD f v1)) v)
      (f x)

⊦ llist.exists P ll ⇔
  ∃n a t. llist.LDROP n ll = Data.Option.SOME (llist.LCONS a t) ∧ P a

⊦ ∀h t.
    llist.LCONS h t =
    llist.llist_abs
      (λn.
         if n = Number.Numeral.zero then Data.Option.SOME h
         else
           llist.llist_rep t
             (Number.Natural.- n
                (Number.Numeral.bit1 Number.Numeral.zero)))

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

⊦ ∀h1 t1 h2 t2. llist.LCONS h1 t1 = llist.LCONS h2 t2 ⇔ h1 = h2 ∧ t1 = t2

⊦ ∀h t ll.
    ll = llist.LCONS h t ⇔
    llist.LHD ll = Data.Option.SOME h ∧ llist.LTL ll = Data.Option.SOME t

⊦ ∀f g s.
    llist.LMAP f (llist.LUNFOLD g s) =
    llist.LUNFOLD
      (λs.
         Data.Option.map (Data.Pair.uncurry (λx y. Data.Pair., x (f y)))
           (g s)) s

⊦ ∀LFINITE'.
    LFINITE' llist.LNIL ∧ (∀h t. LFINITE' t ⇒ LFINITE' (llist.LCONS h t)) ⇒
    ∀a0. llist.LFINITE a0 ⇒ LFINITE' a0

⊦ ∀n l x.
    llist.LTAKE n l = Data.Option.SOME x ⇒
    ∀h. ∃y. llist.LTAKE n (llist.LCONS h l) = Data.Option.SOME y

⊦ (∀ll. llist.LNTH Number.Numeral.zero ll = llist.LHD ll) ∧
  ∀n ll.
    llist.LNTH (Number.Natural.suc n) ll =
    Data.Option.join (Data.Option.map (llist.LNTH n) (llist.LTL ll))

⊦ (∀ll. llist.LDROP Number.Numeral.zero ll = Data.Option.SOME ll) ∧
  ∀n ll.
    llist.LDROP (Number.Natural.suc n) ll =
    Data.Option.join (Data.Option.map (llist.LDROP n) (llist.LTL ll))

⊦ ∀ll1 ll2.
    llist.LLENGTH (llist.LAPPEND ll1 ll2) =
    if llist.LFINITE ll1 ∧ llist.LFINITE ll2 then
      Data.Option.SOME
        (Number.Natural.+ (Data.Option.the (llist.LLENGTH ll1))
           (Data.Option.the (llist.LLENGTH ll2)))
    else Data.Option.NONE

⊦ (∀x. llist.LAPPEND llist.LNIL x = x) ∧
  ∀h t x.
    llist.LAPPEND (llist.LCONS h t) x = llist.LCONS h (llist.LAPPEND t x)

⊦ P llist.LNIL ∧ (∀h t. llist.LFINITE t ∧ P t ⇒ P (llist.LCONS h t)) ⇒
  ∀ll1. llist.LFINITE ll1 ⇒ P ll1

⊦ ∀m h t.
    llist.LTAKE m (llist.LCONS h t) = Data.Option.NONE ⇔
    ∃n. m = Number.Natural.suc n ∧ llist.LTAKE n t = Data.Option.NONE

⊦ (∀f. llist.LMAP f llist.LNIL = llist.LNIL) ∧
  ∀f h t.
    llist.LMAP f (llist.LCONS h t) = llist.LCONS (f h) (llist.LMAP f t)

⊦ ∀P Q.
    (∀h t. Q (llist.LCONS h t) ⇒ P h ∧ Q t) ⇒ ∀ll. Q ll ⇒ llist.every P ll

⊦ ∀n ll.
    llist.LTAKE (Number.Natural.suc n) ll =
    Data.Option.case Data.Option.NONE
      (λl.
         Data.Option.case Data.Option.NONE
           (λe.
              Data.Option.SOME
                (Data.List.@ l (Data.List.:: e Data.List.[])))
           (llist.LNTH n ll)) (llist.LTAKE n ll)

⊦ ∀LFINITE'.
    LFINITE' llist.LNIL ∧
    (∀h t. llist.LFINITE t ∧ LFINITE' t ⇒ LFINITE' (llist.LCONS h t)) ⇒
    ∀a0. llist.LFINITE a0 ⇒ LFINITE' a0

⊦ ∀f.
    ∃g.
      (∀x. llist.LHD (g x) = Data.Option.map Data.Pair.snd (f x)) ∧
      ∀x.
        llist.LTL (g x) =
        Data.Option.map (Function.∘ g Data.Pair.fst) (f x)

⊦ ∀f.
    ∃!g.
      (∀x. llist.LHD (g x) = Data.Option.map Data.Pair.snd (f x)) ∧
      ∀x.
        llist.LTL (g x) =
        Data.Option.map (Function.∘ g Data.Pair.fst) (f x)

⊦ ∀P.
    (∀h t. P h ⇒ llist.exists P (llist.LCONS h t)) ∧
    ∀h t. llist.exists P t ⇒ llist.exists P (llist.LCONS h t)

⊦ llist.LFINITE =
  λa0.
    ∀LFINITE'.
      (∀a0.
         a0 = llist.LNIL ∨ (∃h t. a0 = llist.LCONS h t ∧ LFINITE' t) ⇒
         LFINITE' a0) ⇒ LFINITE' a0

⊦ (∀P. llist.LFILTER P llist.LNIL = llist.LNIL) ∧
  ∀P h t.
    llist.LFILTER P (llist.LCONS h t) =
    if P h then llist.LCONS h (llist.LFILTER P t) else llist.LFILTER P t

⊦ llist.LUNZIP llist.LNIL = Data.Pair., llist.LNIL llist.LNIL ∧
  ∀x y t.
    llist.LUNZIP (llist.LCONS (Data.Pair., x y) t) =
    let
      (Data.Pair.uncurry
         (λll1 ll2. Data.Pair., (llist.LCONS x ll1) (llist.LCONS y ll2)))
      (llist.LUNZIP t)

⊦ ∀P a0.
    llist.exists P a0 ⇔
    (∃h t. a0 = llist.LCONS h t ∧ P h) ∨
    ∃h t. a0 = llist.LCONS h t ∧ llist.exists P t

⊦ ∀lo.
    llist.linear_order_to_list_f lo =
    let
      (λmin.
         if min = Set.∅ then Data.Option.NONE
         else
           Data.Option.SOME
             (Data.Pair.,
                (Relation.restrict lo
                   (Set.- (Set.∪ (Relation.domain lo) (Relation.range lo))
                      min)) (Set.choice min)))
      (Relation.minimalElements
         (Set.∪ (Relation.domain lo) (Relation.range lo)) lo)

⊦ ∀llength_rel'.
    llength_rel' llist.LNIL Number.Numeral.zero ∧
    (∀h n t.
       llength_rel' t n ⇒
       llength_rel' (llist.LCONS h t) (Number.Natural.suc n)) ⇒
    ∀a0 a1. llist.llength_rel a0 a1 ⇒ llength_rel' a0 a1

⊦ (∀ll. llist.LDROP Number.Numeral.zero ll = Data.Option.SOME ll) ∧
  (∀n. llist.LDROP (Number.Natural.suc n) llist.LNIL = Data.Option.NONE) ∧
  ∀n h t.
    llist.LDROP (Number.Natural.suc n) (llist.LCONS h t) = llist.LDROP n t

⊦ ∀P ll.
    llist.LFILTER P ll =
    if ¬llist.exists P ll then llist.LNIL
    else if P (Data.Option.the (llist.LHD ll)) then
      llist.LCONS (Data.Option.the (llist.LHD ll))
        (llist.LFILTER P (Data.Option.the (llist.LTL ll)))
    else llist.LFILTER P (Data.Option.the (llist.LTL ll))

⊦ llist.LFLATTEN llist.LNIL = llist.LNIL ∧
  (∀tl. llist.LFLATTEN (llist.LCONS llist.LNIL t) = llist.LFLATTEN t) ∧
  ∀h t tl.
    llist.LFLATTEN (llist.LCONS (llist.LCONS h t) tl) =
    llist.LCONS h (llist.LFLATTEN (llist.LCONS t tl))

⊦ ∀P exists'.
    (∀h t. P h ⇒ exists' (llist.LCONS h t)) ∧
    (∀h t. exists' t ⇒ exists' (llist.LCONS h t)) ⇒
    ∀a0. llist.exists P a0 ⇒ exists' a0

⊦ (∀ll.
     llist.LTAKE Number.Numeral.zero ll = Data.Option.SOME Data.List.[]) ∧
  ∀n ll.
    llist.LTAKE (Number.Natural.suc n) ll =
    Data.Option.case Data.Option.NONE
      (λhd.
         Data.Option.case Data.Option.NONE
           (λtl. Data.Option.SOME (Data.List.:: hd tl))
           (llist.LTAKE n (Data.Option.the (llist.LTL ll)))) (llist.LHD ll)

⊦ ∀a0 a1.
    llist.llength_rel a0 a1 ⇔
    a0 = llist.LNIL ∧ a1 = Number.Numeral.zero ∨
    ∃h n t.
      a0 = llist.LCONS h t ∧ a1 = Number.Natural.suc n ∧
      llist.llength_rel t n

⊦ ∀f x v1 v2.
    (f x = Data.Option.NONE ⇒ llist.LUNFOLD f x = llist.LNIL) ∧
    (f x = Data.Option.SOME (Data.Pair., v1 v2) ⇒
     llist.LUNFOLD f x = llist.LCONS v2 (llist.LUNFOLD f v1))

⊦ (∀n. llist.LNTH n llist.LNIL = Data.Option.NONE) ∧
  (∀h t.
     llist.LNTH Number.Numeral.zero (llist.LCONS h t) =
     Data.Option.SOME h) ∧
  ∀n h t.
    llist.LNTH (Number.Natural.suc n) (llist.LCONS h t) = llist.LNTH n t

⊦ (∀ll.
     llist.LTAKE Number.Numeral.zero ll = Data.Option.SOME Data.List.[]) ∧
  (∀n. llist.LTAKE (Number.Natural.suc n) llist.LNIL = Data.Option.NONE) ∧
  ∀n h t.
    llist.LTAKE (Number.Natural.suc n) (llist.LCONS h t) =
    Data.Option.map (Data.List.:: h) (llist.LTAKE n t)

⊦ ∀llength_rel'.
    llength_rel' llist.LNIL Number.Numeral.zero ∧
    (∀h n t.
       llist.llength_rel t n ∧ llength_rel' t n ⇒
       llength_rel' (llist.LCONS h t) (Number.Natural.suc n)) ⇒
    ∀a0 a1. llist.llength_rel a0 a1 ⇒ llength_rel' a0 a1

⊦ llist.exists =
  λP a0.
    ∀exists'.
      (∀a0.
         (∃h t. a0 = llist.LCONS h t ∧ P h) ∨
         (∃h t. a0 = llist.LCONS h t ∧ exists' t) ⇒ exists' a0) ⇒
      exists' a0

⊦ ∀P Q.
    (∀h t. P h ⇒ Q (llist.LCONS h t)) ∧
    (∀h t. Q t ∧ llist.exists P t ⇒ Q (llist.LCONS h t)) ⇒
    ∀ll. llist.exists P ll ⇒ Q ll

⊦ ∀P exists'.
    (∀h t. P h ⇒ exists' (llist.LCONS h t)) ∧
    (∀h t. llist.exists P t ∧ exists' t ⇒ exists' (llist.LCONS h t)) ⇒
    ∀a0. llist.exists P a0 ⇒ exists' a0

⊦ ∀P Q.
    (∀h t. Q (llist.LCONS h t) ⇒ P h) ∧
    (∀h t. Q (llist.LCONS h t) ⇒ Q t ∨ llist.every P t) ⇒
    ∀ll. Q ll ⇒ llist.every P ll

⊦ ∀ll.
    llist.LFLATTEN ll =
    if llist.every ((=) llist.LNIL) ll then llist.LNIL
    else if Data.Option.the (llist.LHD ll) = llist.LNIL then
      llist.LFLATTEN (Data.Option.the (llist.LTL ll))
    else
      llist.LCONS
        (Data.Option.the (llist.LHD (Data.Option.the (llist.LHD ll))))
        (llist.LFLATTEN
           (llist.LCONS
              (Data.Option.the
                 (llist.LTL (Data.Option.the (llist.LHD ll))))
              (Data.Option.the (llist.LTL ll))))

⊦ ∀f.
    llist.lrep_ok f ⇔
    ∃P.
      (∀g.
         P g ⇒
         g = (λn. Data.Option.NONE) ∨
         ∃h t.
           P t ∧
           g =
           λn.
             if n = Number.Numeral.zero then Data.Option.SOME h
             else
               t
                 (Number.Natural.- n
                    (Number.Numeral.bit1 Number.Numeral.zero))) ∧ P f

⊦ ∀f g.
    (∀x.
       f x = llist.LNIL ∧ g x = llist.LNIL ∨
       ∃h y. f x = llist.LCONS h (f y) ∧ g x = llist.LCONS h (g y)) ⇒
    ∀x. f x = g x

⊦ (∀l1. llist.LZIP (Data.Pair., l1 llist.LNIL) = llist.LNIL) ∧
  (∀l2. llist.LZIP (Data.Pair., llist.LNIL l2) = llist.LNIL) ∧
  ∀h1 h2 t1 t2.
    llist.LZIP (Data.Pair., (llist.LCONS h1 t1) (llist.LCONS h2 t2)) =
    llist.LCONS (Data.Pair., h1 h2) (llist.LZIP (Data.Pair., t1 t2))

⊦ ∀ll1 ll2.
    ll1 = ll2 ⇔
    ∃R.
      R ll1 ll2 ∧
      ∀ll3 ll4.
        R ll3 ll4 ⇒
        ll3 = llist.LNIL ∧ ll4 = llist.LNIL ∨
        llist.LHD ll3 = llist.LHD ll4 ∧
        R (Data.Option.the (llist.LTL ll3))
          (Data.Option.the (llist.LTL ll4))

⊦ llist.llength_rel =
  λa0 a1.
    ∀llength_rel'.
      (∀a0 a1.
         a0 = llist.LNIL ∧ a1 = Number.Numeral.zero ∨
         (∃h n t.
            a0 = llist.LCONS h t ∧ a1 = Number.Natural.suc n ∧
            llength_rel' t n) ⇒ llength_rel' a0 a1) ⇒ llength_rel' a0 a1

⊦ ∀m h t l.
    llist.LTAKE m (llist.LCONS h t) = Data.Option.SOME l ⇔
    m = Number.Numeral.zero ∧ l = Data.List.[] ∨
    ∃n l'.
      m = Number.Natural.suc n ∧ llist.LTAKE n t = Data.Option.SOME l' ∧
      l = Data.List.:: h l'

⊦ ∀ll1 ll2.
    ll1 = ll2 ⇔
    ∃R.
      R ll1 ll2 ∧
      ∀ll3 ll4.
        R ll3 ll4 ⇒
        ll3 = ll4 ∨
        ∃h t1 t2. ll3 = llist.LCONS h t1 ∧ ll4 = llist.LCONS h t2 ∧ R t1 t2

⊦ (∀n ll.
     ¬llist.LFINITE ll ⇒
     llist.LAPPEND (llist.fromList (Data.Option.the (llist.LTAKE n ll)))
       (Data.Option.the (llist.LDROP n ll)) = ll) ∧
  ∀n ll.
    llist.LFINITE ll ∧
    Number.Natural.≤ n (Data.Option.the (llist.LLENGTH ll)) ⇒
    llist.LAPPEND (llist.fromList (Data.Option.the (llist.LTAKE n ll)))
      (Data.Option.the (llist.LDROP n ll)) = ll

⊦ ∀ll1 ll2.
    ll1 = ll2 ⇔
    ∃R.
      R ll1 ll2 ∧
      ∀ll3 ll4.
        R ll3 ll4 ⇒
        ll3 = llist.LNIL ∧ ll4 = llist.LNIL ∨
        ∃h t1 t2. ll3 = llist.LCONS h t1 ∧ ll4 = llist.LCONS h t2 ∧ R t1 t2

⊦ ∀R f s ll.
    R s ll ∧
    (∀s ll.
       R s ll ⇒
       f s = Data.Option.NONE ∧ ll = llist.LNIL ∨
       ∃s' x ll'.
         f s = Data.Option.SOME (Data.Pair., s' x) ∧
         llist.LHD ll = Data.Option.SOME x ∧
         llist.LTL ll = Data.Option.SOME ll' ∧ R s' ll') ⇒
    llist.LUNFOLD f s = ll

⊦ ∀lo X.
    Relation.linearOrder lo X ∧ Relation.finitePrefixes lo X ⇒
    ∃ll.
      X =
      Set.specification
        (λx. Data.Pair., x (∃i. llist.LNTH i ll = Data.Option.SOME x)) ∧
      Set.⊆ lo
        (Set.specification
           (Data.Pair.uncurry
              (λx y.
                 Data.Pair., (Data.Pair., x y)
                   (∃i j.
                      Number.Natural.≤ i j ∧
                      llist.LNTH i ll = Data.Option.SOME x ∧
                      llist.LNTH j ll = Data.Option.SOME y)))) ∧
      ∀i j x.
        llist.LNTH i ll = Data.Option.SOME x ∧
        llist.LNTH j ll = Data.Option.SOME x ⇒ i = j

Input Type Operators

• →
• bool
• Data
  • List
    • Data.List.list
  • Option
    • Data.Option.option
  • Pair
    • Data.Pair.×
• Number
  • Natural
    • Number.Natural.natural

Input Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ∃!
    • ∨
    • ¬
    • cond
    • let
    • select
    • F
    • T
  • List
    • Data.List.::
    • Data.List.@
    • Data.List.[]
    • Data.List.length
  • Option
    • Data.Option.case
    • Data.Option.join
    • Data.Option.map
    • Data.Option.the
    • Data.Option.NONE
    • Data.Option.SOME
  • Pair
    • Data.Pair.,
    • Data.Pair.case
    • Data.Pair.fst
    • Data.Pair.snd
    • Data.Pair.uncurry
• Function
  • Function.id
  • Function.∘
  • Combinator
    • Function.Combinator.c
    • Function.Combinator.s
• HOL4
  • Numeral
    • HOL4.Numeral.iiSUC
  • HOL4.TYPE_DEFINITION
• Number
  • Natural
    • Number.Natural.*
    • Number.Natural.+
    • Number.Natural.-
    • Number.Natural.<
    • Number.Natural.≤
    • Number.Natural.>
    • Number.Natural.≥
    • Number.Natural.even
    • Number.Natural.exp
    • Number.Natural.odd
    • Number.Natural.pre
    • Number.Natural.suc
  • Numeral
    • Number.Numeral.bit1
    • Number.Numeral.bit2
    • Number.Numeral.zero
• Relation
  • Relation.antisymmetric
  • Relation.domain
  • Relation.finitePrefixes
  • Relation.linearOrder
  • Relation.minimalElements
  • Relation.range
  • Relation.restrict
  • Relation.transitive
• Set
  • Set.-
  • Set.∅
  • Set.choice
  • Set.finite
  • Set.in
  • Set.insert
  • Set.⊂
  • Set.singleton
  • Set.specification
  • Set.⊆
  • Set.∪
• While
  • While.least
  • While.while

Assumptions

⊦ T

⊦ ∀x. x = x

⊦ ∀x. x ⇔ x

⊦ ∀t. F ⇒ t

⊦ ∀n. Number.Natural.≤ Number.Numeral.zero n

⊦ ∀s. Set.⊆ s s

⊦ ¬(t ∧ ¬t)

⊦ Number.Numeral.bit1 Number.Numeral.zero =
  Number.Natural.suc Number.Numeral.zero

⊦ ¬¬p ⇒ p

⊦ ∀x. ¬Set.in x Set.∅

⊦ ∀x. Function.id x = x

⊦ ∀t. t ∨ ¬t

⊦ ∀n. ¬Number.Natural.< n Number.Numeral.zero

⊦ ∀n. Number.Natural.< Number.Numeral.zero (Number.Natural.suc n)

⊦ (¬) = λt. t ⇒ F

⊦ (∃) = λP. P ((select) P)

⊦ ∀a. ∃x. x = a

⊦ ∀t. (∀x. t) ⇔ t

⊦ ∀t. (∃x. t) ⇔ t

⊦ ∀t. (λx. t x) = t

⊦ (∀) = λP. P = λx. T

⊦ Number.Numeral.bit2 Number.Numeral.zero =
  Number.Natural.suc (Number.Numeral.bit1 Number.Numeral.zero)

⊦ ¬(p ⇒ q) ⇒ p

⊦ ∀x. ¬(Data.Option.NONE = Data.Option.SOME x)

⊦ ∀x. ¬(Data.Option.SOME x = Data.Option.NONE)

⊦ ∀x. Data.Option.the (Data.Option.SOME x) = x

⊦ ∀x. x = x ⇔ T

⊦ ∀t. ¬¬t ⇔ t

⊦ ∀n. ¬(Number.Natural.suc n = Number.Numeral.zero)

⊦ ∀n. ¬Number.Natural.≤ (Number.Natural.suc n) Number.Numeral.zero

⊦ Function.Combinator.c = λf x y. f y x

⊦ ¬(p ⇒ q) ⇒ ¬q

⊦ ¬(p ∨ q) ⇒ ¬p

⊦ ¬(p ∨ q) ⇒ ¬q

⊦ ∀x. Set.choice (Set.insert x Set.∅) = x

⊦ ∀A. A ⇒ ¬A ⇒ F

⊦ ∀t. ¬t ⇒ t ⇒ F

⊦ ∀t. (t ⇒ F) ⇒ ¬t

⊦ Function.Combinator.s = λf g x. f x (g x)

⊦ ∀x. (select y. y = x) = x

⊦ ∀s t. Set.⊆ (Set.- s t) s

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ (∀) (Data.Pair.uncurry f) ⇔ (∀) (Function.∘ (∀) f)

⊦ ∀t. t ⇒ F ⇔ t ⇔ F

⊦ ∀t. (t ⇔ T) ∨ (t ⇔ F)

⊦ ∀n.
    Number.Natural.suc n =
    Number.Natural.+ (Number.Numeral.bit1 Number.Numeral.zero) n

⊦ ∀m.
    Number.Natural.- (Number.Natural.suc m)
      (Number.Numeral.bit1 Number.Numeral.zero) = m

⊦ ∀x. Data.Pair., (Data.Pair.fst x) (Data.Pair.snd x) = x

⊦ ∀x y. Data.Pair.fst (Data.Pair., x y) = x

⊦ ∀x y. Data.Pair.snd (Data.Pair., x y) = y

⊦ ∀x s. ¬(Set.insert x s = Set.∅)

⊦ ∀f x. let f x = f x

⊦ ∀P x. P x ⇒ P ((select) P)

⊦ Function.∘ f (λx. g x) = λx. f (g x)

⊦ Function.Combinator.c (λx. f x) y = λx. f x y

⊦ Data.Pair.case f (Data.Pair., x y) = f x y

⊦ Data.Pair.uncurry f = Data.Pair.uncurry g ⇔ f = g

⊦ ∀x. ∃q r. x = Data.Pair., q r

⊦ ∀x y. x = y ⇔ y = x

⊦ ∀A B. A ∨ B ⇔ B ∨ A

⊦ ∀m n. Number.Natural.+ m n = Number.Natural.+ n m

⊦ ∀a c. Number.Natural.- (Number.Natural.+ a c) c = a

⊦ P (let f v) = let (Function.∘ P f) v

⊦ let f v x = let (Function.Combinator.c f x) v

⊦ Function.∘ f (Data.Pair.uncurry g) =
  Data.Pair.uncurry (Function.∘ (Function.∘ f) g)

⊦ (¬A ⇒ F) ⇒ (A ⇒ F) ⇒ F

⊦ Function.Combinator.s f (λx. g x) = λx. f x (g x)

⊦ ∀s. ¬(s = Set.∅) ⇒ Set.in (Set.choice s) s

⊦ ∀f g. Function.∘ f g = λx. f (g x)

⊦ ∀P.
    While.least P =
    While.while (Function.∘ (¬) P) Number.Natural.suc Number.Numeral.zero

⊦ Set.specification (λx. Data.Pair., x (x = y)) = Set.insert y Set.∅

⊦ ∀A B. A ⇒ B ⇔ ¬A ∨ B

⊦ ∀m n. ¬Number.Natural.< m n ⇔ Number.Natural.≤ n m

⊦ ∀m. m = Number.Numeral.zero ∨ ∃n. m = Number.Natural.suc n

⊦ ∀opt. opt = Data.Option.NONE ∨ ∃x. opt = Data.Option.SOME x

⊦ ∀s. Set.singleton s ⇔ ∃x. s = Set.insert x Set.∅

⊦ (∧) = λp q. (λf. f p q) = λf. f T T

⊦ Function.Combinator.c (Data.Pair.uncurry f) x =
  Data.Pair.uncurry
    (Function.Combinator.c (Function.∘ Function.Combinator.c f) x)

⊦ ∀P. ¬(∀x. P x) ⇔ ∃x. ¬P x

⊦ ∀P. ¬(∃x. P x) ⇔ ∀x. ¬P x

⊦ (∃) = λP. ∀q. (∀x. P x ⇒ q) ⇒ q

⊦ (∀p. P p) ⇔ ∀p_1 p_2. P (Data.Pair., p_1 p_2)

⊦ Data.Option.join Data.Option.NONE = Data.Option.NONE ∧
  ∀x. Data.Option.join (Data.Option.SOME x) = x

⊦ ∀x y. Set.in x (Set.insert y Set.∅) ⇔ x = y

⊦ ∀x y. Data.Option.SOME x = Data.Option.SOME y ⇔ x = y

⊦ ∀A B. ¬(A ⇒ B) ⇔ A ∧ ¬B

⊦ ∀m n. Number.Natural.suc m = Number.Natural.suc n ⇔ m = n

⊦ ∀m n.
    Number.Natural.< (Number.Natural.suc m) (Number.Natural.suc n) ⇔
    Number.Natural.< m n

⊦ ∀n m.
    Number.Natural.≤ (Number.Natural.suc n) (Number.Natural.suc m) ⇔
    Number.Natural.≤ n m

⊦ ∀m.
    Number.Natural.- Number.Numeral.zero m = Number.Numeral.zero ∧
    Number.Natural.- m Number.Numeral.zero = m

⊦ ∀f g x. Function.∘ f g x = f (g x)

⊦ ∀f. Function.∘ Function.id f = f ∧ Function.∘ f Function.id = f

⊦ ∀f x y. Function.Combinator.c f x y = f y x

⊦ ∀f g. f = g ⇔ ∀x. f x = g x

⊦ ∀f v. (∀x. x = v ⇒ f x) ⇔ f v

⊦ ∀P a. (∃x. x = a ∧ P x) ⇔ P a

⊦ ∀f x y. Data.Pair.uncurry f (Data.Pair., x y) = f x y

⊦ (∨) = λt1 t2. ∀t. (t1 ⇒ t) ⇒ (t2 ⇒ t) ⇒ t

⊦ ∀t1 t2. (t1 ⇔ t2) ⇔ (t1 ⇒ t2) ∧ (t2 ⇒ t1)

⊦ ∀t1 t2. (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2)

⊦ (p ⇔ ¬q) ⇔ (p ∨ q) ∧ (¬q ∨ ¬p)

⊦ Function.Combinator.s f (Data.Pair.uncurry g) =
  Data.Pair.uncurry
    (Function.Combinator.s
       (Function.∘ Function.Combinator.s
          (Function.∘ (Function.∘ f) Data.Pair.,)) g)

⊦ ¬(¬A ∨ B) ⇒ F ⇔ A ⇒ ¬B ⇒ F

⊦ ∀x r. Set.in x (Relation.domain r) ⇔ ∃y. Set.in (Data.Pair., x y) r

⊦ ∀y r. Set.in y (Relation.range r) ⇔ ∃x. Set.in (Data.Pair., x y) r

⊦ ∀P Q. (∀x. P ∨ Q x) ⇔ P ∨ ∀x. Q x

⊦ ∀Q P. (∀x. P x ∨ Q) ⇔ (∀x. P x) ∨ Q

⊦ ∀P Q. (∃x. P ∧ Q x) ⇔ P ∧ ∃x. Q x

⊦ ∀P Q. P ∧ (∀x. Q x) ⇔ ∀x. P ∧ Q x

⊦ ∀P Q. P ∨ (∃x. Q x) ⇔ ∃x. P ∨ Q x

⊦ ∀P Q. (∀x. P x ⇒ Q) ⇔ (∃x. P x) ⇒ Q

⊦ ∀P Q. (∀x. P x) ∧ Q ⇔ ∀x. P x ∧ Q

⊦ ∀s t. Set.⊂ s t ⇔ Set.⊆ s t ∧ ¬(s = t)

⊦ ¬(A ∨ B) ⇒ F ⇔ (A ⇒ F) ⇒ ¬B ⇒ F

⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∧ z ⇒ y ∧ w

⊦ (x ⇒ y) ∧ (z ⇒ w) ⇒ x ∨ z ⇒ y ∨ w

⊦ ∀t1 t2 t3. t1 ⇒ t2 ⇒ t3 ⇔ t1 ∧ t2 ⇒ t3

⊦ ∀A B C. A ∨ B ∨ C ⇔ (A ∨ B) ∨ C

⊦ ∀m n p.
    Number.Natural.+ m (Number.Natural.+ n p) =
    Number.Natural.+ (Number.Natural.+ m n) p

⊦ ∀m n p. Number.Natural.+ m p = Number.Natural.+ n p ⇔ m = n

⊦ ∀m n p.
    Number.Natural.≤ (Number.Natural.+ m n) (Number.Natural.+ m p) ⇔
    Number.Natural.≤ n p

⊦ ∀m n p.
    Number.Natural.≤ m n ∧ Number.Natural.≤ n p ⇒ Number.Natural.≤ m p

⊦ ∀s t. s = t ⇔ ∀x. Set.in x s ⇔ Set.in x t

⊦ ∀s t. Set.⊆ s t ⇔ ∀x. Set.in x s ⇒ Set.in x t

⊦ ∀P. (∀x. ∃y. P x y) ⇔ ∃f. ∀x. P x (f x)

⊦ ∀f v. Set.in v (Set.specification f) ⇔ ∃x. Data.Pair., v T = f x

⊦ (∀x. P x ⇒ Q x) ⇒ (∃x. P x) ⇒ ∃x. Q x

⊦ ∀t1 t2. (if T then t1 else t2) = t1 ∧ (if F then t1 else t2) = t2

⊦ ∀m n.
    Number.Natural.+ m n = Number.Numeral.zero ⇔
    m = Number.Numeral.zero ∧ n = Number.Numeral.zero

⊦ Data.List.length Data.List.[] = Number.Numeral.zero ∧
  ∀h t.
    Data.List.length (Data.List.:: h t) =
    Number.Natural.suc (Data.List.length t)

⊦ ∀P.
    P Number.Numeral.zero ∧ (∀n. P n ⇒ P (Number.Natural.suc n)) ⇒ ∀n. P n

⊦ (∀t. ¬¬t ⇔ t) ∧ (¬T ⇔ F) ∧ (¬F ⇔ T)

⊦ ∀m n.
    ¬(m = n) ⇔
    Number.Natural.≤ (Number.Natural.suc m) n ∨
    Number.Natural.≤ (Number.Natural.suc n) m

⊦ ∀x y s. Set.in x (Set.insert y s) ⇔ x = y ∨ Set.in x s

⊦ ∀P Q R. P ⇒ Q ∧ R ⇔ (P ⇒ Q) ∧ (P ⇒ R)

⊦ ∀A B C. A ∨ B ∧ C ⇔ (A ∨ B) ∧ (A ∨ C)

⊦ ∀P Q R. P ∨ Q ⇒ R ⇔ (P ⇒ R) ∧ (Q ⇒ R)

⊦ ∀A B C. B ∧ C ∨ A ⇔ (B ∨ A) ∧ (C ∨ A)

⊦ ∀s t x. Set.in x (Set.∪ s t) ⇔ Set.in x s ∨ Set.in x t

⊦ ∀r s s'.
    Relation.linearOrder r s ∧ Set.⊆ s' s ⇒
    Relation.linearOrder (Relation.restrict r s') s'