--- a/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 18:55:37 2001 +0200
+++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri Sep 28 19:17:01 2001 +0200
@@ -8,11 +8,11 @@
can be shown by means of the \rmindex{lexicographic product} @{text"<*lex*>"}:
*}
-consts ack :: "nat\<times>nat \<Rightarrow> nat";
+consts ack :: "nat\<times>nat \<Rightarrow> nat"
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))";
+ "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"
text{*\noindent
The lexicographic product decreases if either its first component
@@ -67,8 +67,8 @@
*}
consts f :: "nat \<Rightarrow> nat"
-recdef f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
-"f i = (if #10 \<le> i then 0 else i * f(Suc i))";
+recdef (*<*)(permissive)(*<*)f "{(i,j). j<i \<and> i \<le> (#10::nat)}"
+"f i = (if #10 \<le> i then 0 else i * f(Suc i))"
text{*\noindent
Since \isacommand{recdef} is not prepared for the relation supplied above,
@@ -81,9 +81,9 @@
txt{*\noindent
The proof is by showing that our relation is a subset of another well-founded
relation: one given by a measure function.\index{*wf_subset (theorem)}
-*};
+*}
-apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast);
+apply (rule wf_subset [of "measure (\<lambda>k::nat. N-k)"], blast)
txt{*
@{subgoals[display,indent=0,margin=65]}
@@ -91,7 +91,7 @@
\noindent
The inclusion remains to be proved. After unfolding some definitions,
we are left with simple arithmetic:
-*};
+*}
apply (clarify, simp add: measure_def inv_image_def)
@@ -100,9 +100,9 @@
\noindent
And that is dispatched automatically:
-*};
+*}
-by arith;
+by arith
text{*\noindent
@@ -114,7 +114,7 @@
recdef g "{(i,j). j<i \<and> i \<le> (#10::nat)}"
"g i = (if #10 \<le> i then 0 else i * g(Suc i))"
(*>*)
-(hints recdef_wf: wf_greater);
+(hints recdef_wf: wf_greater)
text{*\noindent
Alternatively, we could have given @{text "measure (\<lambda>k::nat. #10-k)"} for the