equal
deleted
inserted
replaced
10 |
10 |
11 text{*\noindent |
11 text{*\noindent |
12 and closed with the observation that the associated schema for the definition |
12 and closed with the observation that the associated schema for the definition |
13 of primitive recursive functions leads to overly verbose definitions. Moreover, |
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 |
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 |
15 you needed to declare essentially the same function as @{term"rev"} |
16 @{term"rev"}. We will now show you how \isacommand{recdef} can simplify |
16 and prove many standard properties of list reverse all over again. |
|
17 We will now show you how \isacommand{recdef} can simplify |
17 definitions and proofs about nested recursive datatypes. As an example we |
18 definitions and proofs about nested recursive datatypes. As an example we |
18 choose exercise~\ref{ex:trev-trev}: |
19 choose exercise~\ref{ex:trev-trev}: |
19 *} |
20 *} |
20 |
21 |
21 consts trev :: "('a,'b)term \<Rightarrow> ('a,'b)term" |
22 consts trev :: "('a,'b)term \<Rightarrow> ('a,'b)term" |