*** empty log message ***

--- a/doc-src/TutorialI/CTL/CTL.thy	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/CTL/CTL.thy	Wed Dec 12 09:04:20 2001 +0100
@@ -460,7 +460,7 @@
 our model checkers.  It is clear that if all sets are finite, they can be
 represented as lists and the usual set operations are easily
 implemented. Only @{term lfp} requires a little thought.  Fortunately, theory
-@{text While_Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
+@{text While_Combinator} in the Library~\cite{HOL-Library} provides a
 theorem stating that in the case of finite sets and a monotone
 function~@{term F}, the value of \mbox{@{term"lfp F"}} can be computed by
 iterated application of @{term F} to~@{term"{}"} until a fixed point is

--- a/doc-src/TutorialI/CTL/document/CTL.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/CTL/document/CTL.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -469,7 +469,7 @@
 our model checkers.  It is clear that if all sets are finite, they can be
 represented as lists and the usual set operations are easily
 implemented. Only \isa{lfp} requires a little thought.  Fortunately, theory
-\isa{While{\isacharunderscore}Combinator} in the Library~\cite{isabelle-HOL-lib} provides a
+\isa{While{\isacharunderscore}Combinator} in the Library~\cite{HOL-Library} provides a
 theorem stating that in the case of finite sets and a monotone
 function~\isa{F}, the value of \mbox{\isa{lfp\ F}} can be computed by
 iterated application of \isa{F} to~\isa{{\isacharbraceleft}{\isacharbraceright}} until a fixed point is

--- a/doc-src/TutorialI/Misc/document/simp.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Misc/document/simp.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -232,7 +232,12 @@
   occurrences of $f$ with at least two arguments. This may be helpful for unfolding
   $f$ selectively, but it may also get in the way. Defining
   $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
-\end{warn}%
+\end{warn}
+
+There is also the special method \isa{unfold}\index{*unfold (method)|bold}
+which merely unfolds
+one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
+This is can be useful if \isa{simp} does too much.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %

--- a/doc-src/TutorialI/Misc/simp.thy	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Misc/simp.thy	Wed Dec 12 09:04:20 2001 +0100
@@ -197,6 +197,11 @@
   $f$ selectively, but it may also get in the way. Defining
   $f$~\isasymequiv~\isasymlambda$x\,y.\;t$ allows to unfold all occurrences of $f$.
 \end{warn}
+
+There is also the special method \isa{unfold}\index{*unfold (method)|bold}
+which merely unfolds
+one or several definitions, as in \isacommand{apply}\isa{(unfold xor_def)}.
+This is can be useful in situations where \isa{simp} does too much.
 *}
 
 subsection{*Simplifying {\tt\slshape let}-Expressions*}

--- a/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -23,7 +23,7 @@
 According to the measure function, the second argument should decrease with
 each recursive call. The resulting termination condition
 \begin{isabelle}%
-\ \ \ \ \ n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
+\ \ \ \ \ n\ {\isasymnoteq}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ m\ mod\ n\ {\isacharless}\ n%
 \end{isabelle}
 is proved automatically because it is already present as a lemma in
 HOL\@.  Thus the recursion equation becomes a simplification
@@ -70,7 +70,7 @@
 \begin{isamarkuptext}%
 \noindent
 The order of equations is important: it hides the side condition
-\isa{n\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}}.  Unfortunately, in general the case distinction
+\isa{n\ {\isasymnoteq}\ {\isadigit{0}}}.  Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A simple alternative is to replace \isa{if} by \isa{case}, 

--- a/doc-src/TutorialI/Recdef/document/termination.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/document/termination.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -59,7 +59,7 @@
 \begin{isamarkuptext}%
 \noindent
 This time everything works fine. Now \isa{f{\isachardot}simps} contains precisely
