Quelle NatSum.thy Sprache: Isabelle

(*  Title:      ZF/ex/NatSum.thy
    Author:     Tobias Nipkow & Lawrence C Paulson

A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.

Note: n is a natural number but the sum is an integer,
                            and f maps integers to integers

Summing natural numbers, squares, cubes, etc.

Originally demonstrated permutative rewriting, but add_ac is no longer needed
  thanks to new simprocs.

Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
  http://www.research.att.com/\<not>njas/sequences/
*)

theory NatSum imports ZF begin

consts sum :: "[i\i, i] \ i"
primrec
  "sum (f,0) = #0"
  "sum (f, succ(n)) = f($#n) $+ sum(f,n)"

declare zadd_zmult_distrib [simp]  zadd_zmult_distrib2 [simp]
declare zdiff_zmult_distrib [simp] zdiff_zmult_distrib2 [simp]

(*The sum of the first n odd numbers equals n squared.*)
lemma sum_of_odds: "n \ nat \ sum (\i. i $+ i $+ #1, n) = $#n $* $#n"
by (induct_tac "n", auto)

(*The sum of the first n odd squares*)
lemma sum_of_odd_squares:
     "n \ nat \ #3 $* sum (\i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) =
      $#n $* (#4 $* $#n $* $#n $- #1)"
by (induct_tac "n", auto)

(*The sum of the first n odd cubes*)
lemma sum_of_odd_cubes:
     "n \ nat
      \<Longrightarrow> sum (\<lambda>i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) =
          $#n $* $#n $* (#2 $* $#n $* $#n $- #1)"
by (induct_tac "n", auto)

(*The sum of the first n positive integers equals n(n+1)/2.*)
lemma sum_of_naturals:
     "n \ nat \ #2 $* sum(\i. i, succ(n)) = $#n $* $#succ(n)"
by (induct_tac "n", auto)

lemma sum_of_squares:
     "n \ nat \ #6 $* sum (\i. i$*i, succ(n)) =
                  $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)"
by (induct_tac "n", auto)

lemma sum_of_cubes:
     "n \ nat \ #4 $* sum (\i. i$*i$*i, succ(n)) =
                  $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)"
by (induct_tac "n", auto)

(** Sum of fourth powers **)

lemma sum_of_fourth_powers:
     "n \ nat \ #30 $* sum (\i. i$*i$*i$*i, succ(n)) =
                    $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $*
                    (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)"
by (induct_tac "n", auto)

end

quality100%

¤ Dauer der Verarbeitung: 0.15 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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.