1.1 --- a/doc-src/TutorialI/Misc/Itrev.thy	Wed Aug 30 18:05:20 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Aug 30 18:09:20 2000 +0200
     1.3 @@ -2,25 +2,29 @@
     1.4  theory Itrev = Main:;
     1.5  (*>*)
     1.6  
     1.7 -text{* Function \isa{rev} has quadratic worst-case running time
     1.8 -because it calls function \isa{\at} for each element of the list and
     1.9 -\isa{\at} is linear in its first argument.  A linear time version of
    1.10 -\isa{rev} reqires an extra argument where the result is accumulated
    1.11 -gradually, using only \isa{\#}:*}
    1.12 +text{*
    1.13 +Function @{term"rev"} has quadratic worst-case running time
    1.14 +because it calls function @{term"@"} for each element of the list and
    1.15 +@{term"@"} is linear in its first argument.  A linear time version of
    1.16 +@{term"rev"} reqires an extra argument where the result is accumulated
    1.17 +gradually, using only @{name"#"}:
    1.18 +*}
    1.19  
    1.20  consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
    1.21  primrec
    1.22  "itrev []     ys = ys"
    1.23  "itrev (x#xs) ys = itrev xs (x#ys)";
    1.24  
    1.25 -text{*\noindent The behaviour of \isa{itrev} is simple: it reverses
    1.26 +text{*\noindent
    1.27 +The behaviour of @{term"itrev"} is simple: it reverses
    1.28  its first argument by stacking its elements onto the second argument,
    1.29  and returning that second argument when the first one becomes
    1.30 -empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
    1.31 +empty. Note that @{term"itrev"} is tail-recursive, i.e.\ it can be
    1.32  compiled into a loop.
    1.33  
    1.34 -Naturally, we would like to show that \isa{itrev} does indeed reverse
    1.35 -its first argument provided the second one is empty: *};
    1.36 +Naturally, we would like to show that @{term"itrev"} does indeed reverse
    1.37 +its first argument provided the second one is empty:
    1.38 +*};
    1.39  
    1.40  lemma "itrev xs [] = rev xs";
    1.41  
    1.42 @@ -37,47 +41,46 @@
    1.43  \end{isabelle}
    1.44  Just as predicted above, the overall goal, and hence the induction
    1.45  hypothesis, is too weak to solve the induction step because of the fixed
    1.46 -\isa{[]}. The corresponding heuristic:
    1.47 +@{term"[]"}. The corresponding heuristic:
    1.48  \begin{quote}
    1.49 -{\em 3. Generalize goals for induction by replacing constants by variables.}
    1.50 +\emph{Generalize goals for induction by replacing constants by variables.}
    1.51  \end{quote}
    1.52 -
    1.53 -Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
    1.54 +Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
    1.55  just not true---the correct generalization is
    1.56  *};
    1.57  (*<*)oops;(*>*)
    1.58  lemma "itrev xs ys = rev xs @ ys";
    1.59  
    1.60  txt{*\noindent
    1.61 -If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
    1.62 +If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
    1.63  @{term"rev xs"}, just as required.
    1.64  
    1.65  In this particular instance it was easy to guess the right generalization,
    1.66  but in more complex situations a good deal of creativity is needed. This is
    1.67  the main source of complications in inductive proofs.
    1.68  
    1.69 -Although we now have two variables, only \isa{xs} is suitable for
    1.70 +Although we now have two variables, only @{term"xs"} is suitable for
    1.71  induction, and we repeat our above proof attempt. Unfortunately, we are still
    1.72  not there:
    1.73  \begin{isabelle}
    1.74  ~1.~{\isasymAnd}a~list.\isanewline
    1.75  ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
    1.76 -~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
    1.77 +~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
    1.78  \end{isabelle}
    1.79  The induction hypothesis is still too weak, but this time it takes no
    1.80 -intuition to generalize: the problem is that \isa{ys} is fixed throughout
    1.81 +intuition to generalize: the problem is that @{term"ys"} is fixed throughout
    1.82  the subgoal, but the induction hypothesis needs to be applied with
    1.83 -@{term"a # ys"} instead of \isa{ys}. Hence we prove the theorem
    1.84 -for all \isa{ys} instead of a fixed one:
    1.85 +@{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
    1.86 +for all @{term"ys"} instead of a fixed one:
    1.87  *};
    1.88  (*<*)oops;(*>*)
    1.89  lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
    1.90  
    1.91  txt{*\noindent
    1.92 -This time induction on \isa{xs} followed by simplification succeeds. This
    1.93 +This time induction on @{term"xs"} followed by simplification succeeds. This
    1.94  leads to another heuristic for generalization:
    1.95  \begin{quote}
    1.96 -{\em 4. Generalize goals for induction by universally quantifying all free
    1.97 +\emph{Generalize goals for induction by universally quantifying all free
    1.98  variables {\em(except the induction variable itself!)}.}
    1.99  \end{quote}
   1.100  This prevents trivial failures like the above and does not change the