Structure productTheory

signature productTheory =
sig
  type thm = Thm.thm
  
  (*  Definitions  *)
    val nproduct : thm
    val product : thm
  
  (*  Theorems  *)
    val MULT_AC : thm
    val NPRODUCT_ADD_SPLIT : thm
    val NPRODUCT_CLAUSES : thm
    val NPRODUCT_CLAUSES_LEFT : thm
    val NPRODUCT_CLAUSES_NUMSEG : thm
    val NPRODUCT_CLAUSES_RIGHT : thm
    val NPRODUCT_CLOSED : thm
    val NPRODUCT_CONST : thm
    val NPRODUCT_CONST_NUMSEG : thm
    val NPRODUCT_CONST_NUMSEG_1 : thm
    val NPRODUCT_DELETE : thm
    val NPRODUCT_DELTA : thm
    val NPRODUCT_EQ : thm
    val NPRODUCT_EQ_0 : thm
    val NPRODUCT_EQ_0_NUMSEG : thm
    val NPRODUCT_EQ_1 : thm
    val NPRODUCT_EQ_1_NUMSEG : thm
    val NPRODUCT_EQ_NUMSEG : thm
    val NPRODUCT_FACT : thm
    val NPRODUCT_IMAGE : thm
    val NPRODUCT_LE : thm
    val NPRODUCT_LE_NUMSEG : thm
    val NPRODUCT_MUL : thm
    val NPRODUCT_MUL_GEN : thm
    val NPRODUCT_MUL_NUMSEG : thm
    val NPRODUCT_OFFSET : thm
    val NPRODUCT_ONE : thm
    val NPRODUCT_PAIR : thm
    val NPRODUCT_POS_LT : thm
    val NPRODUCT_POS_LT_NUMSEG : thm
    val NPRODUCT_SING : thm
    val NPRODUCT_SING_NUMSEG : thm
    val NPRODUCT_SUPERSET : thm
    val NPRODUCT_SUPPORT : thm
    val NPRODUCT_UNION : thm
    val PRODUCT_ABS : thm
    val PRODUCT_ADD_SPLIT : thm
    val PRODUCT_CLAUSES : thm
    val PRODUCT_CLAUSES_LEFT : thm
    val PRODUCT_CLAUSES_NUMSEG : thm
    val PRODUCT_CLAUSES_RIGHT : thm
    val PRODUCT_CLOSED : thm
    val PRODUCT_CONG : thm
    val PRODUCT_CONST : thm
    val PRODUCT_CONST_NUMSEG : thm
    val PRODUCT_CONST_NUMSEG_1 : thm
    val PRODUCT_DELETE : thm
    val PRODUCT_DELTA : thm
    val PRODUCT_DIV : thm
    val PRODUCT_DIV_NUMSEG : thm
    val PRODUCT_EQ : thm
    val PRODUCT_EQ_0 : thm
    val PRODUCT_EQ_0_NUMSEG : thm
    val PRODUCT_EQ_1 : thm
    val PRODUCT_EQ_1_NUMSEG : thm
    val PRODUCT_EQ_NUMSEG : thm
    val PRODUCT_IMAGE : thm
    val PRODUCT_INV : thm
    val PRODUCT_LE : thm
    val PRODUCT_LE_1 : thm
    val PRODUCT_LE_NUMSEG : thm
    val PRODUCT_MUL : thm
    val PRODUCT_MUL_GEN : thm
    val PRODUCT_MUL_NUMSEG : thm
    val PRODUCT_NEG : thm
    val PRODUCT_NEG_NUMSEG : thm
    val PRODUCT_NEG_NUMSEG_1 : thm
    val PRODUCT_OFFSET : thm
    val PRODUCT_ONE : thm
    val PRODUCT_PAIR : thm
    val PRODUCT_POS_LE : thm
    val PRODUCT_POS_LE_NUMSEG : thm
    val PRODUCT_POS_LT : thm
    val PRODUCT_POS_LT_NUMSEG : thm
    val PRODUCT_SING : thm
    val PRODUCT_SING_NUMSEG : thm
    val PRODUCT_SUPERSET : thm
    val PRODUCT_SUPPORT : thm
    val PRODUCT_UNION : thm
    val REAL_ADD_AC : thm
    val REAL_OF_NUM_NPRODUCT : thm
    val th : thm
  
  val product_grammars : type_grammar.grammar * term_grammar.grammar
