Theory "indexedLists"

Signature

Definitions

MAPi_def

⊢ (∀f. MAPi f [] = []) ∧ ∀f h t. MAPi f (h::t) = f 0 h::MAPi (f ∘ SUC) t

MAPi_ACC_def

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

FOLDRi_def

⊢ (∀f a. FOLDRi f a [] = a) ∧
  ∀f a h t. FOLDRi f a (h::t) = f 0 h (FOLDRi (f ∘ SUC) a t)

findi_def

⊢ (∀x. findi x [] = 0) ∧
  ∀x h t. findi x (h::t) = if x = h then 0 else 1 + findi x t

delN_def

⊢ (∀i. delN i [] = []) ∧
  ∀i h t. delN i (h::t) = if i = 0 then t else h::delN (i − 1) t

LIST_RELi_def

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

Theorems

MAPi_ACC_MAPi

⊢ MAPi_ACC f n a l = REVERSE a ++ MAPi (f ∘ $+ n) l

MAPi_compute

⊢ MAPi f l = MAPi_ACC f 0 [] l

LT_SUC

⊢ n < SUC m ⇔ n = 0 ∨ ∃n0. n = SUC n0 ∧ n0 < m

MEM_MAPi

⊢ ∀x f l. MEM x (MAPi f l) ⇔ ∃n. n < LENGTH l ∧ x = f n (EL n l)

MAPi_CONG

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

⊢ l1 = l2 ⇒
  (∀x n. x = EL n l2 ⇒ n < LENGTH l2 ⇒ f1 n x = f2 n x) ⇒
  MAPi f1 l1 = MAPi f2 l2

LENGTH_MAPi

⊢ ∀f l. LENGTH (MAPi f l) = LENGTH l

MAP_MAPi

⊢ ∀f g l. MAP f (MAPi g l) = MAPi ($o f ∘ g) l

EL_MAPi

⊢ ∀f n l. n < LENGTH l ⇒ EL n (MAPi f l) = f n (EL n l)

MAPi_APPEND

⊢ ∀l1 l2 f. MAPi f (l1 ++ l2) = MAPi f l1 ++ MAPi (f ∘ $+ (LENGTH l1)) l2

MAPi_GENLIST

⊢ ∀l f. MAPi f l = GENLIST (S f (combin$C EL l)) (LENGTH l)

GENLIST_CONG

⊢ (∀m. m < n ⇒ f1 m = f2 m) ⇒ GENLIST f1 n = GENLIST f2 n

FOLDR_MAPi

⊢ ∀f g a l. FOLDR f a (MAPi g l) = FOLDRi ($o f ∘ g) a l

FOLDRi_APPEND

⊢ ∀f. FOLDRi f a (l1 ++ l2) = FOLDRi f (FOLDRi (f ∘ $+ (LENGTH l1)) a l2) l1

FOLDRi_CONG

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

⊢ 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

MEM_findi

⊢ MEM x l ⇒ findi x l < LENGTH l

findi_EL

⊢ ∀l n. n < LENGTH l ∧ ALL_DISTINCT l ⇒ findi (EL n l) l = n

EL_findi

⊢ ∀l x. MEM x l ⇒ EL (findi x l) l = x

delN_shortens

⊢ ∀l i. i < LENGTH l ⇒ LENGTH (delN i l) = LENGTH l − 1

EL_delN_BEFORE

⊢ ∀l i j. i < j ∧ j < LENGTH l ⇒ EL i (delN j l) = EL i l

EL_delN_AFTER

⊢ ∀l i j. j ≤ i ∧ i + 1 < LENGTH l ⇒ EL i (delN j l) = EL (i + 1) l

fupdLast_ind

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

fupdLast_def

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

⊢ (fupdLast f x = [] ⇔ x = []) ∧ ([] = fupdLast f x ⇔ x = [])

fupdLast_FRONT_LAST

⊢ fupdLast f l = if l = [] then [] else FRONT l ++ [f (LAST l)]

LIST_RELi_rules

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

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

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

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

⊢ ∀l1 l2. LIST_RELi R l1 l2 ⇒ LENGTH l1 = LENGTH l2

LIST_RELi_EL_EQN

⊢ LIST_RELi R l1 l2 ⇔
  LENGTH l1 = LENGTH l2 ∧ ∀i. i < LENGTH l1 ⇒ R i (EL i l1) (EL i l2)

LIST_RELi_thm

⊢ (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')

LIST_RELi_APPEND_I

⊢ LIST_RELi R l1 l2 ∧ LIST_RELi (R ∘ $+ (LENGTH l1)) m1 m2 ⇒
  LIST_RELi R (l1 ++ m1) (l2 ++ m2)

MAP2i_ind

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

MAP2i_def

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

⊢ MAP2i f l1 [] = []

LENGTH_MAP2i

⊢ ∀f l1 l2. LENGTH (MAP2i f l1 l2) = MIN (LENGTH l1) (LENGTH l2)

EL_MAP2i

⊢ ∀f l1 l2 n.
      n < LENGTH l1 ∧ n < LENGTH l2 ⇒
      EL n (MAP2i f l1 l2) = f n (EL n l1) (EL n l2)

MAP2ia_ind

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

MAP2ia_def

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

⊢ indexedLists$MAP2ia f i l1 [] = []

MAP2i_compute

⊢ MAP2i f l1 l2 = indexedLists$MAP2ia f 0 l1 l2