summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 27 Nov 2000 10:38:43 +0100 | |

changeset 10522 | ed3964d1f1a4 |

parent 10521 | 06206298e4d0 |

child 10523 | 68105cf615fa |

*** empty log message ***

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

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

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

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

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

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

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