| changeset 48985 | 5386df44a037 |
| parent 48984 | f51d4a302962 |
| child 48986 | 037d32448e29 |
| 48984:f51d4a302962 | 48985:5386df44a037 |
|---|---|
1 (*<*) |
|
2 theory Plus imports Main begin |
|
3 (*>*) |
|
4 |
|
5 text{*\noindent Define the following addition function *} |
|
6 |
|
7 primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
|
8 "add m 0 = m" | |
|
9 "add m (Suc n) = add (Suc m) n" |
|
10 |
|
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) |
|
20 |
|
21 end |
|
22 (*>*) |