Theory: listRange

Theorems

EL_listRangeLHI

⊢ lo + i < hi ⇒ [lo ..< hi]❲i❳ = lo + i

LENGTH_listRangeLHI

⊢ LENGTH [lo ..< hi] = hi − lo

MEM_listRangeINC

⊢ MEM x [m .. n] ⇔ m ≤ x ∧ x ≤ n

MEM_listRangeLHI

⊢ MEM x [m ..< n] ⇔ m ≤ x ∧ x < n

every_range_cons

⊢ ∀f a b.
    a ≤ b ⇒ ((∀j. a ≤ j ∧ j ≤ b ⇒ f j) ⇔ f a ∧ ∀j. a + 1 ≤ j ∧ j ≤ b ⇒ f j)

every_range_less_ends

⊢ ∀f a b.
    a ≤ b ⇒
    ((∀j. a ≤ j ∧ j ≤ b ⇒ f j) ⇔ f a ∧ f b ∧ ∀j. a < j ∧ j < b ⇒ f j)

every_range_sing

⊢ ∀a j. a ≤ j ∧ j ≤ a ⇔ j = a

every_range_span_max

⊢ ∀f a b.
    a < b ∧ f a ∧ ¬f b ⇒
    ∃m. a ≤ m ∧ m < b ∧ (∀j. a ≤ j ∧ j ≤ m ⇒ f j) ∧ ¬f (SUC m)

every_range_span_min

⊢ ∀f a b.
    a < b ∧ ¬f a ∧ f b ⇒
    ∃m. a < m ∧ m ≤ b ∧ (∀j. m ≤ j ∧ j ≤ b ⇒ f j) ∧ ¬f (PRE m)

every_range_split_head

⊢ ∀f a b.
    a ≤ b ⇒
    ((∀j. PRE a ≤ j ∧ j ≤ b ⇒ f j) ⇔ f (PRE a) ∧ ∀j. a ≤ j ∧ j ≤ b ⇒ f j)

every_range_split_last

⊢ ∀f a b.
    a ≤ b ⇒
    ((∀j. a ≤ j ∧ j ≤ SUC b ⇒ f j) ⇔ f (SUC b) ∧ ∀j. a ≤ j ∧ j ≤ b ⇒ f j)

exists_range_cons

⊢ ∀f a b.
    a ≤ b ⇒ ((∃j. a ≤ j ∧ j ≤ b ∧ f j) ⇔ f a ∨ ∃j. a + 1 ≤ j ∧ j ≤ b ∧ f j)

exists_range_sing

⊢ ∀a. ∃j. a ≤ j ∧ j ≤ a ⇔ j = a

isPREFIX_listRangeINC

⊢ ∀m n m' n'. m = m' ∧ n ≤ n' ⇒ [m .. n] ≼ [m' .. n']

isPREFIX_listRangeINC_EQ

⊢ ∀m n m' n'. m ≤ n ∧ m' ≤ n' ⇒ ([m .. n] ≼ [m' .. n'] ⇔ m = m' ∧ n ≤ n')

isPREFIX_listRangeLHI

⊢ ∀m n m' n'. m = m' ∧ n ≤ n' ⇒ [m ..< n] ≼ [m' ..< n']

isPREFIX_listRangeLHI_EQ

⊢ ∀m n m' n'. m < n ∧ m' < n' ⇒ ([m ..< n] ≼ [m' ..< n'] ⇔ m = m' ∧ n ≤ n')

listRangeINC_11

⊢ ∀m n m' n'. m ≤ n ∧ m' ≤ n' ⇒ ([m .. n] = [m' .. n'] ⇔ m = m' ∧ n = n')

listRangeINC_1_n

⊢ ∀n. [1 .. n] = GENLIST SUC n

listRangeINC_ALL_DISTINCT

⊢ ∀m n. ALL_DISTINCT [m .. n]

listRangeINC_APPEND

⊢ ∀a b c. a ≤ b ∧ b ≤ c ⇒ [a .. b] ⧺ [b + 1 .. c] = [a .. c]

