doc-src/TutorialI/Misc/Itrev.thy

--- a/doc-src/TutorialI/Misc/Itrev.thy	Wed Aug 30 18:05:20 2000 +0200
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Aug 30 18:09:20 2000 +0200
@@ -2,25 +2,29 @@
 theory Itrev = Main:;
 (*>*)
 
-text{* Function \isa{rev} has quadratic worst-case running time
-because it calls function \isa{\at} for each element of the list and
-\isa{\at} is linear in its first argument.  A linear time version of
-\isa{rev} reqires an extra argument where the result is accumulated
-gradually, using only \isa{\#}:*}
+text{*
+Function @{term"rev"} has quadratic worst-case running time
+because it calls function @{term"@"} for each element of the list and
+@{term"@"} is linear in its first argument.  A linear time version of
+@{term"rev"} reqires an extra argument where the result is accumulated
+gradually, using only @{name"#"}:
+*}
 
 consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
 primrec
 "itrev []     ys = ys"
 "itrev (x#xs) ys = itrev xs (x#ys)";
 
-text{*\noindent The behaviour of \isa{itrev} is simple: it reverses
+text{*\noindent
+The behaviour of @{term"itrev"} is simple: it reverses
 its first argument by stacking its elements onto the second argument,
 and returning that second argument when the first one becomes
-empty. Note that \isa{itrev} is tail-recursive, i.e.\ it can be
+empty. Note that @{term"itrev"} is tail-recursive, i.e.\ it can be
 compiled into a loop.
 
-Naturally, we would like to show that \isa{itrev} does indeed reverse
-its first argument provided the second one is empty: *};
+Naturally, we would like to show that @{term"itrev"} does indeed reverse
+its first argument provided the second one is empty:
+*};
 
 lemma "itrev xs [] = rev xs";
 
@@ -37,47 +41,46 @@
 \end{isabelle}
 Just as predicted above, the overall goal, and hence the induction
 hypothesis, is too weak to solve the induction step because of the fixed
-\isa{[]}. The corresponding heuristic:
+@{term"[]"}. The corresponding heuristic:
 \begin{quote}
-{\em 3. Generalize goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
 \end{quote}
-
-Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
+Of course one cannot do this na\"{\i}vely: @{term"itrev xs ys = rev xs"} is
 just not true---the correct generalization is
 *};
 (*<*)oops;(*>*)
 lemma "itrev xs ys = rev xs @ ys";
 
 txt{*\noindent
-If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
+If @{term"ys"} is replaced by @{term"[]"}, the right-hand side simplifies to
 @{term"rev xs"}, just as required.
 
 In this particular instance it was easy to guess the right generalization,
 but in more complex situations a good deal of creativity is needed. This is
 the main source of complications in inductive proofs.
 
-Although we now have two variables, only \isa{xs} is suitable for
+Although we now have two variables, only @{term"xs"} is suitable for
 induction, and we repeat our above proof attempt. Unfortunately, we are still
 not there:
 \begin{isabelle}
 ~1.~{\isasymAnd}a~list.\isanewline
 ~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
-~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
+~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys
 \end{isabelle}
 The induction hypothesis is still too weak, but this time it takes no
-intuition to generalize: the problem is that \isa{ys} is fixed throughout
+intuition to generalize: the problem is that @{term"ys"} is fixed throughout
 the subgoal, but the induction hypothesis needs to be applied with
-@{term"a # ys"} instead of \isa{ys}. Hence we prove the theorem
-for all \isa{ys} instead of a fixed one:
+@{term"a # ys"} instead of @{term"ys"}. Hence we prove the theorem
+for all @{term"ys"} instead of a fixed one:
 *};
 (*<*)oops;(*>*)
 lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
 
 txt{*\noindent
-This time induction on \isa{xs} followed by simplification succeeds. This
+This time induction on @{term"xs"} followed by simplification succeeds. This
 leads to another heuristic for generalization:
 \begin{quote}
-{\em 4. Generalize goals for induction by universally quantifying all free
+\emph{Generalize goals for induction by universally quantifying all free
 variables {\em(except the induction variable itself!)}.}
 \end{quote}
 This prevents trivial failures like the above and does not change the