-the stated recursion equation for \isa{{\isacharquery}{\isacharquery}{\isachardot}f}, which has been stored as a
+the stated recursion equation for \isa{f}, which has been turned into a
 simplification rule.  Thus we can automatically prove results such as this one:%
 \end{isamarkuptext}%
 \isamarkuptrue%

--- a/doc-src/TutorialI/Recdef/simplification.thy	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Dec 12 09:04:20 2001 +0100
@@ -19,7 +19,7 @@
 text{*\noindent
 According to the measure function, the second argument should decrease with
 each recursive call. The resulting termination condition
-@{term[display]"n ~= 0 ==> m mod n < n"}
+@{term[display]"n ~= (0::nat) ==> m mod n < n"}
 is proved automatically because it is already present as a lemma in
 HOL\@.  Thus the recursion equation becomes a simplification
 rule. Of course the equation is nonterminating if we are allowed to unfold
@@ -58,7 +58,7 @@
 
 text{*\noindent
 The order of equations is important: it hides the side condition
-@{prop"n ~= 0"}.  Unfortunately, in general the case distinction
+@{prop"n ~= (0::nat)"}.  Unfortunately, in general the case distinction
 may not be expressible by pattern matching.
 
 A simple alternative is to replace @{text if} by @{text case}, 

--- a/doc-src/TutorialI/Recdef/termination.thy	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Recdef/termination.thy	Wed Dec 12 09:04:20 2001 +0100
@@ -48,7 +48,7 @@
 (*<*)local(*>*)
 text{*\noindent
 This time everything works fine. Now @{thm[source]f.simps} contains precisely
-the stated recursion equation for @{term f}, which has been stored as a
+the stated recursion equation for @{text f}, which has been turned into a
 simplification rule.  Thus we can automatically prove results such as this one:
 *}
 

--- a/doc-src/TutorialI/Sets/sets.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Sets/sets.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -965,7 +965,7 @@
 the well-founded relation used to prove termination.
 
 The \bfindex{multiset ordering}, useful for hard termination proofs, is
-available in the Library~\cite{isabelle-HOL-lib}.
+available in the Library~\cite{HOL-Library}.
 Baader and Nipkow \cite[{\S}2.5]{Baader-Nipkow} discuss it. 
 
 \medskip

--- a/doc-src/TutorialI/Types/Typedefs.thy	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Types/Typedefs.thy	Wed Dec 12 09:04:20 2001 +0100
@@ -69,13 +69,14 @@
 It is easily represented by the first three natural numbers:
 *}
 
-typedef three = "{n::nat. n \<le> 2}"
+typedef three = "{0::nat, 1, 2}"
 
 txt{*\noindent
 In order to enforce that the representing set on the right-hand side is
 non-empty, this definition actually starts a proof to that effect:
 @{subgoals[display,indent=0]}
-Fortunately, this is easy enough to show: take 0 as a witness.
+Fortunately, this is easy enough to show, even \isa{auto} could do it.
+In general, one has to provide a witness, in our case 0:
 *}
 
 apply(rule_tac x = 0 in exI)
@@ -127,7 +128,7 @@
 %
 From this example it should be clear what \isacommand{typedef} does
 in general given a name (here @{text three}) and a set
-(here @{term"{n::nat. n\<le>2}"}).
+(here @{term"{0::nat,1,2}"}).
 
 Our next step is to define the basic functions expected on the new type.
 Although this depends on the type at hand, the following strategy works well:
@@ -161,17 +162,30 @@
 and that they exhaust the type.
 
 In processing our \isacommand{typedef} declaration, 
-Isabelle helpfully proves several lemmas.
-One, @{thm[source]Abs_three_inject},
-expresses that @{term Abs_three} is injective on the representing subset:
+Isabelle proves several helpful lemmas. The first two
+express injectivity of @{term Rep_three} and @{term Abs_three}:
 \begin{center}
-@{thm Abs_three_inject[no_vars]}
+\begin{tabular}{@ {}r@ {\qquad}l@ {}}
+@{thm Rep_three_inject[no_vars]} & (@{thm[source]Rep_three_inject}) \\
+\begin{tabular}{@ {}l@ {}}
+@{text"\<lbrakk>x \<in> three; y \<in> three \<rbrakk>"} \\
+@{text"\<Longrightarrow> (Abs_three x = Abs_three y) = (x = y)"}
+\end{tabular} & (@{thm[source]Abs_three_inject}) \\
+\end{tabular}
 \end{center}
-Another, @{thm[source]Rep_three_inject}, expresses that the representation
-function is also injective:
+The following ones allow to replace some @{text"x::three"} by
+@{text"Abs_three(y::nat)"}, and conversely @{term y} by @{term"Rep_three x"}:
 \begin{center}
-@{thm Rep_three_inject[no_vars]}
+\begin{tabular}{@ {}r@ {\qquad}l@ {}}
+@{thm Rep_three_cases[no_vars]} & (@{thm[source]Rep_three_cases}) \\
+@{thm Abs_three_cases[no_vars]} & (@{thm[source]Abs_three_cases}) \\
+@{thm Rep_three_induct[no_vars]} & (@{thm[source]Rep_three_induct}) \\
+@{thm Abs_three_induct[no_vars]} & (@{thm[source]Abs_three_induct}) \\
+\end{tabular}
 \end{center}
+These theorems are proved for any type definition, with @{term three}
+replaced by the name of the type in question.
+
 Distinctness of @{term A}, @{term B} and @{term C} follows immediately
 if we expand their definitions and rewrite with the injectivity
 of @{term Abs_three}:
@@ -181,57 +195,26 @@
 by(simp add: Abs_three_inject A_def B_def C_def three_def)
 
 text{*\noindent
-Of course we rely on the simplifier to solve goals like @{prop"0 \<noteq> 1"}.
+Of course we rely on the simplifier to solve goals like @{prop"(0::nat) \<noteq> 1"}.
 
 The fact that @{term A}, @{term B} and @{term C} exhaust type @{typ three} is
 best phrased as a case distinction theorem: if you want to prove @{prop"P x"}
 (where @{term x} is of type @{typ three}) it suffices to prove @{prop"P A"},
-@{prop"P B"} and @{prop"P C"}. First we prove the analogous proposition for the
-representation: *}
-
-lemma cases_lemma: "\<lbrakk> Q 0; Q 1; Q 2; n \<in> three \<rbrakk> \<Longrightarrow>  Q n"
-
-txt{*\noindent
-Expanding @{thm[source]three_def} yields the premise @{prop"n\<le>2"}. Repeated
-elimination with @{thm[source]le_SucE}
-@{thm[display]le_SucE}
-reduces @{prop"n\<le>2"} to the three cases @{prop"n\<le>0"}, @{prop"n=1"} and
-@{prop"n=2"} which are trivial for simplification:
-*}
-
-apply(simp add: three_def numerals)   (* FIXME !? *)
-apply((erule le_SucE)+)
-apply simp_all
-done
-
-text{*
-Now the case distinction lemma on type @{typ three} is easy to derive if you 
-know how:
-*}
+@{prop"P B"} and @{prop"P C"}: *}
 
 lemma three_cases: "\<lbrakk> P A; P B; P C \<rbrakk> \<Longrightarrow> P x"
 
