author | nipkow |

Mon Nov 27 10:38:43 2000 +0100 (2000-11-27) | |

changeset 10522 | ed3964d1f1a4 |

parent 10521 | 06206298e4d0 |

child 10523 | 68105cf615fa |

*** empty log message ***

1.1 --- a/doc-src/TutorialI/Advanced/WFrec.thy Sun Nov 26 11:37:49 2000 +0100 1.2 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Mon Nov 27 10:38:43 2000 +0100 1.3 @@ -51,7 +51,7 @@ 1.4 1.5 text{* 1.6 Lexicographic products of measure functions already go a long 1.7 -way. Furthermore you may embedding some type in an 1.8 +way. Furthermore you may embed some type in an 1.9 existing well-founded relation via the inverse image construction @{term 1.10 inv_image}. All these constructions are known to \isacommand{recdef}. Thus you 1.11 will never have to prove well-foundedness of any relation composed

2.1 --- a/doc-src/TutorialI/Advanced/advanced.tex Sun Nov 26 11:37:49 2000 +0100 2.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex Mon Nov 27 10:38:43 2000 +0100 2.3 @@ -35,7 +35,7 @@ 2.4 \index{*recdef|)} 2.5 2.6 \subsection{Beyond measure} 2.7 -\label{sec:wellfounded} 2.8 +\label{sec:beyond-measure} 2.9 \input{Advanced/document/WFrec.tex} 2.10 2.11 \section{Advanced induction techniques}

3.1 --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Sun Nov 26 11:37:49 2000 +0100 3.2 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Mon Nov 27 10:38:43 2000 +0100 3.3 @@ -51,7 +51,7 @@ 3.4 {\isachardoublequote}contrived{\isacharparenleft}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharcomma}{\isadigit{0}}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}% 3.5 \begin{isamarkuptext}% 3.6 Lexicographic products of measure functions already go a long 3.7 -way. Furthermore you may embedding some type in an 3.8 +way. Furthermore you may embed some type in an 3.9 existing well-founded relation via the inverse image construction \isa{inv{\isacharunderscore}image}. All these constructions are known to \isacommand{recdef}. Thus you 3.10 will never have to prove well-foundedness of any relation composed 3.11 solely of these building blocks. But of course the proof of

4.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex Sun Nov 26 11:37:49 2000 +0100 4.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Mon Nov 27 10:38:43 2000 +0100 4.3 @@ -13,7 +13,7 @@ 4.4 the same function. What is more, those equations are automatically declared as 4.5 simplification rules. 4.6 4.7 -In general, Isabelle may not be able to prove all termination condition 4.8 +In general, Isabelle may not be able to prove all termination conditions 4.9 (there is one for each recursive call) automatically. For example, 4.10 termination of the following artificial function% 4.11 \end{isamarkuptext}%

5.1 --- a/doc-src/TutorialI/Recdef/termination.thy Sun Nov 26 11:37:49 2000 +0100 5.2 +++ b/doc-src/TutorialI/Recdef/termination.thy Mon Nov 27 10:38:43 2000 +0100 5.3 @@ -13,7 +13,7 @@ 5.4 the same function. What is more, those equations are automatically declared as 5.5 simplification rules. 5.6 5.7 -In general, Isabelle may not be able to prove all termination condition 5.8 +In general, Isabelle may not be able to prove all termination conditions 5.9 (there is one for each recursive call) automatically. For example, 5.10 termination of the following artificial function 5.11 *}

6.1 --- a/doc-src/TutorialI/fp.tex Sun Nov 26 11:37:49 2000 +0100 6.2 +++ b/doc-src/TutorialI/fp.tex Mon Nov 27 10:38:43 2000 +0100 6.3 @@ -549,7 +549,8 @@ 6.4 defined by means of \isacommand{recdef}: you can use full pattern-matching, 6.5 recursion need not involve datatypes, and termination is proved by showing 6.6 that the arguments of all recursive calls are smaller in a suitable (user 6.7 -supplied) sense. 6.8 +supplied) sense. In this section we ristrict ourselves to measure functions; 6.9 +more advanced termination proofs are discussed in \S\ref{sec:beyond-measure}. 6.10 6.11 \subsection{Defining recursive functions} 6.12

7.1 --- a/doc-src/TutorialI/tutorial.tex Sun Nov 26 11:37:49 2000 +0100 7.2 +++ b/doc-src/TutorialI/tutorial.tex Mon Nov 27 10:38:43 2000 +0100 7.3 @@ -1,6 +1,6 @@ 7.4 \documentclass{article} 7.5 \newif\ifremarks 7.6 -\remarksfalse %TRUE causes remarks to be displayed (as marginal notes) 7.7 +\remarkstrue %TRUE causes remarks to be displayed (as marginal notes) 7.8 \usepackage{cl2emono-modified,isabelle,isabellesym} 7.9 \usepackage{latexsym,verbatim,graphicx,../iman,../extra,../ttbox,comment} 7.10 \usepackage{proof,amsmath}