Structure listRangeTheory

signature listRangeTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val listRangeINC_def : thm
    val listRangeLHI_def : thm
  
  (*  Theorems  *)
    val EL_listRangeLHI : thm
    val LENGTH_listRangeLHI : thm
    val MEM_listRangeINC : thm
    val MEM_listRangeLHI : thm
    val every_range_cons : thm
    val every_range_less_ends : thm
    val every_range_sing : thm
    val every_range_span_max : thm
    val every_range_span_min : thm
    val every_range_split_head : thm
    val every_range_split_last : thm
    val exists_range_cons : thm
    val exists_range_sing : thm
    val isPREFIX_listRangeINC : thm
    val isPREFIX_listRangeINC_EQ : thm
    val isPREFIX_listRangeLHI : thm
    val isPREFIX_listRangeLHI_EQ : thm
    val listRangeINC_11 : thm
    val listRangeINC_1_n : thm
    val listRangeINC_ALL_DISTINCT : thm
    val listRangeINC_APPEND : thm
    val listRangeINC_CONS : thm
    val listRangeINC_EL : thm
    val listRangeINC_EMPTY : thm
    val listRangeINC_EVERY : thm
    val listRangeINC_EVERY_EXISTS : thm
    val listRangeINC_EVERY_less_last : thm
    val listRangeINC_EVERY_span_max : thm
    val listRangeINC_EVERY_span_min : thm
    val listRangeINC_EVERY_split_head : thm
    val listRangeINC_EVERY_split_last : thm
    val listRangeINC_EXISTS : thm
    val listRangeINC_EXISTS_EVERY : thm
    val listRangeINC_FRONT : thm
    val listRangeINC_LAST : thm
    val listRangeINC_LEN : thm
    val listRangeINC_MAP : thm
    val listRangeINC_MAP_SUC : thm
    val listRangeINC_MEM : thm
    val listRangeINC_NIL : thm
    val listRangeINC_REVERSE : thm
    val listRangeINC_REVERSE_MAP : thm
    val listRangeINC_SET : thm
    val listRangeINC_SING : thm
    val listRangeINC_SNOC : thm
    val listRangeINC_SPLIT : thm
    val listRangeINC_SUM : thm
    val listRangeINC_SUM_MAP : thm
    val listRangeINC_has_divisors : thm
    val listRangeINC_to_LHI : thm
    val listRangeLHI_0_n : thm
    val listRangeLHI_11 : thm
    val listRangeLHI_ALL_DISTINCT : thm
    val listRangeLHI_APPEND : thm
    val listRangeLHI_CONS : thm
    val listRangeLHI_EL : thm
    val listRangeLHI_EMPTY : thm
    val listRangeLHI_EQ : thm
    val listRangeLHI_EVERY : thm
    val listRangeLHI_FRONT : thm
    val listRangeLHI_LAST : thm
    val listRangeLHI_LEN : thm
    val listRangeLHI_MAP : thm
    val listRangeLHI_MAP_SUC : thm
    val listRangeLHI_MEM : thm
    val listRangeLHI_NIL : thm
    val listRangeLHI_REVERSE : thm
    val listRangeLHI_REVERSE_MAP : thm
    val listRangeLHI_SET : thm
    val listRangeLHI_SNOC : thm
    val listRangeLHI_SPLIT : thm
    val listRangeLHI_SUM : thm
    val listRangeLHI_SUM_MAP : thm
    val listRangeLHI_has_divisors : thm
    val listRangeLHI_to_INC : thm