-txt{*\noindent
-We start by replacing the @{term x} by @{term"Abs_three(Rep_three x)"}:
-*}
-
-apply(rule subst[OF Rep_three_inverse])
+txt{*\noindent Again this follows easily from a pre-proved general theorem:*}
 
-txt{*\noindent
-This substitution step worked nicely because there was just a single
-occurrence of a term of type @{typ three}, namely @{term x}.
-When we now apply @{thm[source]cases_lemma}, @{term Q} becomes @{term"\<lambda>n. P(Abs_three
-n)"} because @{term"Rep_three x"} is the only term of type @{typ nat}:
-*}
-
-apply(rule cases_lemma)
+apply(rule_tac x = x in Abs_three_induct)
 
 txt{*
 @{subgoals[display,indent=0]}
-The resulting subgoals are easily solved by simplification:
-*}
+Simplification with @{thm[source]three_def} leads to the disjunction @{prop"y
+= 0 \<or> y = 1 \<or> y = (2::nat)"} which \isa{auto} separates into three
+subgoals, each of which is easily solved by simplification: *}
 
-apply(simp_all add:A_def B_def C_def Rep_three)
+apply(auto simp add: three_def A_def B_def C_def)
 done
 
 text{*\noindent
@@ -253,7 +236,7 @@
 example to demonstrate \isacommand{typedef} because its simplicity makes the
 key concepts particularly easy to grasp. If you would like to see a
 non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the Library~\cite{isabelle-HOL-lib}.
+definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
 
 Let us conclude by summarizing the above procedure for defining a new type.
 Given some abstract axiomatic description $P$ of a type $ty$ in terms of a

--- a/doc-src/TutorialI/Types/document/Typedefs.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/Types/document/Typedefs.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -86,16 +86,17 @@
 It is easily represented by the first three natural numbers:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}n{\isacharcolon}{\isacharcolon}nat{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
+\isacommand{typedef}\ three\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}{\isadigit{0}}{\isacharcolon}{\isacharcolon}nat{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \noindent
 In order to enforce that the representing set on the right-hand side is
 non-empty, this definition actually starts a proof to that effect:
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}%
+\ {\isadigit{1}}{\isachardot}\ {\isasymexists}x{\isachardot}\ x\ {\isasymin}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}%
 \end{isabelle}