listRangeINC_CONS

⊢ m ≤ n ⇒ [m .. n] = m::[m + 1 .. n]

listRangeINC_EL

⊢ ∀m n i. m + i ≤ n ⇒ [m .. n]❲i❳ = m + i

listRangeINC_EMPTY

⊢ n < m ⇒ [m .. n] = []

listRangeINC_EVERY

⊢ ∀P m n. EVERY P [m .. n] ⇔ ∀x. m ≤ x ∧ x ≤ n ⇒ P x

listRangeINC_EVERY_EXISTS

⊢ ∀P m n. EVERY P [m .. n] ⇔ ¬EXISTS ($¬ ∘ P) [m .. n]

listRangeINC_EVERY_less_last

⊢ ∀P m n. m ≤ n ⇒ (EVERY P [m .. n] ⇔ P n ∧ EVERY P [m ..< n])

listRangeINC_EVERY_span_max

⊢ ∀P m n.
    m < n ∧ P m ∧ ¬P n ⇒ ∃k. m ≤ k ∧ k < n ∧ EVERY P [m .. k] ∧ ¬P (SUC k)

listRangeINC_EVERY_span_min

⊢ ∀P m n.
    m < n ∧ ¬P m ∧ P n ⇒ ∃k. m < k ∧ k ≤ n ∧ EVERY P [k .. n] ∧ ¬P (PRE k)

listRangeINC_EVERY_split_head

⊢ ∀P m n. m ≤ n ⇒ (EVERY P [m − 1 .. n] ⇔ P (m − 1) ∧ EVERY P [m .. n])

listRangeINC_EVERY_split_last

⊢ ∀P m n. m ≤ n ⇒ (EVERY P [m .. n + 1] ⇔ P (n + 1) ∧ EVERY P [m .. n])

listRangeINC_EXISTS

⊢ ∀P m n. EXISTS P [m .. n] ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ P x

listRangeINC_EXISTS_EVERY

⊢ ∀P m n. EXISTS P [m .. n] ⇔ ¬EVERY ($¬ ∘ P) [m .. n]

listRangeINC_FRONT

⊢ ∀m n. m ≤ n + 1 ⇒ FRONT [m .. n + 1] = [m .. n]

listRangeINC_LAST

⊢ ∀m n. m ≤ n ⇒ LAST [m .. n] = n

listRangeINC_LEN

⊢ ∀m n. LENGTH [m .. n] = n + 1 − m

listRangeINC_MAP

⊢ ∀f n. MAP f [1 .. n] = GENLIST (f ∘ SUC) n

listRangeINC_MAP_SUC

⊢ ∀f m n. MAP f [m + 1 .. n + 1] = MAP (f ∘ SUC) [m .. n]

listRangeINC_MEM

⊢ ∀m n x. MEM x [m .. n] ⇔ m ≤ x ∧ x ≤ n

listRangeINC_NIL

⊢ ∀m n. [m .. n] = [] ⇔ n + 1 ≤ m

listRangeINC_REVERSE

⊢ ∀m n. REVERSE [m .. n] = MAP (λx. n − x + m) [m .. n]

listRangeINC_REVERSE_MAP

⊢ ∀f m n. REVERSE (MAP f [m .. n]) = MAP (f ∘ (λx. n − x + m)) [m .. n]

listRangeINC_SET

⊢ ∀n. set [1 .. n] = IMAGE SUC (count n)

listRangeINC_SING

⊢ [m .. m] = [m]

listRangeINC_SNOC

⊢ ∀m n. m ≤ n + 1 ⇒ [m .. n + 1] = SNOC (n + 1) [m .. n]

listRangeINC_SPLIT

⊢ ∀m n j. m < j ∧ j ≤ n ⇒ [m .. n] = [m .. j − 1] ⧺ j::[j + 1 .. n]

listRangeINC_SUM

⊢ ∀m n. SUM [m .. n] = SUM [1 .. n] − SUM [1 .. m − 1]

