# HG changeset patch
# User nipkow
# Date 987519278 -7200
# Node ID 49afcce3bada3f423ce676bd0e87d286ade6271f
# Parent  ca546b170471785917579b7168f433a1b9101153
*** empty log message ***

diff -r ca546b170471 -r 49afcce3bada doc-src/TutorialI/Advanced/Partial.thy
--- a/doc-src/TutorialI/Advanced/Partial.thy	Tue Apr 17 15:03:41 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy	Tue Apr 17 16:54:38 2001 +0200
@@ -29,7 +29,7 @@
 
 text{*
 The rest of this section is devoted to the question of how to define
-partial recursive functions by other means that non-exhaustive pattern
+partial recursive functions by other means than non-exhaustive pattern
 matching.
 *}
 
diff -r ca546b170471 -r 49afcce3bada doc-src/TutorialI/Advanced/document/Partial.tex
--- a/doc-src/TutorialI/Advanced/document/Partial.tex	Tue Apr 17 15:03:41 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex	Tue Apr 17 16:54:38 2001 +0200
@@ -29,7 +29,7 @@
 {\isachardoublequote}n\ {\isasymle}\ m\ {\isasymLongrightarrow}\ minus\ m\ n\ {\isasymequiv}\ m\ {\isacharminus}\ n{\isachardoublequote}%
 \begin{isamarkuptext}%
 The rest of this section is devoted to the question of how to define
-partial recursive functions by other means that non-exhaustive pattern
+partial recursive functions by other means than non-exhaustive pattern
 matching.%
 \end{isamarkuptext}%
 %
diff -r ca546b170471 -r 49afcce3bada doc-src/TutorialI/Datatype/Nested.thy
--- a/doc-src/TutorialI/Datatype/Nested.thy	Tue Apr 17 15:03:41 2001 +0200
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Tue Apr 17 16:54:38 2001 +0200
@@ -5,7 +5,9 @@
 text{*
 So far, all datatypes had the property that on the right-hand side of their
 definition they occurred only at the top-level, i.e.\ directly below a
-constructor. This is not the case any longer for the following model of terms
+constructor. Now we consider \emph{nested recursion}, where the recursive
+datatupe occurs nested in some other datatype (but not inside itself!).
+Consider the following model of terms
 where function symbols can be applied to a list of arguments:
 *}
 (*<*)hide const Var(*>*)
@@ -126,4 +128,4 @@
 *}
 (*<*)
 end
-(*>*)
\ No newline at end of file
+(*>*)
diff -r ca546b170471 -r 49afcce3bada doc-src/TutorialI/Datatype/document/Nested.tex
--- a/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Apr 17 15:03:41 2001 +0200
+++ b/doc-src/TutorialI/Datatype/document/Nested.tex	Tue Apr 17 16:54:38 2001 +0200
@@ -5,7 +5,9 @@
 \begin{isamarkuptext}%
 So far, all datatypes had the property that on the right-hand side of their
 definition they occurred only at the top-level, i.e.\ directly below a
-constructor. This is not the case any longer for the following model of terms
+constructor. Now we consider \emph{nested recursion}, where the recursive
+datatupe occurs nested in some other datatype (but not inside itself!).
+Consider the following model of terms
 where function symbols can be applied to a list of arguments:%
 \end{isamarkuptext}%
 \isacommand{datatype}\ {\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}{\isachardoublequote}term{\isachardoublequote}\ {\isacharequal}\ Var\ {\isacharprime}v\ {\isacharbar}\ App\ {\isacharprime}f\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}v{\isacharcomma}{\isacharprime}f{\isacharparenright}term\ list{\isachardoublequote}%
diff -r ca546b170471 -r 49afcce3bada doc-src/TutorialI/Misc/AdvancedInd.thy
--- a/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Apr 17 15:03:41 2001 +0200
+++ b/doc-src/TutorialI/Misc/AdvancedInd.thy	Tue Apr 17 16:54:38 2001 +0200
@@ -124,7 +124,16 @@
 consts f :: "nat \<Rightarrow> nat";
 axioms f_ax: "f(f(n)) < f(Suc(n))";
 