-Fortunately, this is easy enough to show: take 0 as a witness.%
+Fortunately, this is easy enough to show, even \isa{auto} could do it.
+In general, one has to provide a witness, in our case 0:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
 \isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ {\isadigit{0}}\ \isakeyword{in}\ exI{\isacharparenright}\isanewline
@@ -117,7 +118,7 @@
 \end{center}
 where constant \isa{three} is explicitly defined as the representing set:
 \begin{center}
-\isa{three\ {\isasymequiv}\ {\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
+\isa{three\ {\isasymequiv}\ {\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}\hfill(\isa{three{\isacharunderscore}def})
 \end{center}
 The situation is best summarized with the help of the following diagram,
 where squares are types and circles are sets:
@@ -147,7 +148,7 @@
 %
 From this example it should be clear what \isacommand{typedef} does
 in general given a name (here \isa{three}) and a set
-(here \isa{{\isacharbraceleft}n{\isachardot}\ n\ {\isasymle}\ {\isadigit{2}}{\isacharbraceright}}).
+(here \isa{{\isacharbraceleft}{\isadigit{0}}{\isacharcomma}\ {\isadigit{1}}{\isacharcomma}\ {\isadigit{2}}{\isacharbraceright}}).
 
 Our next step is to define the basic functions expected on the new type.
 Although this depends on the type at hand, the following strategy works well:
@@ -179,17 +180,30 @@
 and that they exhaust the type.
 
 In processing our \isacommand{typedef} declaration, 
-Isabelle helpfully proves several lemmas.
-One, \isa{Abs{\isacharunderscore}three{\isacharunderscore}inject},
-expresses that \isa{Abs{\isacharunderscore}three} is injective on the representing subset:
+Isabelle proves several helpful lemmas. The first two
+express injectivity of \isa{Rep{\isacharunderscore}three} and \isa{Abs{\isacharunderscore}three}:
 \begin{center}
-\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
+\begin{tabular}{@ {}r@ {\qquad}l@ {}}
+\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}) \\
+\begin{tabular}{@ {}l@ {}}
+\isa{{\isasymlbrakk}x\ {\isasymin}\ three{\isacharsemicolon}\ y\ {\isasymin}\ three\ {\isasymrbrakk}} \\
+\isa{{\isasymLongrightarrow}\ {\isacharparenleft}Abs{\isacharunderscore}three\ x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
+\end{tabular} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}inject}) \\
+\end{tabular}
 \end{center}
