doc-src/TutorialI/Advanced/document/WFrec.tex
changeset 10190 871772d38b30
parent 10189 865918597b63
child 10241 e0428c2778f1
equal deleted inserted replaced
10189:865918597b63 10190:871772d38b30
    37 \isa{wf\ r}\index{*wf|bold} means that relation \isa{r{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is
    37 \isa{wf\ r}\index{*wf|bold} means that relation \isa{r{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} is
    38 wellfounded.
    38 wellfounded.
    39 
    39 
    40 Each \isacommand{recdef} definition should be accompanied (after the
    40 Each \isacommand{recdef} definition should be accompanied (after the
    41 name of the function) by a wellfounded relation on the argument type
    41 name of the function) by a wellfounded relation on the argument type
    42 of the function. For example, \isa{measure} is defined by
    42 of the function. For example, \isaindexbold{measure} is defined by
    43 \begin{isabelle}%
    43 \begin{isabelle}%
    44 \ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}%
    44 \ \ \ \ \ measure\ f\ {\isasymequiv}\ {\isacharbraceleft}{\isacharparenleft}y{\isacharcomma}\ x{\isacharparenright}{\isachardot}\ f\ y\ {\isacharless}\ f\ x{\isacharbraceright}%
    45 \end{isabelle}
    45 \end{isabelle}
    46 and it has been proved that \isa{measure\ f} is always wellfounded.
    46 and it has been proved that \isa{measure\ f} is always wellfounded.
    47 
    47