|
9645
|
1 |
(*<*)
|
|
|
2 |
theory Nested0 = Main:
|
|
|
3 |
(*>*)
|
|
|
4 |
|
|
|
5 |
text{*
|
|
|
6 |
In \S\ref{sec:nested-datatype} we defined the datatype of terms
|
|
|
7 |
*}
|
|
|
8 |
|
|
|
9 |
datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list"
|
|
|
10 |
|
|
|
11 |
text{*\noindent
|
|
|
12 |
and closed with the observation that the associated schema for the definition
|
|
|
13 |
of primitive recursive functions leads to overly verbose definitions. Moreover,
|
|
|
14 |
if you have worked exercise~\ref{ex:trev-trev} you will have noticed that
|
|
|
15 |
you needed to reprove many lemmas reminiscent of similar lemmas about
|
|
|
16 |
@{term"rev"}. We will now show you how \isacommand{recdef} can simplify
|
|
|
17 |
definitions and proofs about nested recursive datatypes. As an example we
|
|
|
18 |
chose exercise~\ref{ex:trev-trev}:
|
|
|
19 |
|
|
|
20 |
FIXME: declare trev now!
|
|
|
21 |
*}
|
|
|
22 |
(* consts trev :: "('a,'b)term => ('a,'b)term" *)
|
|
|
23 |
(*<*)
|
|
|
24 |
end
|
|
|
25 |
(*>*)
|