new example ZF/ex/NatSum
authorpaulson
Fri Aug 18 12:31:20 2000 +0200 (2000-08-18)
changeset 9647e9623f47275b
parent 9646 aa3b82085e07
child 9648 35d761c7d934
new example ZF/ex/NatSum
NEWS
src/ZF/IsaMakefile
src/ZF/ex/NatSum.ML
src/ZF/ex/NatSum.thy
src/ZF/ex/ROOT.ML
     1.1 --- a/NEWS	Fri Aug 18 12:30:41 2000 +0200
     1.2 +++ b/NEWS	Fri Aug 18 12:31:20 2000 +0200
     1.3 @@ -303,6 +303,7 @@
     1.4  * the integer library now contains many of the usual laws for the orderings, 
     1.5  including $<=, and monotonicity laws for $+ and $*; 
     1.6  
     1.7 +* new example ZF/ex/NatSum to demonstrate integer arithmetic simplification;
     1.8  
     1.9  *** FOL & ZF ***
    1.10  
     2.1 --- a/src/ZF/IsaMakefile	Fri Aug 18 12:30:41 2000 +0200
     2.2 +++ b/src/ZF/IsaMakefile	Fri Aug 18 12:31:20 2000 +0200
     2.3 @@ -114,7 +114,7 @@
     2.4    ex/Enum.thy ex/LList.ML ex/LList.thy \
     2.5    ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \
     2.6    ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
     2.7 -  ex/Primrec_defs.ML ex/Primrec_defs.thy \
     2.8 +  ex/NatSum.ML ex/NatSum.thy  ex/Primrec_defs.ML ex/Primrec_defs.thy \
     2.9    ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \
    2.10    ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \
    2.11    ex/Term.ML ex/Term.thy ex/misc.ML
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/ex/NatSum.ML	Fri Aug 18 12:31:20 2000 +0200
     3.3 @@ -0,0 +1,64 @@
     3.4 +(*  Title:      HOL/ex/NatSum.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Tobias Nipkow & Lawrence C Paulson
     3.7 +
     3.8 +Summing natural numbers, squares, cubes, etc.
     3.9 +
    3.10 +Originally demonstrated permutative rewriting, but add_ac is no longer needed
    3.11 +  thanks to new simprocs.
    3.12 +
    3.13 +Thanks to Sloane's On-Line Encyclopedia of Integer Sequences,
    3.14 +  http://www.research.att.com/~njas/sequences/
    3.15 +*)
    3.16 +
    3.17 +Addsimps [zadd_zmult_distrib, zadd_zmult_distrib2];
    3.18 +Addsimps [zdiff_zmult_distrib, zdiff_zmult_distrib2];
    3.19 +
    3.20 +(*The sum of the first n odd numbers equals n squared.*)
    3.21 +Goal "n: nat ==> sum (%i. i $+ i $+ #1, n) = $#n $* $#n";
    3.22 +by (induct_tac "n" 1);
    3.23 +by Auto_tac;
    3.24 +qed "sum_of_odds";
    3.25 +
    3.26 +(*The sum of the first n odd squares*)
    3.27 +Goal "n: nat ==> #3 $* sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
    3.28 +\     $#n $* (#4 $* $#n $* $#n $- #1)";
    3.29 +by (induct_tac "n" 1);
    3.30 +by Auto_tac;  
    3.31 +qed "sum_of_odd_squares";
    3.32 +
    3.33 +(*The sum of the first n odd cubes*)
    3.34 +Goal "n: nat \
    3.35 +\     ==> sum (%i. (i $+ i $+ #1) $* (i $+ i $+ #1) $* (i $+ i $+ #1), n) = \
    3.36 +\         $#n $* $#n $* (#2 $* $#n $* $#n $- #1)";
    3.37 +by (induct_tac "n" 1);
    3.38 +by Auto_tac;  
    3.39 +qed "sum_of_odd_cubes";
    3.40 +
    3.41 +(*The sum of the first n positive integers equals n(n+1)/2.*)
    3.42 +Goal "n: nat ==> #2 $* sum(%i. i, succ(n)) = $#n $* $#succ(n)";
    3.43 +by (induct_tac "n" 1);
    3.44 +by Auto_tac;
    3.45 +qed "sum_of_naturals";
    3.46 +
    3.47 +Goal "n: nat ==> #6 $* sum (%i. i$*i, succ(n)) = \
    3.48 +\                $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1)";
    3.49 +by (induct_tac "n" 1);
    3.50 +by Auto_tac;
    3.51 +qed "sum_of_squares";
    3.52 +
    3.53 +Goal "n: nat ==> #4 $* sum (%i. i$*i$*i, succ(n)) = \
    3.54 +\                $#n $* $#n $* ($#n $+ #1) $* ($#n $+ #1)";
    3.55 +by (induct_tac "n" 1);
    3.56 +by Auto_tac;
    3.57 +qed "sum_of_cubes";
    3.58 +
    3.59 +(** Sum of fourth powers **)
    3.60 +
    3.61 +Goal "n: nat ==> \
    3.62 +\     #30 $* sum (%i. i$*i$*i$*i, succ(n)) = \
    3.63 +\     $#n $* ($#n $+ #1) $* (#2 $* $#n $+ #1) $* \
    3.64 +\     (#3 $* $#n $* $#n $+ #3 $* $#n $- #1)";
    3.65 +by (induct_tac "n" 1);
    3.66 +by Auto_tac;
    3.67 +qed "sum_of_fourth_powers";
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/ZF/ex/NatSum.thy	Fri Aug 18 12:31:20 2000 +0200
     4.3 @@ -0,0 +1,18 @@
     4.4 +(*  Title:      HOL/ex/Natsum.thy
     4.5 +    ID:         $Id$
     4.6 +    Author:     Tobias Nipkow & Lawrence C Paulson
     4.7 +
     4.8 +A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
     4.9 +
    4.10 +Note: n is a natural number but the sum is an integer,
    4.11 +                            and f maps integers to integers
    4.12 +*)
    4.13 +
    4.14 +NatSum = Main +
    4.15 +
    4.16 +consts sum     :: [i=>i, i] => i
    4.17 +primrec 
    4.18 +  "sum (f,0) = #0"
    4.19 +  "sum (f, succ(n)) = f($#n) $+ sum(f,n)"
    4.20 +
    4.21 +end
    4.22 \ No newline at end of file
     5.1 --- a/src/ZF/ex/ROOT.ML	Fri Aug 18 12:30:41 2000 +0200
     5.2 +++ b/src/ZF/ex/ROOT.ML	Fri Aug 18 12:31:20 2000 +0200
     5.3 @@ -8,6 +8,7 @@
     5.4  
     5.5  time_use     "misc.ML";
     5.6  time_use_thy "Primes";          (*GCD theory*)
     5.7 +time_use_thy "NatSum";          (*Summing integers, squares, cubes, etc.*)
     5.8  time_use_thy "Ramsey";          (*Simple form of Ramsey's theorem*)
     5.9  time_use_thy "Limit";           (*Inverse limit construction of domains*)
    5.10  time_use     "BinEx";		(*Binary integer arithmetic*)