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