*** empty log message ***
authornipkow
Mon Nov 27 10:38:43 2000 +0100 (2000-11-27)
changeset 10522ed3964d1f1a4
parent 10521 06206298e4d0
child 10523 68105cf615fa
*** empty log message ***
doc-src/TutorialI/Advanced/WFrec.thy
doc-src/TutorialI/Advanced/advanced.tex
doc-src/TutorialI/Advanced/document/WFrec.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/fp.tex
doc-src/TutorialI/tutorial.tex
     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}