listRangeINC_SUM_MAP

⊢ ∀f n. SUM (MAP f [1 .. SUC n]) = f (SUC n) + SUM (MAP f [1 .. n])

listRangeINC_has_divisors

⊢ ∀m n x. 0 < n ∧ m ≤ x ∧ x divides n ⇒ MEM x [m .. n]

listRangeINC_to_LHI

⊢ ∀m n. [m .. n] = [m ..< SUC n]

listRangeLHI_0_n

⊢ ∀n. [0 ..< n] = GENLIST I n

listRangeLHI_11

⊢ ∀m n m' n'. m < n ∧ m' < n' ⇒ ([m ..< n] = [m' ..< n'] ⇔ m = m' ∧ n = n')

listRangeLHI_ALL_DISTINCT

⊢ ALL_DISTINCT [lo ..< hi]

listRangeLHI_APPEND

⊢ ∀a b c. a ≤ b ∧ b ≤ c ⇒ [a ..< b] ⧺ [b ..< c] = [a ..< c]

listRangeLHI_CONS

⊢ lo < hi ⇒ [lo ..< hi] = lo::[lo + 1 ..< hi]

listRangeLHI_EL

⊢ ∀m n i. m + i < n ⇒ [m ..< n]❲i❳ = m + i

listRangeLHI_EMPTY

⊢ hi ≤ lo ⇒ [lo ..< hi] = []

listRangeLHI_EQ

⊢ [m ..< m] = []

listRangeLHI_EVERY

⊢ ∀P m n. EVERY P [m ..< n] ⇔ ∀x. m ≤ x ∧ x < n ⇒ P x

listRangeLHI_FRONT

⊢ ∀m n. m ≤ n ⇒ FRONT [m ..< n + 1] = [m ..< n]

listRangeLHI_LAST

⊢ ∀m n. m ≤ n ⇒ LAST [m ..< n + 1] = n

listRangeLHI_LEN

⊢ ∀n m. LENGTH [m ..< n] = n − m

listRangeLHI_MAP

⊢ ∀f n. MAP f [0 ..< n] = GENLIST f n

listRangeLHI_MAP_SUC

⊢ ∀f m n. MAP f [m + 1 ..< n + 1] = MAP (f ∘ SUC) [m ..< n]

listRangeLHI_MEM

⊢ ∀m n x. MEM x [m ..< n] ⇔ m ≤ x ∧ x < n

listRangeLHI_NIL

⊢ ∀m n. [m ..< n] = [] ⇔ n ≤ m

listRangeLHI_REVERSE

⊢ ∀m n. REVERSE [m ..< n] = MAP (λx. n − 1 − x + m) [m ..< n]

listRangeLHI_REVERSE_MAP

⊢ ∀f m n.
    REVERSE (MAP f [m ..< n]) = MAP (f ∘ (λx. n − 1 − x + m)) [m ..< n]

listRangeLHI_SET

⊢ ∀n. set [0 ..< n] = count n

listRangeLHI_SNOC

⊢ ∀m n. m ≤ n ⇒ [m ..< n + 1] = SNOC n [m ..< n]

listRangeLHI_SPLIT

⊢ ∀m n j. m ≤ j ∧ j < n ⇒ [m ..< n] = [m ..< j] ⧺ j::[j + 1 ..< n]

listRangeLHI_SUM

⊢ ∀m n. SUM [m ..< n] = SUM [1 ..< n] − SUM [1 ..< m]

listRangeLHI_SUM_MAP

⊢ ∀f n. SUM (MAP f [0 ..< SUC n]) = f n + SUM (MAP f [0 ..< n])

listRangeLHI_has_divisors

⊢ ∀m n x. 0 < n ∧ m ≤ x ∧ x divides n ⇒ MEM x [m ..< n + 1]

listRangeLHI_to_INC

⊢ ∀m n. [m ..< n + 1] = [m .. n]

Theory listRange

Parents

Contents

Type operators

Constants

Definitions

Theorems

Definitions

Theorems