equal
deleted
inserted
replaced
9 \begin{isamarkuptext}% |
9 \begin{isamarkuptext}% |
10 \noindent |
10 \noindent |
11 and closed with the observation that the associated schema for the definition |
11 and closed with the observation that the associated schema for the definition |
12 of primitive recursive functions leads to overly verbose definitions. Moreover, |
12 of primitive recursive functions leads to overly verbose definitions. Moreover, |
13 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that |
13 if you have worked exercise~\ref{ex:trev-trev} you will have noticed that |
14 you needed to reprove many lemmas reminiscent of similar lemmas about |
14 you needed to declare essentially the same function as \isa{rev} |
15 \isa{rev}. We will now show you how \isacommand{recdef} can simplify |
15 and prove many standard properties of list reverse all over again. |
|
16 We will now show you how \isacommand{recdef} can simplify |
16 definitions and proofs about nested recursive datatypes. As an example we |
17 definitions and proofs about nested recursive datatypes. As an example we |
17 choose exercise~\ref{ex:trev-trev}:% |
18 choose exercise~\ref{ex:trev-trev}:% |
18 \end{isamarkuptext}% |
19 \end{isamarkuptext}% |
19 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\end{isabellebody}% |
20 \isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}\end{isabellebody}% |
20 %%% Local Variables: |
21 %%% Local Variables: |