| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 15:03:34 +0200 | |
| branch | isac-from-Isabelle2009-2 |
| changeset 37913 | 20e3616b2d9c |
| parent 27015 | f8537d69f514 |
| permissions | -rw-r--r-- |
1 (*<*)
2 theory Plus imports Main begin
3 (*>*)
5 text{*\noindent Define the following addition function *}
7 primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
8 "add m 0 = m" |
9 "add m (Suc n) = add (Suc m) n"
11 text{*\noindent and prove*}
12 (*<*)
13 lemma [simp]: "!m. add m n = m+n"
14 apply(induct_tac n)
15 by(auto)
16 (*>*)
17 lemma "add m n = m+n"
18 (*<*)
19 by(simp)
21 end
22 (*>*)