13305
|
1 |
(*<*)
|
16417
|
2 |
theory Plus imports Main begin
|
13305
|
3 |
(*>*)
|
|
4 |
|
67406
|
5 |
text\<open>\noindent Define the following addition function\<close>
|
13305
|
6 |
|
27015
|
7 |
primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
|
|
8 |
"add m 0 = m" |
|
19249
|
9 |
"add m (Suc n) = add (Suc m) n"
|
13305
|
10 |
|
67406
|
11 |
text\<open>\noindent and prove\<close>
|
13305
|
12 |
(*<*)
|
67613
|
13 |
lemma [simp]: "\<forall>m. add m n = m+n"
|
13305
|
14 |
apply(induct_tac n)
|
|
15 |
by(auto)
|
|
16 |
(*>*)
|
19249
|
17 |
lemma "add m n = m+n"
|
13305
|
18 |
(*<*)
|
|
19 |
by(simp)
|
|
20 |
|
|
21 |
end
|
|
22 |
(*>*)
|