author | blanchet |
Mon, 15 Sep 2014 10:49:07 +0200 | |
changeset 58335 | a5a3b576fcfb |
parent 48985 | 5386df44a037 |
child 67406 | 23307fd33906 |
permissions | -rw-r--r-- |
(*<*) theory Plus imports Main begin (*>*) text{*\noindent Define the following addition function *} primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where "add m 0 = m" | "add m (Suc n) = add (Suc m) n" text{*\noindent and prove*} (*<*) lemma [simp]: "!m. add m n = m+n" apply(induct_tac n) by(auto) (*>*) lemma "add m n = m+n" (*<*) by(simp) end (*>*)