Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Quellcodebibliothek Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/VDM/VDMSL/looseSL/ (Wiener Entwicklungsmethode ^©) Datei vom 13.4.2020 mit Größe 11 kB

Quelle NatSum.thy Sprache: Isabelle

(*  Title:      HOL/ex/NatSum.thy
    Author:     Tobias Nipkow
*)

section \<open>Summing natural numbers\<close>

theory NatSum
  imports Main
begin

text \<open>
  Summing natural numbers, squares, cubes, etc.

  Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
  \<^url>\<open>https://oeis.org\<close>.
\<close>

lemmas [simp] =
  ring_distribs
  diff_mult_distrib diff_mult_distrib2 \<comment> \<open>for type nat\<close>

text \<open>\<^medskip> The sum of the first \<open>n\<close> odd numbers equals \<open>n\<close> squared.\<close>

lemma sum_of_odds: "(\i=0..
  by (induct n) auto

text \<open>\<^medskip> The sum of the first \<open>n\<close> odd squares.\<close>

lemma sum_of_odd_squares:
  "3 * (\i=0..
  by (induct n) auto

text \<open>\<^medskip> The sum of the first \<open>n\<close> odd cubes.\<close>

lemma sum_of_odd_cubes:
  "(\i=0..
    n * n * (2 * n * n - 1)"
  by (induct n) auto

text \<open>\<^medskip> The sum of the first \<open>n\<close> positive integers equals \<open>n (n + 1) / 2\<close>.\<close>

lemma sum_of_naturals: "2 * (\i=0..n. i) = n * Suc n"
  by (induct n) auto

lemma sum_of_squares: "6 * (\i=0..n. i * i) = n * Suc n * Suc (2 * n)"
  by (induct n) auto

lemma sum_of_cubes: "4 * (\i=0..n. i * i * i) = n * n * Suc n * Suc n"
  by (induct n) auto

text \<open>\<^medskip> A cute identity:\<close>

lemma sum_squared: "(\i=0..n. i)^2 = (\i=0..n. i^3)" for n :: nat
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  have "(\i = 0..Suc n. i)^2 =
        (\<Sum>i = 0..n. i^3) + (2*(\<Sum>i = 0..n. i)*(n+1) + (n+1)^2)"
    (is "_ = ?A + ?B")
    using Suc by (simp add: eval_nat_numeral)
  also have "?B = (n+1)^3"
    using sum_of_naturals by (simp add: eval_nat_numeral)
  also have "?A + (n+1)^3 = (\i=0..Suc n. i^3)" by simp
  finally show ?case .
qed

text \<open>\<^medskip> Sum of fourth powers: three versions.\<close>

lemma sum_of_fourth_powers:
  "30 * (\i=0..n. i * i * i * i) =
    n * Suc n * Suc (2 * n) * (3 * n * n + 3 * n - 1)"
proof (induct n)
  case 0
  show ?case by simp
next
  case (Suc n)
  then show ?case
    by (cases n)  \<comment> \<open>eliminates the subtraction\<close>
      simp_all
qed

text \<open>
  Two alternative proofs, with a change of variables and much more
  subtraction, performed using the integers.
\<close>

lemma int_sum_of_fourth_powers:
  "30 * int (\i=0..
    int m * (int m - 1) * (int(2 * m) - 1) *
    (int(3 * m * m) - int(3 * m) - 1)"
  by (induct m) simp_all

lemma of_nat_sum_of_fourth_powers:
  "30 * of_nat (\i=0..
    of_nat m * (of_nat m - 1) * (of_nat (2 * m) - 1) *
    (of_nat (3 * m * m) - of_nat (3 * m) - (1::int))"
  by (induct m) simp_all

text \<open>\<^medskip> Sums of geometric series: \<open>2\<close>, \<open>3\<close> and the general case.\<close>

lemma sum_of_2_powers: "(\i=0..
  by (induct n) auto

lemma sum_of_3_powers: "2 * (\i=0..
  by (induct n) auto

lemma sum_of_powers: "0 < k \ (k - 1) * (\i=0..
  for k :: nat
  by (induct n) auto

end

quality93%

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.