Structure indexedListsTheory

signature indexedListsTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val FOLDRi_def : thm
    val LIST_RELi_def : thm
    val MAPi_ACC_def : thm
    val MAPi_def : thm
    val delN_def : thm
    val findi_def : thm
  
  (*  Theorems  *)
    val EL_MAP2i : thm
    val EL_MAPi : thm
    val EL_delN_AFTER : thm
    val EL_delN_BEFORE : thm
    val EL_findi : thm
    val FOLDR_MAPi : thm
    val FOLDRi_APPEND : thm
    val FOLDRi_CONG : thm
    val FOLDRi_CONG' : thm
    val LENGTH_MAP2i : thm
    val LENGTH_MAPi : thm
    val LIST_RELi_APPEND_I : thm
    val LIST_RELi_EL_EQN : thm
    val LIST_RELi_LENGTH : thm
    val LIST_RELi_cases : thm
    val LIST_RELi_ind : thm
    val LIST_RELi_rules : thm
    val LIST_RELi_strongind : thm
    val LIST_RELi_thm : thm
    val MAP2i_NIL2 : thm
    val MAP2i_compute : thm
    val MAP2i_def : thm
    val MAP2i_ind : thm
    val MAP2ia_NIL2 : thm
    val MAP2ia_def : thm
    val MAP2ia_ind : thm
    val MAP_MAPi : thm
    val MAPi_ACC_MAPi : thm
    val MAPi_APPEND : thm
    val MAPi_CONG : thm
    val MAPi_CONG' : thm
    val MAPi_GENLIST : thm
    val MAPi_compute : thm
    val MEM_MAPi : thm
    val MEM_findi : thm
    val delN_shortens : thm
    val findi_EL : thm
    val fupdLast_EQ_NIL : thm
    val fupdLast_FRONT_LAST : thm
    val fupdLast_def : thm
    val fupdLast_ind : thm
  
  val indexedLists_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [rich_list] Parent theory of "indexedLists"
   
   [FOLDRi_def]  Definition
      
      ⊢ (∀f a. FOLDRi f a [] = a) ∧
        ∀f a h t. FOLDRi f a (h::t) = f 0 h (FOLDRi (f ∘ SUC) a t)
   
   [LIST_RELi_def]  Definition
      
      ⊢ LIST_RELi =
        (λR a0 a1.
             ∀LIST_RELi'.
               (∀a0 a1.
                  a0 = [] ∧ a1 = [] ∨
                  (∃h1 h2 l1 l2.
                     a0 = l1 ⧺ [h1] ∧ a1 = l2 ⧺ [h2] ∧
                     R (LENGTH l1) h1 h2 ∧ LIST_RELi' l1 l2) ⇒
                  LIST_RELi' a0 a1) ⇒
               LIST_RELi' a0 a1)
   
   [MAPi_ACC_def]  Definition
      
      ⊢ (∀f i a. MAPi_ACC f i a [] = REVERSE a) ∧
        ∀f i a h t. MAPi_ACC f i a (h::t) = MAPi_ACC f (i + 1) (f i h::a) t
   
   [MAPi_def]  Definition
      
      ⊢ (∀f. MAPi f [] = []) ∧
        ∀f h t. MAPi f (h::t) = f 0 h::MAPi (f ∘ SUC) t
   
   [delN_def]  Definition
      
      ⊢ (∀i. delN i [] = []) ∧
        ∀i h t. delN i (h::t) = if i = 0 then t else h::delN (i − 1) t
   
   [findi_def]  Definition
      
      ⊢ (∀x. findi x [] = 0) ∧
        ∀x h t. findi x (h::t) = if x = h then 0 else 1 + findi x t
   
   [EL_MAP2i]  Theorem
      
      ⊢ ∀f l1 l2 n.
          n < LENGTH l1 ∧ n < LENGTH l2 ⇒
          EL n (MAP2i f l1 l2) = f n (EL n l1) (EL n l2)
   
   [EL_MAPi]  Theorem
      
      ⊢ ∀f n l. n < LENGTH l ⇒ EL n (MAPi f l) = f n (EL n l)
   
   [EL_delN_AFTER]  Theorem
      
      ⊢ ∀l i j. j ≤ i ∧ i + 1 < LENGTH l ⇒ EL i (delN j l) = EL (i + 1) l
   
   [EL_delN_BEFORE]  Theorem
      
      ⊢ ∀l i j. i < j ∧ j < LENGTH l ⇒ EL i (delN j l) = EL i l
   
   [EL_findi]  Theorem
      
      ⊢ ∀l x. MEM x l ⇒ EL (findi x l) l = x
   
   [FOLDR_MAPi]  Theorem
      
      ⊢ ∀f g a l. FOLDR f a (MAPi g l) = FOLDRi ($o f ∘ g) a l
   
   [FOLDRi_APPEND]  Theorem
      
      ⊢ ∀f. FOLDRi f a (l1 ⧺ l2) =
            FOLDRi f (FOLDRi (f ∘ $+ (LENGTH l1)) a l2) l1
   
   [FOLDRi_CONG]  Theorem
      
      ⊢ l1 = l2 ⇒
        (∀n e a. n < LENGTH l2 ⇒ MEM e l2 ⇒ f1 n e a = f2 n e a) ⇒
        a1 = a2 ⇒
        FOLDRi f1 a1 l1 = FOLDRi f2 a2 l2
   
   [FOLDRi_CONG']  Theorem
      
      ⊢ l1 = l2 ∧
        (∀n a. n < LENGTH l2 ⇒ f1 n (EL n l2) a = f2 n (EL n l2) a) ∧
        a1 = a2 ⇒
        FOLDRi f1 a1 l1 = FOLDRi f2 a2 l2
   
   [LENGTH_MAP2i]  Theorem
      
      ⊢ ∀f l1 l2. LENGTH (MAP2i f l1 l2) = MIN (LENGTH l1) (LENGTH l2)
   
   [LENGTH_MAPi]  Theorem
      
      ⊢ ∀f l. LENGTH (MAPi f l) = LENGTH l
   
   [LIST_RELi_APPEND_I]  Theorem
      
      ⊢ LIST_RELi R l1 l2 ∧ LIST_RELi (R ∘ $+ (LENGTH l1)) m1 m2 ⇒
        LIST_RELi R (l1 ⧺ m1) (l2 ⧺ m2)
   
   [LIST_RELi_EL_EQN]  Theorem
      
      ⊢ LIST_RELi R l1 l2 ⇔
        LENGTH l1 = LENGTH l2 ∧ ∀i. i < LENGTH l1 ⇒ R i (EL i l1) (EL i l2)
   
   [LIST_RELi_LENGTH]  Theorem
      
      ⊢ ∀l1 l2. LIST_RELi R l1 l2 ⇒ LENGTH l1 = LENGTH l2
   
   [LIST_RELi_cases]  Theorem
      
      ⊢ ∀R a0 a1.
          LIST_RELi R a0 a1 ⇔
          a0 = [] ∧ a1 = [] ∨
          ∃h1 h2 l1 l2.
            a0 = l1 ⧺ [h1] ∧ a1 = l2 ⧺ [h2] ∧ R (LENGTH l1) h1 h2 ∧
            LIST_RELi R l1 l2
   
   [LIST_RELi_ind]  Theorem
      
      ⊢ ∀R LIST_RELi'.
          LIST_RELi' [] [] ∧
          (∀h1 h2 l1 l2.
             R (LENGTH l1) h1 h2 ∧ LIST_RELi' l1 l2 ⇒
             LIST_RELi' (l1 ⧺ [h1]) (l2 ⧺ [h2])) ⇒
          ∀a0 a1. LIST_RELi R a0 a1 ⇒ LIST_RELi' a0 a1
   
   [LIST_RELi_rules]  Theorem
      
      ⊢ ∀R. LIST_RELi R [] [] ∧
            ∀h1 h2 l1 l2.
              R (LENGTH l1) h1 h2 ∧ LIST_RELi R l1 l2 ⇒
              LIST_RELi R (l1 ⧺ [h1]) (l2 ⧺ [h2])
   
   [LIST_RELi_strongind]  Theorem
      
      ⊢ ∀R LIST_RELi'.
          LIST_RELi' [] [] ∧
          (∀h1 h2 l1 l2.
             R (LENGTH l1) h1 h2 ∧ LIST_RELi R l1 l2 ∧ LIST_RELi' l1 l2 ⇒
             LIST_RELi' (l1 ⧺ [h1]) (l2 ⧺ [h2])) ⇒
          ∀a0 a1. LIST_RELi R a0 a1 ⇒ LIST_RELi' a0 a1
   
   [LIST_RELi_thm]  Theorem
      
      ⊢ (LIST_RELi R [] x ⇔ x = []) ∧
        (LIST_RELi R (h::t) l ⇔
         ∃h' t'. l = h'::t' ∧ R 0 h h' ∧ LIST_RELi (R ∘ SUC) t t')
   
   [MAP2i_NIL2]  Theorem
      
      ⊢ MAP2i f l1 [] = []
   
   [MAP2i_compute]  Theorem
      
      ⊢ MAP2i f l1 l2 = indexedLists$MAP2ia f 0 l1 l2
   
   [MAP2i_def]  Theorem
      
      ⊢ (∀v0 f. MAP2i f [] v0 = []) ∧
        (∀v6 v5 f. MAP2i f (v5::v6) [] = []) ∧
        ∀t2 t1 h2 h1 f.
          MAP2i f (h1::t1) (h2::t2) = f 0 h1 h2::MAP2i (f ∘ SUC) t1 t2
   
   [MAP2i_ind]  Theorem
      
      ⊢ ∀P. (∀f v0. P f [] v0) ∧ (∀f v5 v6. P f (v5::v6) []) ∧
            (∀f h1 t1 h2 t2. P (f ∘ SUC) t1 t2 ⇒ P f (h1::t1) (h2::t2)) ⇒
            ∀v v1 v2. P v v1 v2
   
   [MAP2ia_NIL2]  Theorem
      
      ⊢ indexedLists$MAP2ia f i l1 [] = []
   
   [MAP2ia_def]  Theorem
      
      ⊢ (∀v0 i f. indexedLists$MAP2ia f i [] v0 = []) ∧
        (∀v8 v7 i f. indexedLists$MAP2ia f i (v7::v8) [] = []) ∧
        ∀t2 t1 i h2 h1 f.
          indexedLists$MAP2ia f i (h1::t1) (h2::t2) =
          f i h1 h2::indexedLists$MAP2ia f (i + 1) t1 t2
   
   [MAP2ia_ind]  Theorem
      
      ⊢ ∀P. (∀f i v0. P f i [] v0) ∧ (∀f i v7 v8. P f i (v7::v8) []) ∧
            (∀f i h1 t1 h2 t2. P f (i + 1) t1 t2 ⇒ P f i (h1::t1) (h2::t2)) ⇒
            ∀v v1 v2 v3. P v v1 v2 v3
   
   [MAP_MAPi]  Theorem
      
      ⊢ ∀f g l. MAP f (MAPi g l) = MAPi ($o f ∘ g) l
   
   [MAPi_ACC_MAPi]  Theorem
      
      ⊢ MAPi_ACC f n a l = REVERSE a ⧺ MAPi (f ∘ $+ n) l
   
   [MAPi_APPEND]  Theorem
      
      ⊢ ∀l1 l2 f.
          MAPi f (l1 ⧺ l2) = MAPi f l1 ⧺ MAPi (f ∘ $+ (LENGTH l1)) l2
   
   [MAPi_CONG]  Theorem
      
      ⊢ ∀l1 l2 f1 f2.
          l1 = l2 ∧ (∀x n. MEM x l2 ⇒ f1 n x = f2 n x) ⇒
          MAPi f1 l1 = MAPi f2 l2
   
   [MAPi_CONG']  Theorem
      
      ⊢ l1 = l2 ⇒
        (∀x n. x = EL n l2 ⇒ n < LENGTH l2 ⇒ f1 n x = f2 n x) ⇒
        MAPi f1 l1 = MAPi f2 l2
   
   [MAPi_GENLIST]  Theorem
      
      ⊢ ∀l f. MAPi f l = GENLIST (S f (flip EL l)) (LENGTH l)
   
   [MAPi_compute]  Theorem
      
      ⊢ MAPi f l = MAPi_ACC f 0 [] l
   
   [MEM_MAPi]  Theorem
      
      ⊢ ∀x f l. MEM x (MAPi f l) ⇔ ∃n. n < LENGTH l ∧ x = f n (EL n l)
   
   [MEM_findi]  Theorem
      
      ⊢ MEM x l ⇒ findi x l < LENGTH l
   
   [delN_shortens]  Theorem
      
      ⊢ ∀l i. i < LENGTH l ⇒ LENGTH (delN i l) = LENGTH l − 1
   
   [findi_EL]  Theorem
      
      ⊢ ∀l n. n < LENGTH l ∧ ALL_DISTINCT l ⇒ findi (EL n l) l = n
   
   [fupdLast_EQ_NIL]  Theorem
      
      ⊢ (fupdLast f x = [] ⇔ x = []) ∧ ([] = fupdLast f x ⇔ x = [])
   
   [fupdLast_FRONT_LAST]  Theorem
      
      ⊢ fupdLast f l = if l = [] then [] else FRONT l ⧺ [f (LAST l)]
   
   [fupdLast_def]  Theorem
      
      ⊢ (∀f. fupdLast f [] = []) ∧ (∀h f. fupdLast f [h] = [f h]) ∧
        ∀v5 v4 h f. fupdLast f (h::v4::v5) = h::fupdLast f (v4::v5)
   
   [fupdLast_ind]  Theorem
      
      ⊢ ∀P. (∀f. P f []) ∧ (∀f h. P f [h]) ∧
            (∀f h v4 v5. P f (v4::v5) ⇒ P f (h::v4::v5)) ⇒
            ∀v v1. P v v1
   
   
*)
end

HOL 4, Kananaskis-14