|
8745
|
1 |
(*<*)
|
|
|
2 |
theory natsum = Main:;
|
|
|
3 |
(*>*)
|
|
|
4 |
text{*\noindent
|
|
9792
|
5 |
In particular, there are @{text"case"}-expressions, for example
|
|
9541
|
6 |
@{term[display]"case n of 0 => 0 | Suc m => m"}
|
|
8745
|
7 |
primitive recursion, for example
|
|
|
8 |
*}
|
|
|
9 |
|
|
|
10 |
consts sum :: "nat \\<Rightarrow> nat";
|
|
|
11 |
primrec "sum 0 = 0"
|
|
|
12 |
"sum (Suc n) = Suc n + sum n";
|
|
|
13 |
|
|
|
14 |
text{*\noindent
|
|
|
15 |
and induction, for example
|
|
|
16 |
*}
|
|
|
17 |
|
|
|
18 |
lemma "sum n + sum n = n*(Suc n)";
|
|
|
19 |
apply(induct_tac n);
|
|
9458
|
20 |
by(auto);
|
|
8745
|
21 |
|
|
|
22 |
(*<*)
|
|
|
23 |
end
|
|
|
24 |
(*>*)
|