-Another, \isa{Rep{\isacharunderscore}three{\isacharunderscore}inject}, expresses that the representation
-function is also injective:
+The following ones allow to replace some \isa{x{\isacharcolon}{\isacharcolon}three} by
+\isa{Abs{\isacharunderscore}three{\isacharparenleft}y{\isacharcolon}{\isacharcolon}nat{\isacharparenright}}, and conversely \isa{y} by \isa{Rep{\isacharunderscore}three\ x}:
 \begin{center}
-\isa{{\isacharparenleft}Rep{\isacharunderscore}three\ x\ {\isacharequal}\ Rep{\isacharunderscore}three\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}x\ {\isacharequal}\ y{\isacharparenright}}
+\begin{tabular}{@ {}r@ {\qquad}l@ {}}
+\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ y\ {\isacharequal}\ Rep{\isacharunderscore}three\ x\ {\isasymLongrightarrow}\ P{\isasymrbrakk}\ {\isasymLongrightarrow}\ P} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}cases}) \\
+\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ {\isasymlbrakk}x\ {\isacharequal}\ Abs{\isacharunderscore}three\ y{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P{\isacharparenright}\ {\isasymLongrightarrow}\ P} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}cases}) \\
+\isa{{\isasymlbrakk}y\ {\isasymin}\ three{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ P\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ y} & (\isa{Rep{\isacharunderscore}three{\isacharunderscore}induct}) \\
+\isa{{\isacharparenleft}{\isasymAnd}y{\isachardot}\ y\ {\isasymin}\ three\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\ P\ x} & (\isa{Abs{\isacharunderscore}three{\isacharunderscore}induct}) \\
+\end{tabular}
 \end{center}
+These theorems are proved for any type definition, with \isa{three}
+replaced by the name of the type in question.
+
 Distinctness of \isa{A}, \isa{B} and \isa{C} follows immediately
 if we expand their definitions and rewrite with the injectivity
 of \isa{Abs{\isacharunderscore}three}:%
@@ -201,70 +215,31 @@
 %
 \begin{isamarkuptext}%
 \noindent
-Of course we rely on the simplifier to solve goals like \isa{{\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymnoteq}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}}.
+Of course we rely on the simplifier to solve goals like \isa{{\isadigit{0}}\ {\isasymnoteq}\ {\isadigit{1}}}.
 
 The fact that \isa{A}, \isa{B} and \isa{C} exhaust type \isa{three} is
 best phrased as a case distinction theorem: if you want to prove \isa{P\ x}
 (where \isa{x} is of type \isa{three}) it suffices to prove \isa{P\ A},
