equal
deleted
inserted
replaced
2 theory Plus imports Main begin |
2 theory Plus imports Main begin |
3 (*>*) |
3 (*>*) |
4 |
4 |
5 text{*\noindent Define the following addition function *} |
5 text{*\noindent Define the following addition function *} |
6 |
6 |
7 consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
7 primrec add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where |
8 primrec |
8 "add m 0 = m" | |
9 "add m 0 = m" |
|
10 "add m (Suc n) = add (Suc m) n" |
9 "add m (Suc n) = add (Suc m) n" |
11 |
10 |
12 text{*\noindent and prove*} |
11 text{*\noindent and prove*} |
13 (*<*) |
12 (*<*) |
14 lemma [simp]: "!m. add m n = m+n" |
13 lemma [simp]: "!m. add m n = m+n" |