doc-src/TutorialI/Recdef/termination.thy

--- a/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 01 18:29:52 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy	Fri Sep 01 19:09:44 2000 +0200
@@ -1,5 +1,5 @@
 (*<*)
-theory termination = Main:;
+theory termination = examples:
 (*>*)
 
 text{*
@@ -7,10 +7,10 @@
 its termination with the help of the user-supplied measure.  All of the above
 examples are simple enough that Isabelle can prove automatically that the
 measure of the argument goes down in each recursive call. As a result,
-\isa{$f$.simps} will contain the defining equations (or variants derived from
-them) as theorems. For example, look (via \isacommand{thm}) at
-\isa{sep.simps} and \isa{sep1.simps} to see that they define the same
-function. What is more, those equations are automatically declared as
+$f$@{text".simps"} will contain the defining equations (or variants derived
+from them) as theorems. For example, look (via \isacommand{thm}) at
+@{thm[source]sep.simps} and @{thm[source]sep1.simps} to see that they define
+the same function. What is more, those equations are automatically declared as
 simplification rules.
 
 In general, Isabelle may not be able to prove all termination condition
@@ -32,8 +32,8 @@
 lemma termi_lem[simp]: "\\<not> x \\<le> y \\<Longrightarrow> x - Suc y < x - y";
 
 txt{*\noindent
-It was not proved automatically because of the special nature of \isa{-}
-on \isa{nat}. This requires more arithmetic than is tried by default:
+It was not proved automatically because of the special nature of @{text"-"}
+on @{typ"nat"}. This requires more arithmetic than is tried by default:
 *}
 
 by(arith);
@@ -49,8 +49,8 @@
   "g(x,y) = (if x \\<le> y then x else g(x,y+1))";
 
 text{*\noindent
-This time everything works fine. Now \isa{g.simps} contains precisely the
-stated recursion equation for \isa{g} and they are simplification
+This time everything works fine. Now @{thm[source]g.simps} contains precisely
+the stated recursion equation for @{term"g"} and they are simplification
 rules. Thus we can automatically prove
 *}
 
@@ -60,7 +60,7 @@
 text{*\noindent
 More exciting theorems require induction, which is discussed below.
 
-Because lemma \isa{termi_lem} above was only turned into a
+Because lemma @{thm[source]termi_lem} above was only turned into a
 simplification rule for the sake of the termination proof, we may want to
 disable it again:
 *}
@@ -68,26 +68,27 @@
 lemmas [simp del] = termi_lem;
 
 text{*
-The attentive reader may wonder why we chose to call our function \isa{g}
-rather than \isa{f} the second time around. The reason is that, despite
-the failed termination proof, the definition of \isa{f} did not
-fail (and thus we could not define it a second time). However, all theorems
-about \isa{f}, for example \isa{f.simps}, carry as a precondition the
-unproved termination condition. Moreover, the theorems \isa{f.simps} are
-not simplification rules. However, this mechanism allows a delayed proof of
-termination: instead of proving \isa{termi_lem} up front, we could prove
+The attentive reader may wonder why we chose to call our function @{term"g"}
+rather than @{term"f"} the second time around. The reason is that, despite
+the failed termination proof, the definition of @{term"f"} did not
+fail, and thus we could not define it a second time. However, all theorems
+about @{term"f"}, for example @{thm[source]f.simps}, carry as a precondition
+the unproved termination condition. Moreover, the theorems
+@{thm[source]f.simps} are not simplification rules. However, this mechanism
+allows a delayed proof of termination: instead of proving
+@{thm[source]termi_lem} up front, we could prove 
 it later on and then use it to remove the preconditions from the theorems
-about \isa{f}. In most cases this is more cumbersome than proving things
-up front
+about @{term"f"}. In most cases this is more cumbersome than proving things
+up front.
 %FIXME, with one exception: nested recursion.
 
 Although all the above examples employ measure functions, \isacommand{recdef}
 allows arbitrary wellfounded relations. For example, termination of
-Ackermann's function requires the lexicographic product \isa{<*lex*>}:
+Ackermann's function requires the lexicographic product @{text"<*lex*>"}:
 *}
 
 consts ack :: "nat*nat \\<Rightarrow> nat";
-recdef ack "measure(%m. m) <*lex*> measure(%n. n)"
+recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
   "ack(0,n)         = Suc n"
   "ack(Suc m,0)     = ack(m, 1)"
   "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";