(*
   [list] Parent theory of "listRange"
   
   [listRangeINC_def]  Definition
      
      ⊢ ∀m n. [m .. n] = GENLIST (λi. m + i) (n + 1 − m)
   
   [listRangeLHI_def]  Definition
      
      ⊢ ∀m n. [m ..< n] = GENLIST (λi. m + i) (n − m)
   
   [EL_listRangeLHI]  Theorem
      
      ⊢ lo + i < hi ⇒ EL i [lo ..< hi] = lo + i
   
   [LENGTH_listRangeLHI]  Theorem
      
      ⊢ LENGTH [lo ..< hi] = hi − lo
   
   [MEM_listRangeINC]  Theorem
      
      ⊢ MEM x [m .. n] ⇔ m ≤ x ∧ x ≤ n
   
   [MEM_listRangeLHI]  Theorem
      
      ⊢ MEM x [m ..< n] ⇔ m ≤ x ∧ x < n
   
   [every_range_cons]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a j. a ≤ j ∧ j ≤ a ⇔ j = a
   
   [every_range_span_max]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀a. ∃j. a ≤ j ∧ j ≤ a ⇔ j = a
   
   [isPREFIX_listRangeINC]  Theorem
      
      ⊢ ∀m n m' n'. m = m' ∧ n ≤ n' ⇒ [m .. n] ≼ [m' .. n']
   
   [isPREFIX_listRangeINC_EQ]  Theorem
      
      ⊢ ∀m n m' n'.
          m ≤ n ∧ m' ≤ n' ⇒ ([m .. n] ≼ [m' .. n'] ⇔ m = m' ∧ n ≤ n')
   
   [isPREFIX_listRangeLHI]  Theorem
      
      ⊢ ∀m n m' n'. m = m' ∧ n ≤ n' ⇒ [m ..< n] ≼ [m' ..< n']
   
   [isPREFIX_listRangeLHI_EQ]  Theorem
      
      ⊢ ∀m n m' n'.
          m < n ∧ m' < n' ⇒ ([m ..< n] ≼ [m' ..< n'] ⇔ m = m' ∧ n ≤ n')
   
   [listRangeINC_11]  Theorem
      
      ⊢ ∀m n m' n'.
          m ≤ n ∧ m' ≤ n' ⇒ ([m .. n] = [m' .. n'] ⇔ m = m' ∧ n = n')
   
   [listRangeINC_1_n]  Theorem
      
      ⊢ ∀n. [1 .. n] = GENLIST SUC n
   
   [listRangeINC_ALL_DISTINCT]  Theorem
      
      ⊢ ∀m n. ALL_DISTINCT [m .. n]
   
   [listRangeINC_APPEND]  Theorem
      
      ⊢ ∀a b c. a ≤ b ∧ b ≤ c ⇒ [a .. b] ⧺ [b + 1 .. c] = [a .. c]
   
   [listRangeINC_CONS]  Theorem
      
      ⊢ m ≤ n ⇒ [m .. n] = m::[m + 1 .. n]
   
   [listRangeINC_EL]  Theorem
      
      ⊢ ∀m n i. m + i ≤ n ⇒ EL i [m .. n] = m + i
   
   [listRangeINC_EMPTY]  Theorem
      
      ⊢ n < m ⇒ [m .. n] = []
   
   [listRangeINC_EVERY]  Theorem
      
      ⊢ ∀P m n. EVERY P [m .. n] ⇔ ∀x. m ≤ x ∧ x ≤ n ⇒ P x
   
   [listRangeINC_EVERY_EXISTS]  Theorem
      
      ⊢ ∀P m n. EVERY P [m .. n] ⇔ ¬EXISTS ($¬ ∘ P) [m .. n]
   
   [listRangeINC_EVERY_less_last]  Theorem
      
      ⊢ ∀P m n. m ≤ n ⇒ (EVERY P [m .. n] ⇔ P n ∧ EVERY P [m ..< n])
   
   [listRangeINC_EVERY_span_max]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀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]  Theorem
      
      ⊢ ∀P m n.
          m ≤ n ⇒ (EVERY P [m − 1 .. n] ⇔ P (m − 1) ∧ EVERY P [m .. n])
   
   [listRangeINC_EVERY_split_last]  Theorem
      
      ⊢ ∀P m n.
          m ≤ n ⇒ (EVERY P [m .. n + 1] ⇔ P (n + 1) ∧ EVERY P [m .. n])
   
   [listRangeINC_EXISTS]  Theorem
      
      ⊢ ∀P m n. EXISTS P [m .. n] ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ P x
   
   [listRangeINC_EXISTS_EVERY]  Theorem
      
      ⊢ ∀P m n. EXISTS P [m .. n] ⇔ ¬EVERY ($¬ ∘ P) [m .. n]
   
   [listRangeINC_FRONT]  Theorem
      
      ⊢ ∀m n. m ≤ n + 1 ⇒ FRONT [m .. n + 1] = [m .. n]
   
   [listRangeINC_LAST]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ LAST [m .. n] = n
   
   [listRangeINC_LEN]  Theorem
      
      ⊢ ∀m n. LENGTH [m .. n] = n + 1 − m
   
   [listRangeINC_MAP]  Theorem
      
      ⊢ ∀f n. MAP f [1 .. n] = GENLIST (f ∘ SUC) n
   
   [listRangeINC_MAP_SUC]  Theorem
      
      ⊢ ∀f m n. MAP f [m + 1 .. n + 1] = MAP (f ∘ SUC) [m .. n]
   
   [listRangeINC_MEM]  Theorem
      
      ⊢ ∀m n x. MEM x [m .. n] ⇔ m ≤ x ∧ x ≤ n
   
   [listRangeINC_NIL]  Theorem
      
      ⊢ ∀m n. [m .. n] = [] ⇔ n + 1 ≤ m
   
   [listRangeINC_REVERSE]  Theorem
      
      ⊢ ∀m n. REVERSE [m .. n] = MAP (λx. n − x + m) [m .. n]
   
   [listRangeINC_REVERSE_MAP]  Theorem
      
      ⊢ ∀f m n.
          REVERSE (MAP f [m .. n]) = MAP (f ∘ (λx. n − x + m)) [m .. n]
   
   [listRangeINC_SET]  Theorem
      
      ⊢ ∀n. set [1 .. n] = IMAGE SUC (count n)
   
   [listRangeINC_SING]  Theorem
      
      ⊢ [m .. m] = [m]
   
   [listRangeINC_SNOC]  Theorem
      
      ⊢ ∀m n. m ≤ n + 1 ⇒ [m .. n + 1] = SNOC (n + 1) [m .. n]
   
   [listRangeINC_SPLIT]  Theorem
      
      ⊢ ∀m n j. m < j ∧ j ≤ n ⇒ [m .. n] = [m .. j − 1] ⧺ j::[j + 1 .. n]
   
   [listRangeINC_SUM]  Theorem
      
      ⊢ ∀m n. SUM [m .. n] = SUM [1 .. n] − SUM [1 .. m − 1]
   
   [listRangeINC_SUM_MAP]  Theorem
      
      ⊢ ∀f n. SUM (MAP f [1 .. SUC n]) = f (SUC n) + SUM (MAP f [1 .. n])
   
   [listRangeINC_has_divisors]  Theorem
      
      ⊢ ∀m n x. 0 < n ∧ m ≤ x ∧ x divides n ⇒ MEM x [m .. n]
   
   [listRangeINC_to_LHI]  Theorem
      
      ⊢ ∀m n. [m .. n] = [m ..< SUC n]
   
   [listRangeLHI_0_n]  Theorem
      
      ⊢ ∀n. [0 ..< n] = GENLIST I n
   
   [listRangeLHI_11]  Theorem
      
      ⊢ ∀m n m' n'.
          m < n ∧ m' < n' ⇒ ([m ..< n] = [m' ..< n'] ⇔ m = m' ∧ n = n')
   
   [listRangeLHI_ALL_DISTINCT]  Theorem
      
      ⊢ ALL_DISTINCT [lo ..< hi]
   
   [listRangeLHI_APPEND]  Theorem
      
      ⊢ ∀a b c. a ≤ b ∧ b ≤ c ⇒ [a ..< b] ⧺ [b ..< c] = [a ..< c]
   
   [listRangeLHI_CONS]  Theorem
      
      ⊢ lo < hi ⇒ [lo ..< hi] = lo::[lo + 1 ..< hi]
   
   [listRangeLHI_EL]  Theorem
      
      ⊢ ∀m n i. m + i < n ⇒ EL i [m ..< n] = m + i
   
   [listRangeLHI_EMPTY]  Theorem
      
      ⊢ hi ≤ lo ⇒ [lo ..< hi] = []
   
   [listRangeLHI_EQ]  Theorem
      
      ⊢ [m ..< m] = []
   
   [listRangeLHI_EVERY]  Theorem
      
      ⊢ ∀P m n. EVERY P [m ..< n] ⇔ ∀x. m ≤ x ∧ x < n ⇒ P x
   
   [listRangeLHI_FRONT]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ FRONT [m ..< n + 1] = [m ..< n]
   
   [listRangeLHI_LAST]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ LAST [m ..< n + 1] = n
   
   [listRangeLHI_LEN]  Theorem
      
      ⊢ ∀n m. LENGTH [m ..< n] = n − m
   
   [listRangeLHI_MAP]  Theorem
      
      ⊢ ∀f n. MAP f [0 ..< n] = GENLIST f n
   
   [listRangeLHI_MAP_SUC]  Theorem
      
      ⊢ ∀f m n. MAP f [m + 1 ..< n + 1] = MAP (f ∘ SUC) [m ..< n]
   
   [listRangeLHI_MEM]  Theorem
      
      ⊢ ∀m n x. MEM x [m ..< n] ⇔ m ≤ x ∧ x < n
   
   [listRangeLHI_NIL]  Theorem
      
      ⊢ ∀m n. [m ..< n] = [] ⇔ n ≤ m
   
   [listRangeLHI_REVERSE]  Theorem
      
      ⊢ ∀m n. REVERSE [m ..< n] = MAP (λx. n − 1 − x + m) [m ..< n]
   
   [listRangeLHI_REVERSE_MAP]  Theorem
      
      ⊢ ∀f m n.
          REVERSE (MAP f [m ..< n]) =
          MAP (f ∘ (λx. n − 1 − x + m)) [m ..< n]
   
   [listRangeLHI_SET]  Theorem
      
      ⊢ ∀n. set [0 ..< n] = count n
   
   [listRangeLHI_SNOC]  Theorem
      
      ⊢ ∀m n. m ≤ n ⇒ [m ..< n + 1] = SNOC n [m ..< n]
   
   [listRangeLHI_SPLIT]  Theorem
      
      ⊢ ∀m n j. m ≤ j ∧ j < n ⇒ [m ..< n] = [m ..< j] ⧺ j::[j + 1 ..< n]
   
   [listRangeLHI_SUM]  Theorem
      
      ⊢ ∀m n. SUM [m ..< n] = SUM [1 ..< n] − SUM [1 ..< m]
   
   [listRangeLHI_SUM_MAP]  Theorem
      
      ⊢ ∀f n. SUM (MAP f [0 ..< SUC n]) = f n + SUM (MAP f [0 ..< n])
   
   [listRangeLHI_has_divisors]  Theorem
      
      ⊢ ∀m n x. 0 < n ∧ m ≤ x ∧ x divides n ⇒ MEM x [m ..< n + 1]
   
   [listRangeLHI_to_INC]  Theorem
      
      ⊢ ∀m n. [m ..< n + 1] = [m .. n]
   
   
*)
end

HOL 4, Trindemossen-2