summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

doc-src/TutorialI/Recdef/document/Induction.tex

changeset 10971 | 6852682eaf16 |

parent 10950 | aa788fcb75a5 |

child 11023 | 6e6c8d1ec89e |

1.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex Wed Jan 24 11:59:15 2001 +0100 1.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Wed Jan 24 12:29:10 2001 +0100 1.3 @@ -8,7 +8,7 @@ 1.4 equations) are simplification rules, we might like to prove something about 1.5 our function. Since the function is recursive, the natural proof principle is 1.6 again induction. But this time the structural form of induction that comes 1.7 -with datatypes is unlikely to work well---otherwise we could have defined the 1.8 +with datatypes is unlikely to work well --- otherwise we could have defined the 1.9 function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically 1.10 proves a suitable induction rule $f$\isa{{\isachardot}induct} that follows the 1.11 recursion pattern of the particular function $f$. We call this 1.12 @@ -53,7 +53,7 @@ 1.13 \end{quote}\index{*induct_tac}% 1.14 where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the 1.15 name of a function that takes an $n$-tuple. Usually the subgoal will 1.16 -contain the term $f~x@1~\dots~x@n$ but this need not be the case. The 1.17 +contain the term $f(x@1,\dots,x@n)$ but this need not be the case. The 1.18 induction rules do not mention $f$ at all. For example \isa{sep{\isachardot}induct} 1.19 \begin{isabelle} 1.20 {\isasymlbrakk}~{\isasymAnd}a.~P~a~[];\isanewline