signature llistTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val LAPPEND : thm
    val LCONS : thm
    val LDEST : thm
    val LDROP : thm
    val LFILTER : thm
    val LFINITE : thm
    val LFLATTEN : thm
    val LHD : thm
    val LLENGTH : thm
    val LL_ALL : thm
    val LMAP : thm
    val LNIL : thm
    val LNTH : thm
    val LTAKE : thm
    val LTL : thm
    val firstPelemAt : thm
    val fromList : thm
    val lbuild_rep : thm
    val lbuildn_rep : thm
    val lcons_rep : thm
    val ldest_rep : thm
    val llist_TY_DEF : thm
    val llist_absrep : thm
    val lnil_rep : thm
    val lrep_ok : thm
    val lrep_take : thm
    val never : thm
    val toList : thm
  
  (*  Theorems  *)
    val LAPPEND_ASSOC : thm
    val LAPPEND_NIL_2ND : thm
    val LCONS_11 : thm
    val LCONS_NOT_NIL : thm
    val LDROP1_THM : thm
    val LDROP_THM : thm
    val LFILTER_APPEND : thm
    val LFILTER_NIL : thm
    val LFILTER_THM : thm
    val LFINITE_APPEND : thm
    val LFINITE_DROP : thm
    val LFINITE_HAS_LENGTH : thm
    val LFINITE_INDUCTION : thm
    val LFINITE_MAP : thm
    val LFINITE_STRONG_INDUCTION : thm
    val LFINITE_TAKE : thm
    val LFINITE_THM : thm
    val LFINITE_fromList : thm
    val LFINITE_toList : thm
    val LFLATTEN_APPEND : thm
    val LFLATTEN_EQ_NIL : thm
    val LFLATTEN_SINGLETON : thm
    val LFLATTEN_THM : thm
    val LHDTL_CONS_THM : thm
    val LHDTL_EQ_SOME : thm
    val LHD_EQ_NONE : thm
    val LHD_THM : thm
    val LLENGTH_APPEND : thm
    val LLENGTH_MAP : thm
    val LLENGTH_THM : thm
    val LLENGTH_fromList : thm
    val LLIST_BISIMULATION : thm
    val LL_ALL_THM : thm
    val LMAP_APPEND : thm
    val LMAP_MAP : thm
    val LNTH_THM : thm
    val LTAKE_CONS_EQ_NONE : thm
    val LTAKE_CONS_EQ_SOME : thm
    val LTAKE_DROP : thm
    val LTAKE_EQ : thm
    val LTAKE_EQ_NONE : thm
    val LTAKE_EQ_SOME_CONS : thm
    val LTAKE_NIL_EQ_NONE : thm
    val LTAKE_NIL_EQ_SOME : thm
    val LTAKE_THM : thm
    val LTAKE_fromList : thm
    val LTL_EQ_NONE : thm
    val LTL_THM : thm
    val NOT_LFINITE_APPEND : thm
    val NOT_LFINITE_DROP : thm
    val NOT_LFINITE_NO_LENGTH : thm
    val NOT_LFINITE_TAKE : thm
    val firstPelemAt_CONS : thm
    val firstPelemAt_SUC : thm
    val from_toList : thm
    val llist_Axiom : thm
    val llist_CASES : thm
    val never_THM : thm
    val toList_THM : thm
    val to_fromList : thm
  
  val llist_grammars : type_grammar.grammar * term_grammar.grammar
  
  val llist_rwts : simpLib.ssdata
