equal
deleted
inserted
replaced
11 proves a suitable induction rule $f$\isa{.induct} that follows the |
11 proves a suitable induction rule $f$\isa{.induct} that follows the |
12 recursion pattern of the particular function $f$. We call this |
12 recursion pattern of the particular function $f$. We call this |
13 \textbf{recursion induction}. Roughly speaking, it |
13 \textbf{recursion induction}. Roughly speaking, it |
14 requires you to prove for each \isacommand{recdef} equation that the property |
14 requires you to prove for each \isacommand{recdef} equation that the property |
15 you are trying to establish holds for the left-hand side provided it holds |
15 you are trying to establish holds for the left-hand side provided it holds |
16 for all recursive calls on the right-hand side. Here is a simple example:% |
16 for all recursive calls on the right-hand side. Here is a simple example% |
17 \end{isamarkuptext}% |
17 \end{isamarkuptext}% |
18 \isacommand{lemma}~{"}map~f~(sep(x,xs))~=~sep(f~x,~map~f~xs){"}% |
18 \isacommand{lemma}~{"}map~f~(sep(x,xs))~=~sep(f~x,~map~f~xs){"}% |
19 \begin{isamarkuptxt}% |
19 \begin{isamarkuptxt}% |
20 \noindent |
20 \noindent |
21 involving the predefined \isa{map} functional on lists: \isa{map f xs} |
21 involving the predefined \isa{map} functional on lists: \isa{map f xs} |