doc-src/TutorialI/Misc/Plus.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Plus.thy	Fri Jul 05 17:48:05 2002 +0200
@@ -0,0 +1,23 @@
+(*<*)
+theory Plus = Main:
+(*>*)
+
+text{*\noindent Define the following addition function *}
+
+consts plus :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+primrec
+"plus m 0 = m"
+"plus m (Suc n) = plus (Suc m) n"
+
+text{*\noindent and prove*}
+(*<*)
+lemma [simp]: "!m. plus m n = m+n"
+apply(induct_tac n)
+by(auto)
+(*>*)
+lemma "plus m n = m+n"
+(*<*)
+by(simp)
+
+end
+(*>*)