(*
   [list] Parent theory of "llist"
   
   [LAPPEND]  Definition
      
      |- (∀x. LAPPEND LNIL x = x) ∧
         ∀h t x. LAPPEND (LCONS h t) x = LCONS h (LAPPEND t x)
   
   [LCONS]  Definition
      
      |- ∀h t. LCONS h t = llist_abs (lcons_rep h (llist_rep t))
   
   [LDEST]  Definition
      
      |- ∀ll.
           LDEST ll =
           case ldest_rep (llist_rep ll) of
              NONE -> NONE
           || SOME p -> SOME (FST p,llist_abs (SND p))
   
   [LDROP]  Definition
      
      |- (∀ll. LDROP 0 ll = SOME ll) ∧
         ∀n ll. LDROP (SUC n) ll = OPTION_JOIN (OPTION_MAP (LDROP n) (LTL ll))
   
   [LFILTER]  Definition
      
      |- ∀P ll.
           LFILTER P ll =
           (if never P ll then
              LNIL
            else
              (if P (THE (LHD ll)) then
                 LCONS (THE (LHD ll)) (LFILTER P (THE (LTL ll)))
               else
                 LFILTER P (THE (LTL ll))))
   
   [LFINITE]  Definition
      
      |- ∀ll. LFINITE ll = ∃n. LTAKE n ll = NONE
   
   [LFLATTEN]  Definition
      
      |- ∀ll.
           LFLATTEN ll =
           (if LL_ALL ($= LNIL) ll then
              LNIL
            else
              (if THE (LHD ll) = LNIL then
                 LFLATTEN (THE (LTL ll))
               else
                 LCONS (THE (LHD (THE (LHD ll))))
                   (LFLATTEN (LCONS (THE (LTL (THE (LHD ll)))) (THE (LTL ll))))))
   
   [LHD]  Definition
      
      |- ∀ll. LHD ll = OPTION_MAP FST (ldest_rep (llist_rep ll))
   
   [LLENGTH]  Definition
      
      |- ∀ll.
           LLENGTH ll =
           (if LFINITE ll then
              SOME
                ((εn.
                    (LTAKE n ll = NONE) ∧
                    ∀m. m < n ⇒ ∃ll'. LTAKE m ll = SOME ll') -
                 1)
            else
              NONE)
   
   [LL_ALL]  Definition
      
      |- ∀P ll. LL_ALL P ll = never ($~ o P) ll
   
   [LMAP]  Definition
      
      |- (∀f. LMAP f LNIL = LNIL) ∧
         ∀f h t. LMAP f (LCONS h t) = LCONS (f h) (LMAP f t)
   
   [LNIL]  Definition
      
      |- LNIL = llist_abs lnil_rep
   
   [LNTH]  Definition
      
      |- (∀ll. LNTH 0 ll = LHD ll) ∧
         ∀n ll. LNTH (SUC n) ll = OPTION_JOIN (OPTION_MAP (LNTH n) (LTL ll))
   
   [LTAKE]  Definition
      
      |- (∀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]  Definition
      
      |- ∀ll. LTL ll = OPTION_MAP (llist_abs o SND) (ldest_rep (llist_rep ll))
   
   [firstPelemAt]  Definition
      
      |- ∀P n ll.
           firstPelemAt P n ll =
           case F P (LNTH n ll) ∧
           ∀m. m < n ⇒ (OPTION_MAP P (LNTH m ll) = SOME F)
   
   [fromList]  Definition
      
      |- (fromList [] = LNIL) ∧
         ∀h t. fromList (h::t) = LCONS h (fromList t)
   
   [lbuild_rep]  Definition
      
      |- ∀f x.
           lbuild_rep f x =
           (\pfx.
              case NONE
                (\(pfx',nthseed).
                   (if pfx' = pfx then OPTION_MAP SND (f nthseed) else NONE))
                (lbuildn_rep f x (LENGTH pfx)))
   
   [lbuildn_rep]  Definition
      
      |- (∀f x. lbuildn_rep f x 0 = SOME ([],x)) ∧
         ∀f x n.
           lbuildn_rep f x (SUC n) =
           case NONE
             (\(pfx,x'). case NONE (\(x'',last). SOME (pfx ++ [last],x'')) (f x'))
             (lbuildn_rep f x n)
   
   [lcons_rep]  Definition
      
      |- ∀h t.
           lcons_rep h t =
           (\l. (if l = [] then SOME h else (if HD l = h then t (TL l) else NONE)))
   
   [ldest_rep]  Definition
      
      |- ∀f.
           ldest_rep f =
           case f [] of NONE -> NONE || SOME x -> SOME (x,(\l. f (x::l)))
   
   [llist_TY_DEF]  Definition
      
      |- ∃rep. TYPE_DEFINITION lrep_ok rep
   
   [llist_absrep]  Definition
      
      |- (∀a. llist_abs (llist_rep a) = a) ∧
         ∀r. lrep_ok r = (llist_rep (llist_abs r) = r)
   
   [lnil_rep]  Definition
      
      |- lnil_rep = (\l. NONE)
   
   [lrep_ok]  Definition
      
      |- ∀f.
           lrep_ok f =
           ∀l x. (f l = SOME x) ⇒ ∃n. lrep_take f n = SOME l
   
   [lrep_take]  Definition
      
      |- (∀f. lrep_take f 0 = SOME []) ∧
         ∀f n.
           lrep_take f (SUC n) =
           case lrep_take f n of
              NONE -> NONE
           || SOME pfx -> case f pfx of NONE -> NONE || SOME a -> SOME (pfx ++ [a])
   
   [never]  Definition
      
      |- ∀P ll. never P ll = ∀n. ¬firstPelemAt P n ll
   
   [toList]  Definition
      
      |- ∀ll.
           toList ll = (if LFINITE ll then LTAKE (THE (LLENGTH ll)) ll else NONE)
   
   [LAPPEND_ASSOC]  Theorem
      
      |- ∀ll1 ll2 ll3.
           LAPPEND (LAPPEND ll1 ll2) ll3 = LAPPEND ll1 (LAPPEND ll2 ll3)
   
   [LAPPEND_NIL_2ND]  Theorem
      
      |- ∀ll. LAPPEND ll LNIL = ll
   
   [LCONS_11]  Theorem
      
      |- ∀h1 t1 h2 t2. (LCONS h1 t1 = LCONS h2 t2) = (h1 = h2) ∧ (t1 = t2)
   
   [LCONS_NOT_NIL]  Theorem
      
      |- ∀h t. ¬(LCONS h t = LNIL) ∧ ¬(LNIL = LCONS h t)
   
   [LDROP1_THM]  Theorem
      
      |- LDROP 1 = LTL
   
   [LDROP_THM]  Theorem
      
      |- (∀ll. LDROP 0 ll = SOME ll) ∧
         (∀n. LDROP (SUC n) LNIL = NONE) ∧
         ∀n h t. LDROP (SUC n) (LCONS h t) = LDROP n t
   
   [LFILTER_APPEND]  Theorem
      
      |- ∀P ll1 ll2.
           LFINITE ll1 ⇒
           (LFILTER P (LAPPEND ll1 ll2) = LAPPEND (LFILTER P ll1) (LFILTER P ll2))
   
   [LFILTER_NIL]  Theorem
      
      |- ∀P ll. LL_ALL ($~ o P) ll ⇒ (LFILTER P ll = LNIL)
   
   [LFILTER_THM]  Theorem
      
      |- (∀P. LFILTER P LNIL = LNIL) ∧
         ∀P h t.
           LFILTER P (LCONS h t) =
           (if P h then LCONS h (LFILTER P t) else LFILTER P t)
   
   [LFINITE_APPEND]  Theorem
      
      |- ∀ll1 ll2. LFINITE (LAPPEND ll1 ll2) = LFINITE ll1 ∧ LFINITE ll2
   
   [LFINITE_DROP]  Theorem
      
      |- ∀n ll.
           LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒
           ∃y. LDROP n ll = SOME y
   
   [LFINITE_HAS_LENGTH]  Theorem
      
      |- ∀ll. LFINITE ll ⇒ ∃n. LLENGTH ll = SOME n
   
   [LFINITE_INDUCTION]  Theorem
      
      |- ∀P.
           P LNIL ∧ (∀t. P t ⇒ ∀h. P (LCONS h t)) ⇒
           ∀ll. LFINITE ll ⇒ P ll
   
   [LFINITE_MAP]  Theorem
      
      |- ∀f ll. LFINITE (LMAP f ll) = LFINITE ll
   
   [LFINITE_STRONG_INDUCTION]  Theorem
      
      |- P LNIL ∧
         (∀t. LFINITE t ∧ P t ⇒ ∀h. P (LCONS h t)) ⇒
         ∀ll. LFINITE ll ⇒ P ll
   
   [LFINITE_TAKE]  Theorem
      
      |- ∀n ll.
           LFINITE ll ∧ n ≤ THE (LLENGTH ll) ⇒
           ∃y. LTAKE n ll = SOME y
   
   [LFINITE_THM]  Theorem
      
      |- (LFINITE LNIL = T) ∧ ∀h t. LFINITE (LCONS h t) = LFINITE t
   
   [LFINITE_fromList]  Theorem
      
      |- ∀l. LFINITE (fromList l)
   
   [LFINITE_toList]  Theorem
      
      |- ∀ll. LFINITE ll ⇒ ∃l. toList ll = SOME l
   
   [LFLATTEN_APPEND]  Theorem
      
      |- ∀h t. LFLATTEN (LCONS h t) = LAPPEND h (LFLATTEN t)
   
   [LFLATTEN_EQ_NIL]  Theorem
      
      |- ∀ll. (LFLATTEN ll = LNIL) = LL_ALL ($= LNIL) ll
   
   [LFLATTEN_SINGLETON]  Theorem
      
      |- ∀h. LFLATTEN (LCONS h LNIL) = h
   
   [LFLATTEN_THM]  Theorem
      
      |- (LFLATTEN LNIL = LNIL) ∧
         (∀tl. LFLATTEN (LCONS LNIL t) = LFLATTEN t) ∧
         ∀h t tl.
           LFLATTEN (LCONS (LCONS h t) tl) = LCONS h (LFLATTEN (LCONS t tl))
   
   [LHDTL_CONS_THM]  Theorem
      
      |- ∀h t. (LHD (LCONS h t) = SOME h) ∧ (LTL (LCONS h t) = SOME t)
   
   [LHDTL_EQ_SOME]  Theorem
      
      |- ∀h t ll. (ll = LCONS h t) = (LHD ll = SOME h) ∧ (LTL ll = SOME t)
   
   [LHD_EQ_NONE]  Theorem
      
      |- ∀ll. (LHD ll = NONE) = (ll = LNIL)
   
   [LHD_THM]  Theorem
      
      |- (LHD LNIL = NONE) ∧ ∀h t. LHD (LCONS h t) = SOME h
   
   [LLENGTH_APPEND]  Theorem
      
      |- ∀ll1 ll2.
           LLENGTH (LAPPEND ll1 ll2) =
           (if LFINITE ll1 ∧ LFINITE ll2 then
              SOME (THE (LLENGTH ll1) + THE (LLENGTH ll2))
            else
              NONE)
   
   [LLENGTH_MAP]  Theorem
      
      |- ∀ll f. LLENGTH (LMAP f ll) = LLENGTH ll
   
   [LLENGTH_THM]  Theorem
      
      |- (LLENGTH LNIL = SOME 0) ∧
         ∀h t. LLENGTH (LCONS h t) = OPTION_MAP SUC (LLENGTH t)
   
   [LLENGTH_fromList]  Theorem
      
      |- ∀l. LLENGTH (fromList l) = SOME (LENGTH l)
   
   [LLIST_BISIMULATION]  Theorem
      
      |- ∀ll1 ll2.
           (ll1 = ll2) =
           ∃R.
             R ll1 ll2 ∧
             ∀ll3 ll4.
               R ll3 ll4 ⇒
               (ll3 = LNIL) ∧ (ll4 = LNIL) ∨
               (LHD ll3 = LHD ll4) ∧ R (THE (LTL ll3)) (THE (LTL ll4))
   
   [LL_ALL_THM]  Theorem
      
      |- (∀P. LL_ALL P LNIL = T) ∧
         ∀P h t. LL_ALL P (LCONS h t) = P h ∧ LL_ALL P t
   
   [LMAP_APPEND]  Theorem
      
      |- ∀f ll1 ll2.
           LMAP f (LAPPEND ll1 ll2) = LAPPEND (LMAP f ll1) (LMAP f ll2)
   
   [LMAP_MAP]  Theorem
      
      |- ∀f g ll. LMAP f (LMAP g ll) = LMAP (f o g) ll
   
   [LNTH_THM]  Theorem
      
      |- (∀n. LNTH n LNIL = NONE) ∧
         (∀h t. LNTH 0 (LCONS h t) = SOME h) ∧
         ∀n h t. LNTH (SUC n) (LCONS h t) = LNTH n t
   
   [LTAKE_CONS_EQ_NONE]  Theorem
      
      |- ∀m h t.
           (LTAKE m (LCONS h t) = NONE) =
           ∃n. (m = SUC n) ∧ (LTAKE n t = NONE)
   
   [LTAKE_CONS_EQ_SOME]  Theorem
      
      |- ∀m h t l.
           (LTAKE m (LCONS h t) = SOME l) =
           (m = 0) ∧ (l = []) ∨
           ∃n l'. (m = SUC n) ∧ (LTAKE n t = SOME l') ∧ (l = h::l')
   
   [LTAKE_DROP]  Theorem
      
      |- (∀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]  Theorem
      
      |- ∀ll1 ll2. (ll1 = ll2) = ∀n. LTAKE n ll1 = LTAKE n ll2
   
   [LTAKE_EQ_NONE]  Theorem
      
      |- ∀ll n. (LTAKE n ll = NONE) ⇒ 0 < n
   
   [LTAKE_EQ_SOME_CONS]  Theorem
      
      |- ∀n l x.
           (LTAKE n l = SOME x) ⇒
           ∀h. ∃y. LTAKE n (LCONS h l) = SOME y
   
   [LTAKE_NIL_EQ_NONE]  Theorem
      
      |- ∀m. (LTAKE m LNIL = NONE) = 0 < m
   
   [LTAKE_NIL_EQ_SOME]  Theorem
      
      |- ∀l m. (LTAKE m LNIL = SOME l) = (m = 0) ∧ (l = [])
   
   [LTAKE_THM]  Theorem
      
      |- (∀l. LTAKE 0 l = SOME []) ∧
         (∀n. LTAKE (SUC n) LNIL = NONE) ∧
         ∀n h t. LTAKE (SUC n) (LCONS h t) = OPTION_MAP (CONS h) (LTAKE n t)
   
   [LTAKE_fromList]  Theorem
      
      |- ∀l. LTAKE (LENGTH l) (fromList l) = SOME l
   
   [LTL_EQ_NONE]  Theorem
      
      |- ∀ll. (LTL ll = NONE) = (ll = LNIL)
   
   [LTL_THM]  Theorem
      
      |- (LTL LNIL = NONE) ∧ ∀h t. LTL (LCONS h t) = SOME t
   
   [NOT_LFINITE_APPEND]  Theorem
      
      |- ∀ll1 ll2. ¬LFINITE ll1 ⇒ (LAPPEND ll1 ll2 = ll1)
   
   [NOT_LFINITE_DROP]  Theorem
      
      |- ∀ll. ¬LFINITE ll ⇒ ∀n. ∃y. LDROP n ll = SOME y
   
   [NOT_LFINITE_NO_LENGTH]  Theorem
      
      |- ∀ll. ¬LFINITE ll ⇒ (LLENGTH ll = NONE)
   
   [NOT_LFINITE_TAKE]  Theorem
      
      |- ∀ll. ¬LFINITE ll ⇒ ∀n. ∃y. LTAKE n ll = SOME y
   
   [firstPelemAt_CONS]  Theorem
      
      |- ∀P n h t.
           firstPelemAt P n (LCONS h t) =
           (n = 0) ∧ P h ∨
           ∃m. (n = SUC m) ∧ firstPelemAt P m t ∧ ¬P h
   
   [firstPelemAt_SUC]  Theorem
      
      |- ∀P n h t.
           firstPelemAt P (SUC n) (LCONS h t) ⇒ firstPelemAt P n t
   
   [from_toList]  Theorem
      
      |- ∀l. toList (fromList l) = SOME l
   
   [llist_Axiom]  Theorem
      
      |- ∀f.
           ∃g.
             (∀x. LHD (g x) = OPTION_MAP SND (f x)) ∧
             ∀x. LTL (g x) = OPTION_MAP (g o FST) (f x)
   
   [llist_CASES]  Theorem
      
      |- ∀l. (l = LNIL) ∨ ∃h t. l = LCONS h t
   
   [never_THM]  Theorem
      
      |- (∀P. never P LNIL = T) ∧
         ∀P h t. never P (LCONS h t) = ¬P h ∧ never P t
   
   [toList_THM]  Theorem
      
      |- (toList LNIL = SOME []) ∧
         ∀h t. toList (LCONS h t) = OPTION_MAP (CONS h) (toList t)
   
   [to_fromList]  Theorem
      
      |- ∀ll. LFINITE ll ⇒ (fromList (THE (toList ll)) = ll)
   
   
*)
end