-text{*\noindent
+text{*
+\begin{warn}
+We discourage the use of axioms because of the danger of
+inconsistencies.  Axiom @{text f_ax} does
+not introduce an inconsistency because, for example, the identity function
+satisfies it.  Axioms can be useful in exploratory developments, say when 
+you assume some well-known theorems so that you can quickly demonstrate some
+point about methodology.  If your example turns into a substantial proof
+development, you should replace axioms by theorems.
+\end{warn}\noindent
 The axiom for @{term"f"} implies @{prop"n <= f n"}, which can
 be proved by induction on \mbox{@{term"f n"}}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:
@@ -197,40 +206,31 @@
 (*<*)oops;(*>*)
 
 text{*
-\begin{warn}
-We discourage the use of axioms because of the danger of
-inconsistencies.  Axiom @{text f_ax} does
-not introduce an inconsistency because, for example, the identity function
-satisfies it.  Axioms can be useful in exploratory developments, say when 
-you assume some well-known theorems so that you can quickly demonstrate some
-point about methodology.  If your example turns into a substantial proof
-development, you should replace the axioms by proofs.
-\end{warn}
+\begin{exercise}
+From the axiom and lemma for @{term"f"}, show that @{term"f"} is the
+identity function.
+\end{exercise}
 
-\bigskip
-In general, @{text induct_tac} can be applied with any rule $r$
+Method @{text induct_tac} can be applied with any rule $r$
 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
 format is
 \begin{quote}
 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"rule:"} $r$@{text")"}
 \end{quote}\index{*induct_tac}%
 where $y@1, \dots, y@n$ are variables in the first subgoal.
-A further example of a useful induction rule is @{thm[source]length_induct},
-induction on the length of a list:\indexbold{*length_induct}
-@{thm[display]length_induct[no_vars]}
-
-In fact, @{text"induct_tac"} even allows the conclusion of
-$r$ to be an (iterated) conjunction of formulae of the above form, in
-which case the application is
+The conclusion of $r$ can even be an (iterated) conjunction of formulae of
+the above form in which case the application is
 \begin{quote}
 \isacommand{apply}@{text"(induct_tac"} $y@1 \dots y@n$ @{text"and"} \dots\ @{text"and"} $z@1 \dots z@m$ @{text"rule:"} $r$@{text")"}
 \end{quote}
 
-\begin{exercise}
-From the axiom and lemma for @{term"f"}, show that @{term"f"} is the
-identity function.
-\end{exercise}
-*};
+A further useful induction rule is @{thm[source]length_induct},
+induction on the length of a list\indexbold{*length_induct}
+@{thm[display]length_induct[no_vars]}
+which is a special case of @{thm[source]measure_induct}
+@{thm[display]measure_induct[no_vars]}
+where @{term f} may be any function into type @{typ nat}.
+*}
 
 subsection{*Derivation of New Induction Schemas*};
 
@@ -259,9 +259,9 @@
 @{thm[display]"less_SucE"[no_vars]}
 
 Now it is straightforward to derive the original version of
-@{thm[source]nat_less_induct} by manipulting the conclusion of the above lemma:
-instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"} and
-remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
+@{thm[source]nat_less_induct} by manipulating the conclusion of the above
+lemma: instantiate @{term"n"} by @{term"Suc n"} and @{term"m"} by @{term"n"}
+and remove the trivial condition @{prop"n < Suc n"}. Fortunately, this
 happens automatically when we add the lemma as a new premise to the
 desired goal:
 *};
diff -r ca546b170471 -r 49afcce3bada doc-src/TutorialI/Misc/document/AdvancedInd.tex
--- a/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Apr 17 15:03:41 2001 +0200
+++ b/doc-src/TutorialI/Misc/document/AdvancedInd.tex	Tue Apr 17 16:54:38 2001 +0200
@@ -120,7 +120,15 @@
 \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
 \isacommand{axioms}\ f{\isacharunderscore}ax{\isacharcolon}\ {\isachardoublequote}f{\isacharparenleft}f{\isacharparenleft}n{\isacharparenright}{\isacharparenright}\ {\isacharless}\ f{\isacharparenleft}Suc{\isacharparenleft}n{\isacharparenright}{\isacharparenright}{\isachardoublequote}%
 \begin{isamarkuptext}%
-\noindent
+\begin{warn}
+We discourage the use of axioms because of the danger of
+inconsistencies.  Axiom \isa{f{\isacharunderscore}ax} does
+not introduce an inconsistency because, for example, the identity function
+satisfies it.  Axioms can be useful in exploratory developments, say when 
+you assume some well-known theorems so that you can quickly demonstrate some
+point about methodology.  If your example turns into a substantial proof
+development, you should replace axioms by theorems.
+\end{warn}\noindent
 The axiom for \isa{f} implies \isa{n\ {\isasymle}\ f\ n}, which can
 be proved by induction on \mbox{\isa{f\ n}}. Following the recipe outlined
 above, we have to phrase the proposition as follows to allow induction:%
