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