-\isa{P\ B} and \isa{P\ C}. First we prove the analogous proposition for the
-representation:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\ cases{\isacharunderscore}lemma{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ Q\ {\isadigit{0}}{\isacharsemicolon}\ Q\ {\isadigit{1}}{\isacharsemicolon}\ Q\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isasymin}\ three\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ \ Q\ n{\isachardoublequote}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-Expanding \isa{three{\isacharunderscore}def} yields the premise \isa{n\ {\isasymle}\ {\isadigit{2}}}. Repeated
-elimination with \isa{le{\isacharunderscore}SucE}
-\begin{isabelle}%
-{\isasymlbrakk}{\isacharquery}m\ {\isasymle}\ Suc\ {\isacharquery}n{\isacharsemicolon}\ {\isacharquery}m\ {\isasymle}\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharsemicolon}\ {\isacharquery}m\ {\isacharequal}\ Suc\ {\isacharquery}n\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R%
-\end{isabelle}
-reduces \isa{n\ {\isasymle}\ {\isadigit{2}}} to the three cases \isa{n\ {\isasymle}\ {\isadigit{0}}}, \isa{n\ {\isacharequal}\ {\isadigit{1}}} and
-\isa{n\ {\isacharequal}\ {\isadigit{2}}} which are trivial for simplification:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ numerals{\isacharparenright}\ \ \ \isanewline
-\isamarkupfalse%
-\isacommand{apply}{\isacharparenleft}{\isacharparenleft}erule\ le{\isacharunderscore}SucE{\isacharparenright}{\isacharplus}{\isacharparenright}\isanewline
-\isamarkupfalse%
-\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
-\isamarkupfalse%
-\isacommand{done}\isamarkupfalse%
-%
-\begin{isamarkuptext}%
-Now the case distinction lemma on type \isa{three} is easy to derive if you 
-know how:%
+\isa{P\ B} and \isa{P\ C}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{lemma}\ three{\isacharunderscore}cases{\isacharcolon}\ {\isachardoublequote}{\isasymlbrakk}\ P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ x{\isachardoublequote}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
-\noindent
-We start by replacing the \isa{x} by \isa{Abs{\isacharunderscore}three\ {\isacharparenleft}Rep{\isacharunderscore}three\ x{\isacharparenright}}:%
+\noindent Again this follows easily from a pre-proved general theorem:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}rule\ subst{\isacharbrackleft}OF\ Rep{\isacharunderscore}three{\isacharunderscore}inverse{\isacharbrackright}{\isacharparenright}\isamarkupfalse%
-%
-\begin{isamarkuptxt}%
-\noindent
-This substitution step worked nicely because there was just a single
-occurrence of a term of type \isa{three}, namely \isa{x}.
-When we now apply \isa{cases{\isacharunderscore}lemma}, \isa{Q} becomes \isa{{\isasymlambda}n{\isachardot}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ n{\isacharparenright}} because \isa{Rep{\isacharunderscore}three\ x} is the only term of type \isa{nat}:%
-\end{isamarkuptxt}%
-\isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}rule\ cases{\isacharunderscore}lemma{\isacharparenright}\isamarkupfalse%
+\isacommand{apply}{\isacharparenleft}rule{\isacharunderscore}tac\ x\ {\isacharequal}\ x\ \isakeyword{in}\ Abs{\isacharunderscore}three{\isacharunderscore}induct{\isacharparenright}\isamarkupfalse%
 %
 \begin{isamarkuptxt}%
 \begin{isabelle}%
