author paulson Wed, 21 May 1997 10:55:21 +0200 changeset 3269 eca2a3634acd parent 3268 012c43174664 child 3270 4a3ab8d43451
Function "sum" now defined using primrec
 src/HOL/ex/NatSum.ML file | annotate | diff | comparison | revisions src/HOL/ex/NatSum.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/ex/NatSum.ML	Wed May 21 10:54:10 1997 +0200
+++ b/src/HOL/ex/NatSum.ML	Wed May 21 10:55:21 1997 +0200
@@ -3,11 +3,12 @@
Author:     Tobias Nipkow
Copyright   1994 TU Muenchen

-Summing natural numbers, squares and cubes. Could be continued...
+Summing natural numbers, squares and cubes.  Could be continued...
+Demonstrates permutative rewriting.
*)

-Addsimps ([NatSum.sum_0,NatSum.sum_Suc] @ add_ac);
-Addsimps [add_mult_distrib,add_mult_distrib2];
+Addsimps add_ac;
+Addsimps [add_mult_distrib, add_mult_distrib2];

(*The sum of the first n positive integers equals n(n+1)/2.*)
goal NatSum.thy "2*sum (%i.i) (Suc n) = n*Suc(n)";```
```--- a/src/HOL/ex/NatSum.thy	Wed May 21 10:54:10 1997 +0200
+++ b/src/HOL/ex/NatSum.thy	Wed May 21 10:55:21 1997 +0200
@@ -8,6 +8,8 @@

NatSum = Arith +
consts sum     :: [nat=>nat, nat] => nat
-rules  sum_0      "sum f 0 = 0"
-       sum_Suc    "sum f (Suc n) = f(n) + sum f n"
+primrec "sum" nat
+  "sum f 0 = 0"
+  "sum f (Suc n) = f(n) + sum f n"
+
end```