[isabelle] Indexed Sum/Product Operator



Dear Isabelle Users,

I was playing with the exercise below, and I wanted to find the
theory where the indexed sum operator is defined.

I tried  find_consts name: Sum, but this does not seem to
be the way.

Thanks for any help!

theorem sum02: "∑{0..n::nat} = n * (n+1) div 2" (is "?P n")
  proof (induction n)
    show "?P 0"
       proof -
         have "∑{0..0::nat} = 0" by simp
         also have "...= 0 * 0" by simp
         also have "... = 0 * (0 + 1)" by simp
         also have "... = (0 * (0 + 1)) div 2" by simp
         finally show ?thesis by this
       qed
    next
      fix x0::nat
      assume IH: "?P x0"
      show "?P (Suc x0)"
        proof -
            have "∑{0..(Suc x0)} = ∑{0..x0} + Suc x0" by simp
            also have  "...= ∑{0..x0} + (x0 + 1)" by simp
            also have  "...= (x0 * (x0 + 1) div 2) + (x0 + 1)" by (simp
only: IH)
            also have  "...= (x0 * (x0 + 1) + 2 * x0 + 2) div 2" by simp
            also have  "...= (x0 * x0 + x0 + 2*x0 + 2) div 2" by simp
            also have  "...= (x0 * x0 + 3*x0 +2) div 2" by simp
            also have  "...= (x0 + 1) * (x0 + 2) div 2" by simp
            also have  "...= Suc x0 * (Suc x0 + 1) div 2" by simp
            finally show ?thesis by this
        qed
  qed

-- 
Alfio Ricardo Martini
PhD in Computer Science (TU Berlin)
Associate Professor at Faculty of Informatics (PUCRS)
Coordenador do Curso de Ciência da Computação
Av. Ipiranga, 6681 - Prédio 32 - Faculdade de Informática
90619-900 -Porto Alegre - RS - Brasil




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.