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