(*
   [iterate] Parent theory of "product"
   
   [nproduct]  Definition
      
      ⊢ nproduct = iterate $*
   
   [product]  Definition
      
      ⊢ product = iterate $*
   
   [MULT_AC]  Theorem
      
      ⊢ m * n = n * m ∧ m * n * p = m * (n * p) ∧ m * (n * p) = n * (m * p)
   
   [NPRODUCT_ADD_SPLIT]  Theorem
      
      ⊢ ∀f m n p.
          m ≤ n + 1 ⇒
          nproduct (m .. n + p) f =
          nproduct (m .. n) f * nproduct (n + 1 .. n + p) f
   
   [NPRODUCT_CLAUSES]  Theorem
      
      ⊢ (∀f. nproduct ∅ f = 1) ∧
        ∀x f s.
          FINITE s ⇒
          nproduct (x INSERT s) f =
          if x ∈ s then nproduct s f else f x * nproduct s f
   
   [NPRODUCT_CLAUSES_LEFT]  Theorem
      
      ⊢ ∀f m n. m ≤ n ⇒ nproduct (m .. n) f = f m * nproduct (m + 1 .. n) f
   
   [NPRODUCT_CLAUSES_NUMSEG]  Theorem
      
      ⊢ (∀m. nproduct (m .. 0) f = if m = 0 then f 0 else 1) ∧
        ∀m n.
          nproduct (m .. SUC n) f =
          if m ≤ SUC n then nproduct (m .. n) f * f (SUC n)
          else nproduct (m .. n) f
   
   [NPRODUCT_CLAUSES_RIGHT]  Theorem
      
      ⊢ ∀f m n.
          0 < n ∧ m ≤ n ⇒
          nproduct (m .. n) f = nproduct (m .. n − 1) f * f n
   
   [NPRODUCT_CLOSED]  Theorem
      
      ⊢ ∀P f s.
          P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
          P (nproduct s f)
   
   [NPRODUCT_CONST]  Theorem
      
      ⊢ ∀c s. FINITE s ⇒ nproduct s (λx. c) = c ** CARD s
   
   [NPRODUCT_CONST_NUMSEG]  Theorem
      
      ⊢ ∀c m n. nproduct (m .. n) (λx. c) = c ** (n + 1 − m)
   
   [NPRODUCT_CONST_NUMSEG_1]  Theorem
      
      ⊢ ∀c n. nproduct (1 .. n) (λx. c) = c ** n
   
   [NPRODUCT_DELETE]  Theorem
      
      ⊢ ∀f s a.
          FINITE s ∧ a ∈ s ⇒ f a * nproduct (s DELETE a) f = nproduct s f
   
   [NPRODUCT_DELTA]  Theorem
      
      ⊢ ∀s a.
          nproduct s (λx. if x = a then b else 1) = if a ∈ s then b else 1
   
   [NPRODUCT_EQ]  Theorem
      
      ⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ nproduct s f = nproduct s g
   
   [NPRODUCT_EQ_0]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ (nproduct s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)
   
   [NPRODUCT_EQ_0_NUMSEG]  Theorem
      
      ⊢ ∀f m n. nproduct (m .. n) f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0
   
   [NPRODUCT_EQ_1]  Theorem
      
      ⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ nproduct s f = 1
   
   [NPRODUCT_EQ_1_NUMSEG]  Theorem
      
      ⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ nproduct (m .. n) f = 1
   
   [NPRODUCT_EQ_NUMSEG]  Theorem
      
      ⊢ ∀f g m n.
          (∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
          nproduct (m .. n) f = nproduct (m .. n) g
   
   [NPRODUCT_FACT]  Theorem
      
      ⊢ ∀n. nproduct (1 .. n) (λm. m) = FACT n
   
   [NPRODUCT_IMAGE]  Theorem
      
      ⊢ ∀f g s.
          (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
          nproduct (IMAGE f s) g = nproduct s (g ∘ f)
   
   [NPRODUCT_LE]  Theorem
      
      ⊢ ∀f s.
          FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒
          nproduct s f ≤ nproduct s g
   
   [NPRODUCT_LE_NUMSEG]  Theorem
      
      ⊢ ∀f m n.
          (∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
          nproduct (m .. n) f ≤ nproduct (m .. n) g
   
   [NPRODUCT_MUL]  Theorem
      
      ⊢ ∀f g s.
          FINITE s ⇒
          nproduct s (λx. f x * g x) = nproduct s f * nproduct s g
   
   [NPRODUCT_MUL_GEN]  Theorem
      
      ⊢ ∀f g s.
          FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
          nproduct s (λx. f x * g x) = nproduct s f * nproduct s g
   
   [NPRODUCT_MUL_NUMSEG]  Theorem
      
      ⊢ ∀f g m n.
          nproduct (m .. n) (λx. f x * g x) =
          nproduct (m .. n) f * nproduct (m .. n) g
   
   [NPRODUCT_OFFSET]  Theorem
      
      ⊢ ∀f m p.
          nproduct (m + p .. n + p) f = nproduct (m .. n) (λi. f (i + p))
   
   [NPRODUCT_ONE]  Theorem
      
      ⊢ ∀s. nproduct s (λn. 1) = 1
   
   [NPRODUCT_PAIR]  Theorem
      
      ⊢ ∀f m n.
          nproduct (2 * m .. 2 * n + 1) f =
          nproduct (m .. n) (λi. f (2 * i) * f (2 * i + 1))
   
   [NPRODUCT_POS_LT]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < nproduct s f
   
   [NPRODUCT_POS_LT_NUMSEG]  Theorem
      
      ⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < nproduct (m .. n) f
   
   [NPRODUCT_SING]  Theorem
      
      ⊢ ∀f x. nproduct {x} f = f x
   
   [NPRODUCT_SING_NUMSEG]  Theorem
      
      ⊢ ∀f n. nproduct (n .. n) f = f n
   
   [NPRODUCT_SUPERSET]  Theorem
      
      ⊢ ∀f u v.
          u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒
          nproduct v f = nproduct u f
   
   [NPRODUCT_SUPPORT]  Theorem
      
      ⊢ ∀f s. nproduct (support $* f s) f = nproduct s f
   
   [NPRODUCT_UNION]  Theorem
      
      ⊢ ∀f s t.
          FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
          nproduct (s ∪ t) f = nproduct s f * nproduct t f
   
   [PRODUCT_ABS]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ product s (λx. abs (f x)) = abs (product s f)
   
   [PRODUCT_ADD_SPLIT]  Theorem
      
      ⊢ ∀f m n p.
          m ≤ n + 1 ⇒
          product (m .. n + p) f =
          product (m .. n) f * product (n + 1 .. n + p) f
   
   [PRODUCT_CLAUSES]  Theorem
      
      ⊢ (∀f. product ∅ f = 1) ∧
        ∀x f s.
          FINITE s ⇒
          product (x INSERT s) f =
          if x ∈ s then product s f else f x * product s f
   
   [PRODUCT_CLAUSES_LEFT]  Theorem
      
      ⊢ ∀f m n. m ≤ n ⇒ product (m .. n) f = f m * product (m + 1 .. n) f
   
   [PRODUCT_CLAUSES_NUMSEG]  Theorem
      
      ⊢ (∀m. product (m .. 0) f = if m = 0 then f 0 else 1) ∧
        ∀m n.
          product (m .. SUC n) f =
          if m ≤ SUC n then product (m .. n) f * f (SUC n)
          else product (m .. n) f
   
   [PRODUCT_CLAUSES_RIGHT]  Theorem
      
      ⊢ ∀f m n.
          0 < n ∧ m ≤ n ⇒ product (m .. n) f = product (m .. n − 1) f * f n
   
   [PRODUCT_CLOSED]  Theorem
      
      ⊢ ∀P f s.
          P 1 ∧ (∀x y. P x ∧ P y ⇒ P (x * y)) ∧ (∀a. a ∈ s ⇒ P (f a)) ⇒
          P (product s f)
   
   [PRODUCT_CONG]  Theorem
      
      ⊢ (∀f g s.
           (∀x. x ∈ s ⇒ f x = g x) ⇒ product s (λi. f i) = product s g) ∧
        (∀f g a b.
           (∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
           product (a .. b) (λi. f i) = product (a .. b) g) ∧
        ∀f g p.
          (∀x. p x ⇒ f x = g x) ⇒
          product {y | p y} (λi. f i) = product {y | p y} g
   
   [PRODUCT_CONST]  Theorem
      
      ⊢ ∀c s. FINITE s ⇒ product s (λx. c) = c pow CARD s
   
   [PRODUCT_CONST_NUMSEG]  Theorem
      
      ⊢ ∀c m n. product (m .. n) (λx. c) = c pow (n + 1 − m)
   
   [PRODUCT_CONST_NUMSEG_1]  Theorem
      
      ⊢ ∀c n. product (1 .. n) (λx. c) = c pow n
   
   [PRODUCT_DELETE]  Theorem
      
      ⊢ ∀f s a.
          FINITE s ∧ a ∈ s ⇒ f a * product (s DELETE a) f = product s f
   
   [PRODUCT_DELTA]  Theorem
      
      ⊢ ∀s a.
          product s (λx. if x = a then b else 1) = if a ∈ s then b else 1
   
   [PRODUCT_DIV]  Theorem
      
      ⊢ ∀f g s.
          FINITE s ⇒ product s (λx. f x / g x) = product s f / product s g
   
   [PRODUCT_DIV_NUMSEG]  Theorem
      
      ⊢ ∀f g m n.
          product (m .. n) (λx. f x / g x) =
          product (m .. n) f / product (m .. n) g
   
   [PRODUCT_EQ]  Theorem
      
      ⊢ ∀f g s. (∀x. x ∈ s ⇒ f x = g x) ⇒ product s f = product s g
   
   [PRODUCT_EQ_0]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ (product s f = 0 ⇔ ∃x. x ∈ s ∧ f x = 0)
   
   [PRODUCT_EQ_0_NUMSEG]  Theorem
      
      ⊢ ∀f m n. product (m .. n) f = 0 ⇔ ∃x. m ≤ x ∧ x ≤ n ∧ f x = 0
   
   [PRODUCT_EQ_1]  Theorem
      
      ⊢ ∀f s. (∀x. x ∈ s ⇒ f x = 1) ⇒ product s f = 1
   
   [PRODUCT_EQ_1_NUMSEG]  Theorem
      
      ⊢ ∀f m n. (∀i. m ≤ i ∧ i ≤ n ⇒ f i = 1) ⇒ product (m .. n) f = 1
   
   [PRODUCT_EQ_NUMSEG]  Theorem
      
      ⊢ ∀f g m n.
          (∀i. m ≤ i ∧ i ≤ n ⇒ f i = g i) ⇒
          product (m .. n) f = product (m .. n) g
   
   [PRODUCT_IMAGE]  Theorem
      
      ⊢ ∀f g s.
          (∀x y. x ∈ s ∧ y ∈ s ∧ f x = f y ⇒ x = y) ⇒
          product (IMAGE f s) g = product s (g ∘ f)
   
   [PRODUCT_INV]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ product s (λx. (f x)⁻¹) = (product s f)⁻¹
   
   [PRODUCT_LE]  Theorem
      
      ⊢ ∀f s.
          FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ g x) ⇒
          product s f ≤ product s g
   
   [PRODUCT_LE_1]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x ∧ f x ≤ 1) ⇒ product s f ≤ 1
   
   [PRODUCT_LE_NUMSEG]  Theorem
      
      ⊢ ∀f m n.
          (∀i. m ≤ i ∧ i ≤ n ⇒ 0 ≤ f i ∧ f i ≤ g i) ⇒
          product (m .. n) f ≤ product (m .. n) g
   
   [PRODUCT_MUL]  Theorem
      
      ⊢ ∀f g s.
          FINITE s ⇒ product s (λx. f x * g x) = product s f * product s g
   
   [PRODUCT_MUL_GEN]  Theorem
      
      ⊢ ∀f g s.
          FINITE {x | x ∈ s ∧ f x ≠ 1} ∧ FINITE {x | x ∈ s ∧ g x ≠ 1} ⇒
          product s (λx. f x * g x) = product s f * product s g
   
   [PRODUCT_MUL_NUMSEG]  Theorem
      
      ⊢ ∀f g m n.
          product (m .. n) (λx. f x * g x) =
          product (m .. n) f * product (m .. n) g
   
   [PRODUCT_NEG]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ product s (λi. -f i) = -1 pow CARD s * product s f
   
   [PRODUCT_NEG_NUMSEG]  Theorem
      
      ⊢ ∀f m n.
          product (m .. n) (λi. -f i) =
          -1 pow (n + 1 − m) * product (m .. n) f
   
   [PRODUCT_NEG_NUMSEG_1]  Theorem
      
      ⊢ ∀f n. product (1 .. n) (λi. -f i) = -1 pow n * product (1 .. n) f
   
   [PRODUCT_OFFSET]  Theorem
      
      ⊢ ∀f m p.
          product (m + p .. n + p) f = product (m .. n) (λi. f (i + p))
   
   [PRODUCT_ONE]  Theorem
      
      ⊢ ∀s. product s (λn. 1) = 1
   
   [PRODUCT_PAIR]  Theorem
      
      ⊢ ∀f m n.
          product (2 * m .. 2 * n + 1) f =
          product (m .. n) (λi. f (2 * i) * f (2 * i + 1))
   
   [PRODUCT_POS_LE]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 ≤ f x) ⇒ 0 ≤ product s f
   
   [PRODUCT_POS_LE_NUMSEG]  Theorem
      
      ⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 ≤ f x) ⇒ 0 ≤ product (m .. n) f
   
   [PRODUCT_POS_LT]  Theorem
      
      ⊢ ∀f s. FINITE s ∧ (∀x. x ∈ s ⇒ 0 < f x) ⇒ 0 < product s f
   
   [PRODUCT_POS_LT_NUMSEG]  Theorem
      
      ⊢ ∀f m n. (∀x. m ≤ x ∧ x ≤ n ⇒ 0 < f x) ⇒ 0 < product (m .. n) f
   
   [PRODUCT_SING]  Theorem
      
      ⊢ ∀f x. product {x} f = f x
   
   [PRODUCT_SING_NUMSEG]  Theorem
      
      ⊢ ∀f n. product (n .. n) f = f n
   
   [PRODUCT_SUPERSET]  Theorem
      
      ⊢ ∀f u v.
          u ⊆ v ∧ (∀x. x ∈ v ∧ x ∉ u ⇒ f x = 1) ⇒ product v f = product u f
   
   [PRODUCT_SUPPORT]  Theorem
      
      ⊢ ∀f s. product (support $* f s) f = product s f
   
   [PRODUCT_UNION]  Theorem
      
      ⊢ ∀f s t.
          FINITE s ∧ FINITE t ∧ DISJOINT s t ⇒
          product (s ∪ t) f = product s f * product t f
   
   [REAL_ADD_AC]  Theorem
      
      ⊢ m + n = n + m ∧ m + n + p = m + (n + p) ∧ m + (n + p) = n + (m + p)
   
   [REAL_OF_NUM_NPRODUCT]  Theorem
      
      ⊢ ∀f s. FINITE s ⇒ &nproduct s f = product s (λx. &f x)
   
   [th]  Theorem
      
      ⊢ (∀f g s.
           (∀x. x ∈ s ⇒ f x = g x) ⇒ nproduct s (λi. f i) = nproduct s g) ∧
        (∀f g a b.
           (∀i. a ≤ i ∧ i ≤ b ⇒ f i = g i) ⇒
           nproduct (a .. b) (λi. f i) = nproduct (a .. b) g) ∧
        ∀f g p.
          (∀x. p x ⇒ f x = g x) ⇒
          nproduct {y | p y} (λi. f i) = nproduct {y | p y} g
   
   
*)
end

HOL 4, Kananaskis-14