1.1 --- a/doc-src/TutorialI/Inductive/document/AB.tex	Wed Dec 06 12:34:40 2000 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/document/AB.tex	Wed Dec 06 13:22:58 2000 +0100
     1.3 @@ -100,7 +100,7 @@
     1.4  \ \ \ \ \ {\isasymLongrightarrow}\ {\isasymexists}i{\isachardot}\ i\ {\isasymle}\ n\ {\isasymand}\ f\ i\ {\isacharequal}\ k%
     1.5  \end{isabelle}
     1.6  where \isa{f} is of type \isa{nat\ {\isasymRightarrow}\ int}, \isa{int} are the integers,
     1.7 -\isa{abs} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
     1.8 +\isa{{\isasymbar}{\isachardot}{\isasymbar}} is the absolute value function, and \isa{{\isacharhash}{\isadigit{1}}} is the
     1.9  integer 1 (see \S\ref{sec:numbers}).
    1.10  
    1.11  First we show that the our specific function, the difference between the
    1.12 @@ -111,15 +111,12 @@
    1.13  roles of \isa{a}'s and \isa{b}'s interchanged.%
    1.14  \end{isamarkuptext}%
    1.15  \isacommand{lemma}\ step{\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i\ {\isacharless}\ size\ w{\isachardot}\isanewline
    1.16 -\ \ abs{\isacharparenleft}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
    1.17 -\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
    1.18 -\ \ \ \ \ \ {\isacharminus}\isanewline
    1.19 -\ \ \ \ \ \ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ \ P\ x{\isacharbrackright}{\isacharparenright}\ {\isacharminus}\isanewline
    1.20 -\ \ \ \ \ \ \ int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
    1.21 +\ \ {\isasymbar}{\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ {\isacharparenleft}i{\isacharplus}{\isadigit{1}}{\isacharparenright}\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}\isanewline
    1.22 +\ \ \ {\isacharminus}\ {\isacharparenleft}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}{\isacharparenright}{\isacharminus}int{\isacharparenleft}size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharparenright}{\isacharparenright}{\isasymbar}\ {\isasymle}\ {\isacharhash}{\isadigit{1}}{\isachardoublequote}%
    1.23  \begin{isamarkuptxt}%
    1.24  \noindent
    1.25  The lemma is a bit hard to read because of the coercion function
    1.26 -\isa{{\isachardoublequote}int{\isacharcolon}{\isacharcolon}nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
    1.27 +\isa{{\isachardoublequote}int\ {\isacharcolon}{\isacharcolon}\ nat\ {\isasymRightarrow}\ int{\isachardoublequote}}. It is required because \isa{size} returns
    1.28  a natural number, but \isa{{\isacharminus}} on \isa{nat} will do the wrong thing.
    1.29  Function \isa{take} is predefined and \isa{take\ i\ xs} is the prefix of
    1.30  length \isa{i} of \isa{xs}; below we als need \isa{drop\ i\ xs}, which
    1.31 @@ -141,16 +138,14 @@
    1.32  \ \ {\isasymexists}i{\isasymle}size\ w{\isachardot}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ P\ x{\isacharbrackright}\ {\isacharequal}\ size{\isacharbrackleft}x{\isasymin}take\ i\ w{\isachardot}\ {\isasymnot}P\ x{\isacharbrackright}{\isacharplus}{\isadigit{1}}{\isachardoublequote}%
    1.33  \begin{isamarkuptxt}%
    1.34  \noindent
    1.35 -This is proved with the help of the intermediate value theorem, instantiated
    1.36 -appropriately and with its first premise disposed of by lemma
    1.37 -\isa{step{\isadigit{1}}}.%
    1.38 +This is proved by force with the help of the intermediate value theorem,
    1.39 +instantiated appropriately and with its first premise disposed of by lemma
    1.40 +\isa{step{\isadigit{1}}}:%
    1.41  \end{isamarkuptxt}%
    1.42  \isacommand{apply}{\isacharparenleft}insert\ nat{\isadigit{0}}{\isacharunderscore}intermed{\isacharunderscore}int{\isacharunderscore}val{\isacharbrackleft}OF\ step{\isadigit{1}}{\isacharcomma}\ of\ {\isachardoublequote}P{\isachardoublequote}\ {\isachardoublequote}w{\isachardoublequote}\ {\isachardoublequote}{\isacharhash}{\isadigit{1}}{\isachardoublequote}{\isacharbrackright}{\isacharparenright}\isanewline
    1.43 -\isacommand{apply}\ simp\isanewline
    1.44 -\isacommand{by}{\isacharparenleft}simp\ del{\isacharcolon}int{\isacharunderscore}Suc\ add{\isacharcolon}zdiff{\isacharunderscore}eq{\isacharunderscore}eq\ sym{\isacharbrackleft}OF\ int{\isacharunderscore}Suc{\isacharbrackright}{\isacharparenright}%
    1.45 +\isacommand{by}\ force%
    1.46  \begin{isamarkuptext}%
    1.47  \noindent
    1.48 -The additional lemmas are needed to mediate between \isa{nat} and \isa{int}.
    1.49  
    1.50  Lemma \isa{part{\isadigit{1}}} tells us only about the prefix \isa{take\ i\ w}.
    1.51  The suffix \isa{drop\ i\ w} is dealt with in the following easy lemma:%