@@ -193,41 +201,34 @@
 \end{isamarkuptext}%
 \isacommand{lemma}\ f{\isacharunderscore}incr{\isacharbrackleft}rule{\isacharunderscore}format{\isacharcomma}\ OF\ refl{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}i{\isachardot}\ k\ {\isacharequal}\ f\ i\ {\isasymlongrightarrow}\ i\ {\isasymle}\ f\ i{\isachardoublequote}%
 \begin{isamarkuptext}%
-\begin{warn}
-We discourage the use of axioms because of the danger of
-inconsistencies.  Axiom \isa{f{\isacharunderscore}ax} does
-not introduce an inconsistency because, for example, the identity function
-satisfies it.  Axioms can be useful in exploratory developments, say when 
-you assume some well-known theorems so that you can quickly demonstrate some
-point about methodology.  If your example turns into a substantial proof
-development, you should replace the axioms by proofs.
-\end{warn}
+\begin{exercise}
+From the axiom and lemma for \isa{f}, show that \isa{f} is the
+identity function.
+\end{exercise}
 
-\bigskip
-In general, \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
+Method \isa{induct{\isacharunderscore}tac} can be applied with any rule $r$
 whose conclusion is of the form ${?}P~?x@1 \dots ?x@n$, in which case the
 format is
 \begin{quote}
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
 \end{quote}\index{*induct_tac}%
 where $y@1, \dots, y@n$ are variables in the first subgoal.
-A further example of a useful induction rule is \isa{length{\isacharunderscore}induct},
-induction on the length of a list:\indexbold{*length_induct}
-\begin{isabelle}%
-\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
-\end{isabelle}
-
-In fact, \isa{induct{\isacharunderscore}tac} even allows the conclusion of
-$r$ to be an (iterated) conjunction of formulae of the above form, in
-which case the application is
+The conclusion of $r$ can even be an (iterated) conjunction of formulae of
+the above form in which case the application is
 \begin{quote}
 \isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac} $y@1 \dots y@n$ \isa{and} \dots\ \isa{and} $z@1 \dots z@m$ \isa{rule{\isacharcolon}} $r$\isa{{\isacharparenright}}
 \end{quote}
 
-\begin{exercise}
-From the axiom and lemma for \isa{f}, show that \isa{f} is the
-identity function.
-\end{exercise}%
+A further useful induction rule is \isa{length{\isacharunderscore}induct},
+induction on the length of a list\indexbold{*length_induct}
+\begin{isabelle}%
+\ \ \ \ \ {\isacharparenleft}{\isasymAnd}xs{\isachardot}\ {\isasymforall}ys{\isachardot}\ length\ ys\ {\isacharless}\ length\ xs\ {\isasymlongrightarrow}\ P\ ys\ {\isasymLongrightarrow}\ P\ xs{\isacharparenright}\ {\isasymLongrightarrow}\ P\ xs%
+\end{isabelle}
+which is a special case of \isa{measure{\isacharunderscore}induct}
+\begin{isabelle}%
+\ \ \ \ \ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isasymforall}y{\isachardot}\ f\ y\ {\isacharless}\ f\ x\ {\isasymlongrightarrow}\ P\ y\ {\isasymLongrightarrow}\ P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ P\ a%
+\end{isabelle}
+where \isa{f} may be any function into type \isa{nat}.%
 \end{isamarkuptext}%
 %
 \isamarkupsubsection{Derivation of New Induction Schemas%
@@ -259,9 +260,9 @@
 \end{isabelle}
 
 Now it is straightforward to derive the original version of
-\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulting the conclusion of the above lemma:
-instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n} and
-remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
+\isa{nat{\isacharunderscore}less{\isacharunderscore}induct} by manipulating the conclusion of the above
+lemma: instantiate \isa{n} by \isa{Suc\ n} and \isa{m} by \isa{n}
+and remove the trivial condition \isa{n\ {\isacharless}\ Suc\ n}. Fortunately, this
 happens automatically when we add the lemma as a new premise to the
 desired goal:%
 \end{isamarkuptext}%
diff -r ca546b170471 -r 49afcce3bada doc-src/TutorialI/todo.tobias
--- a/doc-src/TutorialI/todo.tobias	Tue Apr 17 15:03:41 2001 +0200
+++ b/doc-src/TutorialI/todo.tobias	Tue Apr 17 16:54:38 2001 +0200
@@ -54,8 +54,10 @@
 ===========================
 
 recdef: failed tcs no longer shown!
+say something about how conditions are proved?
+No, better show failed proof attempts.
 
-Advanced recdef: explain recdef_tc?
+Advanced recdef: explain recdef_tc? No. Adjust recdef!
 
 Adjust FP textbook refs: new Bird, Hudak
 Discrete math textbook: Rosen?