doc-src/TutorialI/Misc/natsum.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,28 @@
+(*<*)
+theory natsum = Main:;
+(*>*)
+text{*\noindent
+In particular, there are \isa{case}-expressions, for example
+*}
+
+(*<*)term(*>*) "case n of 0 \\<Rightarrow> 0 | Suc m \\<Rightarrow> m";
+
+text{*\noindent
+primitive recursion, for example
+*}
+
+consts sum :: "nat \\<Rightarrow> nat";
+primrec "sum 0 = 0"
+        "sum (Suc n) = Suc n + sum n";
+
+text{*\noindent
+and induction, for example
+*}
+
+lemma "sum n + sum n = n*(Suc n)";
+apply(induct_tac n);
+apply(auto).;
+
+(*<*)
+end
+(*>*)