equal
deleted
inserted
replaced
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 |