-\ {\isadigit{1}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{0}}{\isacharparenright}\isanewline
-\ {\isadigit{2}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{1}}{\isacharparenright}\isanewline
-\ {\isadigit{3}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ {\isadigit{2}}{\isacharparenright}\isanewline
-\ {\isadigit{4}}{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isasymrbrakk}\ {\isasymLongrightarrow}\ Rep{\isacharunderscore}three\ x\ {\isasymin}\ three%
+\ {\isadigit{1}}{\isachardot}\ {\isasymAnd}y{\isachardot}\ {\isasymlbrakk}P\ A{\isacharsemicolon}\ P\ B{\isacharsemicolon}\ P\ C{\isacharsemicolon}\ y\ {\isasymin}\ three{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}Abs{\isacharunderscore}three\ y{\isacharparenright}%
 \end{isabelle}
-The resulting subgoals are easily solved by simplification:%
+Simplification with \isa{three{\isacharunderscore}def} leads to the disjunction \isa{y\ {\isacharequal}\ {\isadigit{0}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{1}}\ {\isasymor}\ y\ {\isacharequal}\ {\isadigit{2}}} which \isa{auto} separates into three
+subgoals, each of which is easily solved by simplification:%
 \end{isamarkuptxt}%
 \isamarkuptrue%
-\isacommand{apply}{\isacharparenleft}simp{\isacharunderscore}all\ add{\isacharcolon}A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def\ Rep{\isacharunderscore}three{\isacharparenright}\isanewline
+\isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ three{\isacharunderscore}def\ A{\isacharunderscore}def\ B{\isacharunderscore}def\ C{\isacharunderscore}def{\isacharparenright}\isanewline
 \isamarkupfalse%
 \isacommand{done}\isamarkupfalse%
 %
@@ -289,7 +264,7 @@
 example to demonstrate \isacommand{typedef} because its simplicity makes the
 key concepts particularly easy to grasp. If you would like to see a
 non-trivial example that cannot be defined more directly, we recommend the
-definition of \emph{finite multisets} in the Library~\cite{isabelle-HOL-lib}.
+definition of \emph{finite multisets} in the Library~\cite{HOL-Library}.
 
 Let us conclude by summarizing the above procedure for defining a new type.
 Given some abstract axiomatic description $P$ of a type $ty$ in terms of a

--- a/doc-src/TutorialI/basics.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/basics.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -89,9 +89,9 @@
   Unless you know what you are doing, always include \isa{Main}
   as a direct or indirect parent of all your theories.
 \end{warn}
-There is also a growing Library~\cite{isabelle-library}\index{Library}
+There is also a growing Library~\cite{HOL-Library}\index{Library}
 of useful theories that are not part of \isa{Main} but can to be included
-among the parents of a theory and will then be included automatically.%
+among the parents of a theory and will then be loaded automatically.%
 \index{theories|)}
 
 

--- a/doc-src/TutorialI/fp.tex	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/fp.tex	Wed Dec 12 09:04:20 2001 +0100
@@ -527,7 +527,6 @@
 
 \subsection{Simplification and Recursive Functions}
 \label{sec:recdef-simplification}
-
 \input{Recdef/document/simplification.tex}
 
 \subsection{Induction and Recursive Functions}

--- a/doc-src/TutorialI/todo.tobias	Tue Dec 11 17:07:45 2001 +0100
+++ b/doc-src/TutorialI/todo.tobias	Wed Dec 12 09:04:20 2001 +0100
@@ -36,9 +36,6 @@
 use arith_tac in recdef to solve termination conditions?
 -> new example in Recdef/termination
 
-a tactic for replacing a specific occurrence:
-apply(subst [2] thm)
-
 it would be nice if @term could deal with ?-vars.
 then a number of (unchecked!) @texts could be converted to @terms.
 
@@ -60,49 +57,16 @@
 Minor fixes in the tutorial
 ===========================
 
-1/2 no longer abbrevs for Suc.
-Warning: needs simplification to turn 1 into Suc 0. arith does so
-automatically.
-
-recdef: failed tcs no longer shown! (sec:Recursion over nested datatypes)
-say something about how conditions are proved?
-No, better show failed proof attempts.
-
-Advanced recdef: explain recdef_tc? No. Adjust recdef!
-
-Adjust FP textbook refs: new Bird, Hudak
-Discrete math textbook: Rosen?
-
-adjust type of ^ in tab:overloading
-
-an example of induction: !y. A --> B --> C ??
-
-Explain type_definition and mention pre-proved thms in subset.thy?
--> Types/typedef
-
 Appendix: Lexical: long ids.
 
 Warning: infixes automatically become reserved words!
 
-Forward ref from blast proof of Puzzle (AdvancedInd) to Isar proof?
-
-recdef with nested recursion: either an example or at least a pointer to the
-literature. In Recdef/termination.thy, at the end.
-%FIXME, with one exception: nested recursion.
-
 Syntax section: syntax annotations not just for consts but also for constdefs and datatype.
 
 Appendix with list functions.
 
 All theory sources on the web?
 
-
-Minor additions to the tutorial, unclear where
-==============================================
-
-unfold?
-
-
 Possible exercises
 ==================