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