1.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Fri Sep 01 18:29:52 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Fri Sep 01 19:09:44 2000 +0200
     1.3 @@ -6,10 +6,10 @@
     1.4  its termination with the help of the user-supplied measure.  All of the above
     1.5  examples are simple enough that Isabelle can prove automatically that the
     1.6  measure of the argument goes down in each recursive call. As a result,
     1.7 -\isa{$f$.simps} will contain the defining equations (or variants derived from
     1.8 -them) as theorems. For example, look (via \isacommand{thm}) at
     1.9 -\isa{sep.simps} and \isa{sep1.simps} to see that they define the same
    1.10 -function. What is more, those equations are automatically declared as
    1.11 +$f$\isa{{\isachardot}simps} will contain the defining equations (or variants derived
    1.12 +from them) as theorems. For example, look (via \isacommand{thm}) at
    1.13 +\isa{sep{\isachardot}simps} and \isa{sep\isadigit{1}{\isachardot}simps} to see that they define
    1.14 +the same function. What is more, those equations are automatically declared as
    1.15  simplification rules.
    1.16  
    1.17  In general, Isabelle may not be able to prove all termination condition
    1.18 @@ -29,7 +29,7 @@
    1.19  \isacommand{lemma}\ termi{\isacharunderscore}lem{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ {\isacharminus}\ Suc\ y\ {\isacharless}\ x\ {\isacharminus}\ y{\isachardoublequote}%
    1.20  \begin{isamarkuptxt}%
    1.21  \noindent
    1.22 -It was not proved automatically because of the special nature of \isa{-}
    1.23 +It was not proved automatically because of the special nature of \isa{{\isacharminus}}
    1.24  on \isa{nat}. This requires more arithmetic than is tried by default:%
    1.25  \end{isamarkuptxt}%
    1.26  \isacommand{by}{\isacharparenleft}arith{\isacharparenright}%
    1.27 @@ -44,8 +44,8 @@
    1.28  \ \ {\isachardoublequote}g{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ g{\isacharparenleft}x{\isacharcomma}y{\isacharplus}\isadigit{1}{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
    1.29  \begin{isamarkuptext}%
    1.30  \noindent
    1.31 -This time everything works fine. Now \isa{g.simps} contains precisely the
    1.32 -stated recursion equation for \isa{g} and they are simplification
    1.33 +This time everything works fine. Now \isa{g{\isachardot}simps} contains precisely
    1.34 +the stated recursion equation for \isa{g} and they are simplification
    1.35  rules. Thus we can automatically prove%
    1.36  \end{isamarkuptext}%
    1.37  \isacommand{theorem}\ wow{\isacharcolon}\ {\isachardoublequote}g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{0}{\isacharparenright}\ {\isacharequal}\ g{\isacharparenleft}\isadigit{1}{\isacharcomma}\isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
    1.38 @@ -54,7 +54,7 @@
    1.39  \noindent
    1.40  More exciting theorems require induction, which is discussed below.
    1.41  
    1.42 -Because lemma \isa{termi_lem} above was only turned into a
    1.43 +Because lemma \isa{termi{\isacharunderscore}lem} above was only turned into a
    1.44  simplification rule for the sake of the termination proof, we may want to
    1.45  disable it again:%
    1.46  \end{isamarkuptext}%
    1.47 @@ -63,22 +63,23 @@
    1.48  The attentive reader may wonder why we chose to call our function \isa{g}
    1.49  rather than \isa{f} the second time around. The reason is that, despite
    1.50  the failed termination proof, the definition of \isa{f} did not
    1.51 -fail (and thus we could not define it a second time). However, all theorems
    1.52 -about \isa{f}, for example \isa{f.simps}, carry as a precondition the
    1.53 -unproved termination condition. Moreover, the theorems \isa{f.simps} are
    1.54 -not simplification rules. However, this mechanism allows a delayed proof of
    1.55 -termination: instead of proving \isa{termi_lem} up front, we could prove
    1.56 +fail, and thus we could not define it a second time. However, all theorems
    1.57 +about \isa{f}, for example \isa{f{\isachardot}simps}, carry as a precondition
    1.58 +the unproved termination condition. Moreover, the theorems
    1.59 +\isa{f{\isachardot}simps} are not simplification rules. However, this mechanism
    1.60 +allows a delayed proof of termination: instead of proving
    1.61 +\isa{termi{\isacharunderscore}lem} up front, we could prove 
    1.62  it later on and then use it to remove the preconditions from the theorems
    1.63  about \isa{f}. In most cases this is more cumbersome than proving things
    1.64 -up front
    1.65 +up front.
    1.66  %FIXME, with one exception: nested recursion.
    1.67  
    1.68  Although all the above examples employ measure functions, \isacommand{recdef}
    1.69  allows arbitrary wellfounded relations. For example, termination of
    1.70 -Ackermann's function requires the lexicographic product \isa{<*lex*>}:%
    1.71 +Ackermann's function requires the lexicographic product \isa{{\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}}:%
    1.72  \end{isamarkuptext}%
    1.73  \isacommand{consts}\ ack\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isacharasterisk}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
    1.74 -\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isacharpercent}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
    1.75 +\isacommand{recdef}\ ack\ {\isachardoublequote}measure{\isacharparenleft}{\isasymlambda}m{\isachardot}\ m{\isacharparenright}\ {\isacharless}{\isacharasterisk}lex{\isacharasterisk}{\isachargreater}\ measure{\isacharparenleft}{\isasymlambda}n{\isachardot}\ n{\isacharparenright}{\isachardoublequote}\isanewline
    1.76  \ \ {\isachardoublequote}ack{\isacharparenleft}\isadigit{0}{\isacharcomma}n{\isacharparenright}\ \ \ \ \ \ \ \ \ {\isacharequal}\ Suc\ n{\isachardoublequote}\isanewline
    1.77  \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}\isadigit{0}{\isacharparenright}\ \ \ \ \ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}\ \isadigit{1}{\isacharparenright}{\isachardoublequote}\isanewline
    1.78  \ \ {\isachardoublequote}ack{\isacharparenleft}Suc\ m{\isacharcomma}Suc\ n{\isacharparenright}\ {\isacharequal}\ ack{\isacharparenleft}m{\isacharcomma}ack{\isacharparenleft}Suc\ m{\isacharcomma}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%