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 plus :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
7 consts add :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
8 primrec |
8 primrec |
9 "plus m 0 = m" |
9 "add m 0 = m" |
10 "plus m (Suc n) = plus (Suc m) n" |
10 "add m (Suc n) = add (Suc m) n" |
11 |
11 |
12 text{*\noindent and prove*} |
12 text{*\noindent and prove*} |
13 (*<*) |
13 (*<*) |
14 lemma [simp]: "!m. plus m n = m+n" |
14 lemma [simp]: "!m. add m n = m+n" |
15 apply(induct_tac n) |
15 apply(induct_tac n) |
16 by(auto) |
16 by(auto) |
17 (*>*) |
17 (*>*) |
18 lemma "plus m n = m+n" |
18 lemma "add m n = m+n" |
19 (*<*) |
19 (*<*) |
20 by(simp) |
20 by(simp) |
21 |
21 |
22 end |
22 end |
23 (*>*) |
23 (*>*) |