I wonder which files i forgot.

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,127 @@
+(*<*)
+theory ABexpr = Main:;
+(*>*)
+
+text{*
+Sometimes it is necessary to define two datatypes that depend on each
+other. This is called \textbf{mutual recursion}. As an example consider a
+language of arithmetic and boolean expressions where
+\begin{itemize}
+\item arithmetic expressions contain boolean expressions because there are
+  conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
+  and
+\item boolean expressions contain arithmetic expressions because of
+  comparisons like ``$m<n$''.
+\end{itemize}
+In Isabelle this becomes
+*}
+
+datatype 'a aexp = IF   "'a bexp" "'a aexp" "'a aexp"
+                 | Sum  "'a aexp" "'a aexp"
+                 | Diff "'a aexp" "'a aexp"
+                 | Var 'a
+                 | Num nat
+and      'a bexp = Less "'a aexp" "'a aexp"
+                 | And  "'a bexp" "'a bexp"
+                 | Neg  "'a bexp";
+
+text{*\noindent
+Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
+except that we have fixed the values to be of type \isa{nat} and that we
+have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
+expressions can be arithmetic comparisons, conjunctions and negations.
+The semantics is fixed via two evaluation functions
+*}
+
+consts  evala :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a aexp \\<Rightarrow> nat"
+        evalb :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a bexp \\<Rightarrow> bool";
+
+text{*\noindent
+that take an environment (a mapping from variables \isa{'a} to values
+\isa{nat}) and an expression and return its arithmetic/boolean
+value. Since the datatypes are mutually recursive, so are functions that
+operate on them. Hence they need to be defined in a single \isacommand{primrec}
+section:
+*}
+
+primrec
+  "evala env (IF b a1 a2) =
+     (if evalb env b then evala env a1 else evala env a2)"
+  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
+  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
+  "evala env (Var v) = env v"
+  "evala env (Num n) = n"
+
+  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
+  "evalb env (And b1 b2) = (evalb env b1 \\<and> evalb env b2)"
+  "evalb env (Neg b) = (\\<not> evalb env b)"
+
+text{*\noindent
+In the same fashion we also define two functions that perform substitution:
+*}
+
+consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp"
+       substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp";
+
+text{*\noindent
+The first argument is a function mapping variables to expressions, the
+substitution. It is applied to all variables in the second argument. As a
+result, the type of variables in the expression may change from \isa{'a}
+to \isa{'b}. Note that there are only arithmetic and no boolean variables.
+*}
+
+primrec
+  "substa s (IF b a1 a2) =
+     IF (substb s b) (substa s a1) (substa s a2)"
+  "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
+  "substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)"
+  "substa s (Var v) = s v"
+  "substa s (Num n) = Num n"
+
+  "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
+  "substb s (And b1 b2) = And (substb s b1) (substb s b2)"
+  "substb s (Neg b) = Neg (substb s b)";
+
+text{*
+Now we can prove a fundamental theorem about the interaction between
+evaluation and substitution: applying a substitution $s$ to an expression $a$
+and evaluating the result in an environment $env$ yields the same result as
+evaluation $a$ in the environment that maps every variable $x$ to the value
+of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
+boolean expressions (by induction), you find that you always need the other
+theorem in the induction step. Therefore you need to state and prove both
+theorems simultaneously:
+*}
+
+lemma "evala env (substa s a) = evala (\\<lambda>x. evala env (s x)) a \\<and>
+        evalb env (substb s b) = evalb (\\<lambda>x. evala env (s x)) b";
+apply(induct_tac a and b);
+
+txt{*\noindent
+The resulting 8 goals (one for each constructor) are proved in one fell swoop:
+*}
+
+apply auto.;
+
+text{*
+In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
+an inductive proof expects a goal of the form
+\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
+where each variable $x@i$ is of type $\tau@i$. Induction is started by
+\begin{ttbox}
+apply(induct_tac \(x@1\) \texttt{and} \(\dots\) \texttt{and} \(x@n\));
+\end{ttbox}
+
+\begin{exercise}
+  Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that
+  replaces \isa{IF}s with complex boolean conditions by nested
+  \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
+  \isa{Neg} should be eliminated completely. Prove that \isa{norma}
+  preserves the value of an expression and that the result of \isa{norma}
+  is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
+  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
+\end{exercise}
+*}
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/Fundata.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,53 @@
+(*<*)
+theory Fundata = Main:
+(*>*)
+datatype ('a,'i)bigtree = Tip | Branch 'a "'i \\<Rightarrow> ('a,'i)bigtree"
+
+text{*\noindent Parameter \isa{'a} is the type of values stored in
+the \isa{Branch}es of the tree, whereas \isa{'i} is the index
+type over which the tree branches. If \isa{'i} is instantiated to
+\isa{bool}, the result is a binary tree; if it is instantiated to
+\isa{nat}, we have an infinitely branching tree because each node
+has as many subtrees as there are natural numbers. How can we possibly
+write down such a tree? Using functional notation! For example, the *}
+
+term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))";
+
+text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose
+root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
+has merely \isa{Tip}s as further subtrees.
+
+Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:
+*}
+
+consts map_bt :: "('a \\<Rightarrow> 'b) \\<Rightarrow> ('a,'i)bigtree \\<Rightarrow> ('b,'i)bigtree"
+primrec
+"map_bt f Tip          = Tip"
+"map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))"
+
+text{*\noindent This is a valid \isacommand{primrec} definition because the
+recursive calls of \isa{map_bt} involve only subtrees obtained from
+\isa{F}, i.e.\ the left-hand side. Thus termination is assured.  The
+seasoned functional programmer might have written \isa{map_bt~f~o~F} instead
+of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by
+Isabelle because the termination proof is not as obvious since
+\isa{map_bt} is only partially applied.
+
+The following lemma has a canonical proof  *}
+
+lemma "map_bt g (map_bt f T) = map_bt (g o f) T";
+apply(induct_tac "T", auto).
+
+text{*\noindent
+but it is worth taking a look at the proof state after the induction step
+to understand what the presence of the function type entails:
+\begin{isabellepar}%
+~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
+~2.~{\isasymAnd}a~F.\isanewline
+~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
+~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
+\end{isabellepar}%
+*}
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/Nested.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,90 @@
+(*<*)
+theory Nested = Main:;
+(*>*)
+
+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
+where function symbols can be applied to a list of arguments:
+*}
+
+datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
+
+text{*\noindent
+Note that we need to quote \isa{term} on the left to avoid confusion with
+the command \isacommand{term}.
+Parameter \isa{'a} is the type of variables and \isa{'b} the type of
+function symbols.
+A mathematical term like $f(x,g(y))$ becomes \isa{App f [Var x, App g
+  [Var y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
+suitable values, e.g.\ numbers or strings.
+
+What complicates the definition of \isa{term} is the nested occurrence of
+\isa{term} inside \isa{list} on the right-hand side. In principle,
+nested recursion can be eliminated in favour of mutual recursion by unfolding
+the offending datatypes, here \isa{list}. The result for \isa{term}
+would be something like
+\begin{ttbox}
+\input{Datatype/tunfoldeddata}\end{ttbox}
+Although we do not recommend this unfolding to the user, it shows how to
+simulate nested recursion by mutual recursion.
+Now we return to the initial definition of \isa{term} using
+nested recursion.
+
+Let us define a substitution function on terms. Because terms involve term
+lists, we need to define two substitution functions simultaneously:
+*}
+
+consts
+subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term      \\<Rightarrow> ('a,'b)term"
+substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";
+
+primrec
+  "subst s (Var x) = s x"
+  "subst s (App f ts) = App f (substs s ts)"
+
+  "substs s [] = []"
+  "substs s (t # ts) = subst s t # substs s ts";
+
+text{*\noindent
+Similarly, when proving a statement about terms inductively, we need
+to prove a related statement about term lists simultaneously. For example,
+the fact that the identity substitution does not change a term needs to be
+strengthened and proved as follows:
+*}
+
+lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
+        substs Var ts = (ts::('a,'b)term list)";
+apply(induct_tac t and ts, auto).;
+
+text{*\noindent
+Note that \isa{Var} is the identity substitution because by definition it
+leaves variables unchanged: \isa{subst Var (Var $x$) = Var $x$}. Note also
+that the type annotations are necessary because otherwise there is nothing in
+the goal to enforce that both halves of the goal talk about the same type
+parameters \isa{('a,'b)}. As a result, induction would fail
+because the two halves of the goal would be unrelated.
+
+\begin{exercise}
+The fact that substitution distributes over composition can be expressed
+roughly as follows:
+\begin{ttbox}
+subst (f o g) t = subst f (subst g t)
+\end{ttbox}
+Correct this statement (you will find that it does not type-check),
+strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
+its definition is found in theorem \isa{o_def}).
+\end{exercise}
+
+Of course, you may also combine mutual and nested recursion. For example,
+constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
+expressions as its argument: \isa{Sum "'a aexp list"}.
+*}
+(*<*)
+
+lemma "subst s (App f ts) = App f (map (subst s) ts)";
+apply(induct_tac ts, auto).;
+
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,3 @@
+use_thy "ABexpr";
+use_thy "Nested";
+use_thy "Fundata";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Datatype/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,4 @@
+\documentclass{article}
+\begin{document}
+xxx
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,164 @@
+(*<*)
+theory Ifexpr = Main:;
+(*>*)
+
+text{*
+\subsubsection{How can we model boolean expressions?}
+
+We want to represent boolean expressions built up from variables and
+constants by negation and conjunction. The following datatype serves exactly
+that purpose:
+*}
+
+datatype boolex = Const bool | Var nat | Neg boolex
+                | And boolex boolex;
+
+text{*\noindent
+The two constants are represented by \isa{Const~True} and
+\isa{Const~False}. Variables are represented by terms of the form
+\isa{Var~$n$}, where $n$ is a natural number (type \isa{nat}).
+For example, the formula $P@0 \land \neg P@1$ is represented by the term
+\isa{And~(Var~0)~(Neg(Var~1))}.
+
+\subsubsection{What is the value of a boolean expression?}
+
+The value of a boolean expression depends on the value of its variables.
+Hence the function \isa{value} takes an additional parameter, an {\em
+  environment} of type \isa{nat \isasymFun\ bool}, which maps variables to
+their values:
+*}
+
+consts value :: "boolex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
+primrec
+"value (Const b) env = b"
+"value (Var x)   env = env x"
+"value (Neg b)   env = (\\<not> value b env)"
+"value (And b c) env = (value b env \\<and> value c env)";
+
+text{*\noindent
+\subsubsection{If-expressions}
+
+An alternative and often more efficient (because in a certain sense
+canonical) representation are so-called \emph{If-expressions} built up
+from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
+(\isa{IF}):
+*}
+
+datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
+
+text{*\noindent
+The evaluation if If-expressions proceeds as for \isa{boolex}:
+*}
+
+consts valif :: "ifex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
+primrec
+"valif (CIF b)    env = b"
+"valif (VIF x)    env = env x"
+"valif (IF b t e) env = (if valif b env then valif t env
+                                        else valif e env)";
+
+text{*
+\subsubsection{Transformation into and of If-expressions}
+
+The type \isa{boolex} is close to the customary representation of logical
+formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
+translate from \isa{boolex} into \isa{ifex}:
+*}
+
+consts bool2if :: "boolex \\<Rightarrow> ifex";
+primrec
+"bool2if (Const b) = CIF b"
+"bool2if (Var x)   = VIF x"
+"bool2if (Neg b)   = IF (bool2if b) (CIF False) (CIF True)"
+"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)";
+
+text{*\noindent
+At last, we have something we can verify: that \isa{bool2if} preserves the
+value of its argument:
+*}
+
+lemma "valif (bool2if b) env = value b env";
+
+txt{*\noindent
+The proof is canonical:
+*}
+
+apply(induct_tac b);
+apply(auto).;
+
+text{*\noindent
+In fact, all proofs in this case study look exactly like this. Hence we do
+not show them below.
+
+More interesting is the transformation of If-expressions into a normal form
+where the first argument of \isa{IF} cannot be another \isa{IF} but
+must be a constant or variable. Such a normal form can be computed by
+repeatedly replacing a subterm of the form \isa{IF~(IF~b~x~y)~z~u} by
+\isa{IF b (IF x z u) (IF y z u)}, which has the same value. The following
+primitive recursive functions perform this task:
+*}
+
+consts normif :: "ifex \\<Rightarrow> ifex \\<Rightarrow> ifex \\<Rightarrow> ifex";
+primrec
+"normif (CIF b)    t e = IF (CIF b) t e"
+"normif (VIF x)    t e = IF (VIF x) t e"
+"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)";
+
+consts norm :: "ifex \\<Rightarrow> ifex";
+primrec
+"norm (CIF b)    = CIF b"
+"norm (VIF x)    = VIF x"
+"norm (IF b t e) = normif b (norm t) (norm e)";
+
+text{*\noindent
+Their interplay is a bit tricky, and we leave it to the reader to develop an
+intuitive understanding. Fortunately, Isabelle can help us to verify that the
+transformation preserves the value of the expression:
+*}
+
+theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)
+
+text{*\noindent
+The proof is canonical, provided we first show the following simplification
+lemma (which also helps to understand what \isa{normif} does):
+*}
+
+lemma [simp]:
+  "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
+(*<*)
+apply(induct_tac b);
+apply(auto).;
+
+theorem "valif (norm b) env = valif b env";
+apply(induct_tac b);
+apply(auto).;
+(*>*)
+text{*\noindent
+Note that the lemma does not have a name, but is implicitly used in the proof
+of the theorem shown above because of the \isa{[simp]} attribute.
+
+But how can we be sure that \isa{norm} really produces a normal form in
+the above sense? We define a function that tests If-expressions for normality
+*}
+
+consts normal :: "ifex \\<Rightarrow> bool";
+primrec
+"normal(CIF b) = True"
+"normal(VIF x) = True"
+"normal(IF b t e) = (normal t \\<and> normal e \\<and>
+     (case b of CIF b \\<Rightarrow> True | VIF x \\<Rightarrow> True | IF x y z \\<Rightarrow> False))";
+
+text{*\noindent
+and prove \isa{normal(norm b)}. Of course, this requires a lemma about
+normality of \isa{normif}:
+*}
+
+lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*)
+apply(induct_tac b);
+apply(auto).;
+
+theorem "normal(norm b)";
+apply(induct_tac b);
+apply(auto).;
+
+end(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Ifexpr/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,1 @@
+use_thy "Ifexpr";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Ifexpr/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,4 @@
+\documentclass{article}
+\begin{document}
+xxx
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,90 @@
+(*<*)
+theory Itrev = Main:;
+(*>*)
+
+text{*
+We define a tail-recursive version of list-reversal,
+i.e.\ one that can be compiled into a loop:
+*}
+
+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 its first argument by
+stacking its elements onto the second argument, and returning that second
+argument when the first one becomes empty.
+We need to show that \isa{itrev} does indeed reverse its first argument
+provided the second one is empty:
+*}
+
+lemma "itrev xs [] = rev xs";
+
+txt{*\noindent
+There is no choice as to the induction variable, and we immediately simplify:
+*}
+
+apply(induct_tac xs, auto);
+
+txt{*\noindent
+Unfortunately, this is not a complete success:
+\begin{isabellepar}%
+~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
+\end{isabellepar}%
+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:
+\begin{quote}
+{\em 3. 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
+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
+\isa{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
+induction, and we repeat our above proof attempt. Unfortunately, we are still
+not there:
+\begin{isabellepar}%
+~1.~{\isasymAnd}a~list.\isanewline
+~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
+~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
+\end{isabellepar}%
+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
+the subgoal, but the induction hypothesis needs to be applied with
+\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
+for all \isa{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
+leads to another heuristic for generalization:
+\begin{quote}
+{\em 4. 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
+provability of the goal. Because it is not always required, and may even
+complicate matters in some cases, this heuristic is often not
+applied blindly.
+*}
+
+(*<*)
+oops;
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,18 @@
+use_thy "Tree";
+use_thy "cases";
+use_thy "fakenat";
+use_thy "natsum";
+use_thy "arith1";
+use_thy "arith2";
+use_thy "arith3";
+use_thy "arith4";
+use_thy "pairs";
+use_thy "types";
+use_thy "prime_def";
+use_thy "def_rewr";
+use_thy "let_rewr";
+use_thy "cond_rewr";
+use_thy "case_splits";
+use_thy "trace_simp";
+use_thy "Itrev";
+use_thy "asm_simp";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/Tree.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,27 @@
+(*<*)
+theory Tree = Main:
+(*>*)
+
+text{*\noindent
+Define the datatype of binary trees
+*}
+
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
+
+consts mirror :: "'a tree \\<Rightarrow> 'a tree";
+primrec
+"mirror Tip = Tip"
+"mirror (Node l x r) = Node (mirror l) x (mirror r)";(*>*)
+
+text{*\noindent
+and a function \isa{mirror} that mirrors a binary tree
+by swapping subtrees (recursively). Prove
+*}
+
+lemma mirror_mirror: "mirror(mirror t) = t";
+(*<*)
+apply(induct_tac t);
+apply(auto).;
+
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/arith1.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,8 @@
+(*<*)
+theory arith1 = Main:;
+(*>*)
+lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n";
+(**)(*<*)
+apply(auto).;
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/arith2.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,8 @@
+(*<*)
+theory arith2 = Main:;
+(*>*)
+lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
+apply(arith).;
+(**)(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/arith3.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,8 @@
+(*<*)
+theory arith3 = Main:;
+(*>*)
+lemma "n*n = n \\<Longrightarrow> n=0 \\<or> n=1";
+(**)(*<*)
+oops;
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/arith4.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,8 @@
+(*<*)
+theory arith4 = Main:;
+(*>*)
+lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
+(**)(*<*)
+oops;
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/asm_simp.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,49 @@
+(*<*)
+theory asm_simp = Main:;
+
+(*>*)text{*
+By default, assumptions are part of the simplification process: they are used
+as simplification rules and are simplified themselves. For example:
+*}
+
+lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
+apply simp.;
+
+text{*\noindent
+The second assumption simplifies to \isa{xs = []}, which in turn
+simplifies the first assumption to \isa{zs = ys}, thus reducing the
+conclusion to \isa{ys = ys} and hence to \isa{True}.
+
+In some cases this may be too much of a good thing and may lead to
+nontermination:
+*}
+
+lemma "\\<forall>x. f x = g (f (g x)) \\<Longrightarrow> f [] = f [] @ []";
+
+txt{*\noindent
+cannot be solved by an unmodified application of \isa{simp} because the
+simplification rule \isa{f x = g(f(g x))} extracted from the assumption
+does not terminate. Isabelle notices certain simple forms of
+nontermination but not this one. The problem can be circumvented by
+explicitly telling the simplifier to ignore the assumptions:
+*}
+
+apply(simp no_asm:).;
+
+text{*\noindent
+There are three modifiers that influence the treatment of assumptions:
+\begin{description}
+\item[\isaindexbold{no_asm:}] means that assumptions are completely ignored.
+\item[\isaindexbold{no_asm_simp:}] means that the assumptions are not simplified but
+  are used in the simplification of the conclusion.
+\item[\isaindexbold{no_asm_use:}] means that the assumptions are simplified
+but are not
+  used in the simplification of each other or the conclusion.
+\end{description}
+Neither \isa{no_asm_simp:} nor \isa{no_asm_use:} allow to simplify the above
+problematic subgoal.
+
+Note that only one of the above modifiers is allowed, and it must precede all
+other modifiers.
+*}
+(*<*)end(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/case_splits.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,85 @@
+(*<*)
+theory case_splits = Main:;
+(*>*)
+
+text{*
+Goals containing \isaindex{if}-expressions are usually proved by case
+distinction on the condition of the \isa{if}. For example the goal
+*}
+
+lemma "\\<forall>xs. if xs = [] then rev xs = [] else rev xs \\<noteq> []";
+
+txt{*\noindent
+can be split into
+\begin{isabellepar}%
+~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%
+\end{isabellepar}%
+by a degenerate form of simplification
+*}
+
+apply(simp only: split: split_if);
+(*<*)oops;(*>*)
+
+text{*\noindent
+where no simplification rules are included (\isa{only:} is followed by the
+empty list of theorems) but the rule \isaindexbold{split_if} for
+splitting \isa{if}s is added (via the modifier \isa{split:}). Because
+case-splitting on \isa{if}s is almost always the right proof strategy, the
+simplifier performs it automatically. Try \isacommand{apply}\isa{(simp)}
+on the initial goal above.
+
+This splitting idea generalizes from \isa{if} to \isaindex{case}:
+*}
+
+lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
+txt{*\noindent
+becomes
+\begin{isabellepar}%
+~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
+~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%
+\end{isabellepar}%
+by typing
+*}
+
+apply(simp only: split: list.split);
+(*<*)oops;(*>*)
+
+text{*\noindent
+In contrast to \isa{if}-expressions, the simplifier does not split
+\isa{case}-expressions by default because this can lead to nontermination
+in case of recursive datatypes. Again, if the \isa{only:} modifier is
+dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)}
+alone will not do:
+*}
+(*<*)
+lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
+(*>*)
+apply(simp split: list.split).;
+
+text{*
+In general, every datatype $t$ comes with a theorem
+\isa{$t$.split} which can be declared to be a \bfindex{split rule} either
+locally as above, or by giving it the \isa{split} attribute globally:
+*}
+
+theorems [split] = list.split;
+
+text{*\noindent
+The \isa{split} attribute can be removed with the \isa{del} modifier,
+either locally
+*}
+(*<*)
+lemma "dummy=dummy";
+(*>*)
+apply(simp split del: split_if);
+(*<*)
+oops;
+(*>*)
+text{*\noindent
+or globally:
+*}
+theorems [split del] = list.split;
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/cases.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,19 @@
+(*<*)
+theory "cases" = Main:;
+(*>*)
+
+lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
+apply(case_tac xs);
+
+txt{*
+\begin{isabellepar}%
+~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
+~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
+\end{isabellepar}%
+*}
+
+apply(auto).;
+(**)
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/cond_rewr.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,35 @@
+(*<*)
+theory cond_rewr = Main:;
+(*>*)
+
+text{*
+So far all examples of rewrite rules were equations. The simplifier also
+accepts \emph{conditional} equations, for example
+*}
+
+lemma hd_Cons_tl[simp]: "xs \\<noteq> []  \\<Longrightarrow>  hd xs # tl xs = xs";
+apply(case_tac xs, simp, simp).;
+
+text{*\noindent
+Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
+sequence of methods. Assuming that the simplification rule
+*}(*<*)term(*>*) "(rev xs = []) = (xs = [])";
+text{*\noindent
+is present as well,
+*}
+
+lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
+(*<*)
+apply(simp).
+(*>*)
+text{*\noindent
+is proved by simplification:
+the conditional equation \isa{hd_Cons_tl} above
+can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs}
+because the corresponding precondition \isa{rev xs \isasymnoteq\ []}
+simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local
+assumption of the subgoal.
+*}
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/consts.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,5 @@
+(*<*)theory "consts" = Main:;
+(*>*)consts nand :: gate
+            exor :: gate(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/def_rewr.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,46 @@
+(*<*)
+theory def_rewr = Main:;
+
+(*>*)text{*\noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
+be used as simplification rules, but by default they are not.  Hence the
+simplifier does not expand them automatically, just as it should be:
+definitions are introduced for the purpose of abbreviating complex
+concepts. Of course we need to expand the definitions initially to derive
+enough lemmas that characterize the concept sufficiently for us to forget the
+original definition. For example, given
+*}
+
+constdefs exor :: "bool \\<Rightarrow> bool \\<Rightarrow> bool"
+         "exor A B \\<equiv> (A \\<and> \\<not>B) \\<or> (\\<not>A \\<and> B)";
+
+text{*\noindent
+we may want to prove
+*}
+
+lemma "exor A (\\<not>A)";
+
+txt{*\noindent
+There is a special method for \emph{unfolding} definitions, which we need to
+get started:\indexbold{*unfold}\indexbold{definition!unfolding}
+*}
+
+apply(unfold exor_def);
+
+txt{*\noindent
+It unfolds the given list of definitions (here merely one) in all subgoals:
+\begin{isabellepar}%
+~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
+\end{isabellepar}%
+The resulting goal can be proved by simplification.
+
+In case we want to expand a definition in the middle of a proof, we can
+simply include it locally:*}(*<*)oops;lemma "exor A (\\<not>A)";(*>*)
+apply(simp add: exor_def);(*<*).(*>*)
+
+text{*\noindent
+In fact, this one command proves the above lemma directly.
+
+You should normally not turn a definition permanently into a simplification
+rule because this defeats the whole purpose of an abbreviation.
+*}
+(*<*)end(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,4 @@
+\documentclass{article}
+\begin{document}
+xxx
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/fakenat.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,13 @@
+(*<*)
+theory fakenat = Main:;
+(*>*)
+
+text{*\noindent
+The type \isaindexbold{nat} of natural numbers is predefined and
+behaves like
+*}
+
+datatype nat = "0" | Suc nat
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/let_rewr.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,14 @@
+(*<*)
+theory let_rewr = Main:;
+(*>*)
+lemma "(let xs = [] in xs@ys@xs) = ys";
+apply(simp add: Let_def).;
+
+text{*
+If, in a particular context, there is no danger of a combinatorial explosion
+of nested \texttt{let}s one could even add \texttt{Let_def} permanently:
+*}
+theorems [simp] = Let_def;
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,28 @@
+(*<*)
+theory natsum = Main:;
+(*>*)
+text{*\noindent
+In particular, there are \isa{case}-expressions, for example
+*}
+
+(*<*)term(*>*) "case n of 0 \\<Rightarrow> 0 | Suc m \\<Rightarrow> m";
+
+text{*\noindent
+primitive recursion, for example
+*}
+
+consts sum :: "nat \\<Rightarrow> nat";
+primrec "sum 0 = 0"
+        "sum (Suc n) = Suc n + sum n";
+
+text{*\noindent
+and induction, for example
+*}
+
+lemma "sum n + sum n = n*(Suc n)";
+apply(induct_tac n);
+apply(auto).;
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/pairs.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,8 @@
+(*<*)
+theory pairs = Main:;
+term(*>*) "let (x,y) = f z in (y,x)";
+(*<*)
+term(*>*) "case xs of [] \\<Rightarrow> 0 | (x,y)#zs \\<Rightarrow> x+y"
+(**)(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/prime_def.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,18 @@
+(*<*)
+theory prime_def = Main:;
+consts prime :: "nat \\<Rightarrow> bool"
+(*>*)
+(*<*)term(*>*)
+
+    "prime(p) \\<equiv> 1 < p \\<and> ((m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))";
+text{*\noindent\small
+where \isa{dvd} means ``divides''.
+Isabelle rejects this ``definition'' because of the extra \isa{m} on the
+right-hand side, which would introduce an inconsistency. (Why?) What you
+should have written is
+*}
+(*<*)term(*>*)
+ "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/trace_simp.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,46 @@
+(*<*)
+theory trace_simp = Main:;
+(*>*)
+
+text{*
+Using the simplifier effectively may take a bit of experimentation.  Set the
+\ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
+on:
+*}
+ML "set trace_simp";
+lemma "rev [a] = []";
+apply(simp);
+
+txt{*\noindent
+produces the trace
+
+\begin{ttbox}
+Applying instance of rewrite rule:
+rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
+Rewriting:
+rev [x] == rev [] @ [x]
+Applying instance of rewrite rule:
+rev [] == []
+Rewriting:
+rev [] == []
+Applying instance of rewrite rule:
+[] @ ?y == ?y
+Rewriting:
+[] @ [x] == [x]
+Applying instance of rewrite rule:
+?x3 \# ?t3 = ?t3 == False
+Rewriting:
+[x] = [] == False
+\end{ttbox}
+
+In more complicated cases, the trace can quite lenghty, especially since
+invocations of the simplifier are often nested (e.g.\ when solving conditions
+of rewrite rules). Thus it is advisable to reset it:
+*}
+
+ML "reset trace_simp";
+
+(*<*)
+oops;
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/types.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,46 @@
+(*<*)
+theory "types" = Main:;
+(*>*)types number       = nat
+      gate         = "bool \\<Rightarrow> bool \\<Rightarrow> bool"
+      ('a,'b)alist = "('a * 'b)list";
+
+text{*\noindent\indexbold{*types}%
+Internally all synonyms are fully expanded.  As a consequence Isabelle's
+output never contains synonyms.  Their main purpose is to improve the
+readability of theory definitions.  Synonyms can be used just like any other
+type:
+*}
+
+consts nand :: gate
+       exor :: gate;
+
+text{*
+\subsection{Constant definitions}
+\label{sec:ConstDefinitions}
+\indexbold{definition}
+
+The above constants \isa{nand} and \isa{exor} are non-recursive and can
+therefore be defined directly by
+*}
+
+defs nand_def: "nand A B \\<equiv> \\<not>(A \\<and> B)"
+     exor_def: "exor A B \\<equiv> A \\<and> \\<not>B \\<or> \\<not>A \\<and> B";
+
+text{*\noindent%
+where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
+\isa{exor_def} are arbitrary user-supplied names.
+The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
+that should only be used in constant definitions.
+Declarations and definitions can also be merged
+*}
+
+constdefs nor :: gate
+         "nor A B \\<equiv> \\<not>(A \\<or> B)"
+          exor2 :: gate
+         "exor2 A B \\<equiv> (A \\<or> B) \\<and> (\\<not>A \\<or> \\<not>B)";
+
+text{*\noindent\indexbold{*constdefs}%
+in which case the default name of each definition is \isa{$f$_def}, where
+$f$ is the name of the defined constant.*}(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/Induction.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,74 @@
+(*<*)
+theory Induction = examples + simplification:;
+(*>*)
+
+text{*
+Assuming we have defined our function such that Isabelle could prove
+termination and that the recursion equations (or some suitable derived
+equations) are simplification rules, we might like to prove something about
+our function. Since the function is recursive, the natural proof principle is
+again induction. But this time the structural form of induction that comes
+with datatypes is unlikely to work well---otherwise we could have defined the
+function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
+proves a suitable induction rule $f$\isa{.induct} that follows the
+recursion pattern of the particular function $f$. We call this
+\textbf{recursion induction}. Roughly speaking, it
+requires you to prove for each \isacommand{recdef} equation that the property
+you are trying to establish holds for the left-hand side provided it holds
+for all recursive calls on the right-hand side. Here is a simple example:
+*}
+
+lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
+
+txt{*\noindent
+involving the predefined \isa{map} functional on lists: \isa{map f xs}
+is the result of applying \isa{f} to all elements of \isa{xs}. We prove
+this lemma by recursion induction w.r.t. \isa{sep}:
+*}
+
+apply(induct_tac x xs rule: sep.induct);
+
+txt{*\noindent
+The resulting proof state has three subgoals corresponding to the three
+clauses for \isa{sep}:
+\begin{isabellepar}%
+~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
+~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
+~3.~{\isasymAnd}a~x~y~zs.\isanewline
+~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
+~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
+\end{isabellepar}%
+The rest is pure simplification:
+*}
+
+apply auto.;
+
+text{*
+Try proving the above lemma by structural induction, and you find that you
+need an additional case distinction. What is worse, the names of variables
+are invented by Isabelle and have nothing to do with the names in the
+definition of \isa{sep}.
+
+In general, the format of invoking recursion induction is
+\begin{ttbox}
+apply(induct_tac \(x@1 \dots x@n\) rule: \(f\).induct)
+\end{ttbox}\index{*induct_tac}%
+where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
+name of a function that takes an $n$-tuple. Usually the subgoal will
+contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
+induction rules do not mention $f$ at all. For example \isa{sep.induct}
+\begin{isabellepar}%
+{\isasymlbrakk}~{\isasymAnd}a.~?P~a~[];\isanewline
+~~{\isasymAnd}a~x.~?P~a~[x];\isanewline
+~~{\isasymAnd}a~x~y~zs.~?P~a~(y~\#~zs)~{\isasymLongrightarrow}~?P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
+{\isasymLongrightarrow}~?P~?u~?v%
+\end{isabellepar}%
+merely says that in order to prove a property \isa{?P} of \isa{?u} and
+\isa{?v} you need to prove it for the three cases where \isa{?v} is the
+empty list, the singleton list, and the list with at least two elements
+(in which case you may assume it holds for the tail of that list).
+*}
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,2 @@
+use_thy "termination";
+use_thy "Induction";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,4 @@
+\documentclass{article}
+\begin{document}
+xxx
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/examples.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,92 @@
+(*<*)
+theory examples = Main:;
+(*>*)
+
+text{*
+Here is a simple example, the Fibonacci function:
+*}
+
+consts fib :: "nat \\<Rightarrow> nat";
+recdef fib "measure(\\<lambda>n. n)"
+  "fib 0 = 0"
+  "fib 1 = 1"
+  "fib (Suc(Suc x)) = fib x + fib (Suc x)";
+
+text{*\noindent
+The definition of \isa{fib} is accompanied by a \bfindex{measure function}
+\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
+natural number. The requirement is that in each equation the measure of the
+argument on the left-hand side is strictly greater than the measure of the
+argument of each recursive call. In the case of \isa{fib} this is
+obviously true because the measure function is the identity and
+\isa{Suc(Suc~x)} is strictly greater than both \isa{x} and
+\isa{Suc~x}.
+
+Slightly more interesting is the insertion of a fixed element
+between any two elements of a list:
+*}
+
+consts sep :: "'a * 'a list \\<Rightarrow> 'a list";
+recdef sep "measure (\\<lambda>(a,xs). length xs)"
+  "sep(a, [])     = []"
+  "sep(a, [x])    = [x]"
+  "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
+
+text{*\noindent
+This time the measure is the length of the list, which decreases with the
+recursive call; the first component of the argument tuple is irrelevant.
+
+Pattern matching need not be exhaustive:
+*}
+
+consts last :: "'a list \\<Rightarrow> 'a";
+recdef last "measure (\\<lambda>xs. length xs)"
+  "last [x]      = x"
+  "last (x#y#zs) = last (y#zs)";
+
+text{*
+Overlapping patterns are disambiguated by taking the order of equations into
+account, just as in functional programming:
+*}
+
+consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";
+recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
+  "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
+  "sep1(a, xs)     = xs";
+
+text{*\noindent
+This defines exactly the same function as \isa{sep} above, i.e.\
+\isa{sep1 = sep}.
+
+\begin{warn}
+  \isacommand{recdef} only takes the first argument of a (curried)
+  recursive function into account. This means both the termination measure
+  and pattern matching can only use that first argument. In general, you will
+  therefore have to combine several arguments into a tuple. In case only one
+  argument is relevant for termination, you can also rearrange the order of
+  arguments as in the following definition:
+\end{warn}
+*}
+consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";
+recdef sep2 "measure length"
+  "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"
+  "sep2 xs       = (\\<lambda>a. xs)";
+
+text{*
+Because of its pattern-matching syntax, \isacommand{recdef} is also useful
+for the definition of non-recursive functions:
+*}
+
+consts swap12 :: "'a list \\<Rightarrow> 'a list";
+recdef swap12 "{}"
+  "swap12 (x#y#zs) = y#x#zs"
+  "swap12 zs       = zs";
+
+text{*\noindent
+In the non-recursive case the termination measure degenerates to the empty
+set \isa{\{\}}.
+*}
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,105 @@
+(*<*)
+theory simplification = Main:;
+(*>*)
+
+text{*
+Once we have succeeded in proving all termination conditions, the recursion
+equations become simplification rules, just as with
+\isacommand{primrec}. In most cases this works fine, but there is a subtle
+problem that must be mentioned: simplification may not
+terminate because of automatic splitting of \isa{if}.
+Let us look at an example:
+*}
+
+consts gcd :: "nat*nat \\<Rightarrow> nat";
+recdef gcd "measure (\\<lambda>(m,n).n)"
+  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
+
+text{*\noindent
+According to the measure function, the second argument should decrease with
+each recursive call. The resulting termination condition
+*}
+
+(*<*)term(*>*) "n \\<noteq> 0 \\<Longrightarrow> m mod n < n";
+
+text{*\noindent
+is provded automatically because it is already present as a lemma in the
+arithmetic library. Thus the recursion equation becomes a simplification
+rule. Of course the equation is nonterminating if we are allowed to unfold
+the recursive call inside the \isa{else} branch, which is why programming
+languages and our simplifier don't do that. Unfortunately the simplifier does
+something else which leads to the same problem: it splits \isa{if}s if the
+condition simplifies to neither \isa{True} nor \isa{False}. For
+example, simplification reduces
+*}
+
+(*<*)term(*>*) "gcd(m,n) = k";
+
+text{*\noindent
+in one step to
+*}
+
+(*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k";
+
+text{*\noindent
+where the condition cannot be reduced further, and splitting leads to
+*}
+
+(*<*)term(*>*) "(n=0 \\<longrightarrow> m=k) \\<and> (n\\<noteq>0 \\<longrightarrow> gcd(n, m mod n)=k)";
+
+text{*\noindent
+Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
+an \isa{if}, this leads to an infinite chain of simplification steps.
+Fortunately, this problem can be avoided in many different ways.
+
+Of course the most radical solution is to disable the offending
+\isa{split_if} as shown in the section on case splits in
+\S\ref{sec:SimpFeatures}.
+However, we do not recommend this because it means you will often have to
+invoke the rule explicitly when \isa{if} is involved.
+
+If possible, the definition should be given by pattern matching on the left
+rather than \isa{if} on the right. In the case of \isa{gcd} the
+following alternative definition suggests itself:
+*}
+
+consts gcd1 :: "nat*nat \\<Rightarrow> nat";
+recdef gcd1 "measure (\\<lambda>(m,n).n)"
+  "gcd1 (m, 0) = m"
+  "gcd1 (m, n) = gcd1(n, m mod n)";
+
+
+text{*\noindent
+Note that the order of equations is important and hides the side condition
+\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
+may not be expressible by pattern matching.
+
+A very simple alternative is to replace \isa{if} by \isa{case}, which
+is also available for \isa{bool} but is not split automatically:
+*}
+
+consts gcd2 :: "nat*nat \\<Rightarrow> nat";
+recdef gcd2 "measure (\\<lambda>(m,n).n)"
+  "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
+
+text{*\noindent
+In fact, this is probably the neatest solution next to pattern matching.
+
+A final alternative is to replace the offending simplification rules by
+derived conditional ones. For \isa{gcd} it means we have to prove
+*}
+
+lemma [simp]: "gcd (m, 0) = m";
+apply(simp).;
+lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
+apply(simp).;
+
+text{*\noindent
+after which we can disable the original simplification rule:
+*}
+
+lemmas [simp del] = gcd.simps;
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Recdef/termination.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,102 @@
+(*<*)
+theory termination = Main:;
+(*>*)
+
+text{*
+When a function is defined via \isacommand{recdef}, Isabelle tries to prove
+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. In that case
+$f$.\isa{simps} contains 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
+simplification rules.
+
+In general, Isabelle may not be able to prove all termination condition
+(there is one for each recursive call) automatically. For example,
+termination of the following artificial function
+*}
+
+consts f :: "nat*nat \\<Rightarrow> nat";
+recdef f "measure(\\<lambda>(x,y). x-y)"
+  "f(x,y) = (if x \\<le> y then x else f(x,y+1))";
+
+text{*\noindent
+is not proved automatically (although maybe it should be). Isabelle prints a
+kind of error message showing you what it was unable to prove. You will then
+have to prove it as a separate lemma before you attempt the definition
+of your function once more. In our case the required lemma is the obvious one:
+*}
+
+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:
+*}
+
+apply(arith).;
+
+text{*\noindent
+Because \isacommand{recdef}'s the termination prover involves simplification,
+we have declared our lemma a simplification rule. Therefore our second
+attempt to define our function will automatically take it into account:
+*}
+
+consts g :: "nat*nat \\<Rightarrow> nat";
+recdef g "measure(\\<lambda>(x,y). x-y)"
+  "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
+rules. Thus we can automatically prove
+*}
+
+theorem wow: "g(1,0) = g(1,1)";
+apply(simp).;
+
+text{*\noindent
+More exciting theorems require induction, which is discussed below.
+
+Because lemma \isa{termi_lem} above was only turned into a
+simplification rule for the sake of the termination proof, we may want to
+disable it again:
+*}
+
+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
+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
+%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*>}:
+*}
+
+consts ack :: "nat*nat \\<Rightarrow> nat";
+recdef ack "measure(%m. m) <*lex*> measure(%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))";
+
+text{*\noindent
+For details see the manual~\cite{isabelle-HOL} and the examples in the
+library.
+*}
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/ToyList/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,2 @@
+use_thy "ToyList";
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,354 @@
+theory ToyList = PreList:
+
+text{*\noindent
+HOL already has a predefined theory of lists called \texttt{List} ---
+\texttt{ToyList} is merely a small fragment of it chosen as an example. In
+contrast to what is recommended in \S\ref{sec:Basic:Theories},
+\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a
+theory that contains pretty much everything but lists, thus avoiding
+ambiguities caused by defining lists twice.
+*}
+
+datatype 'a list = Nil                          ("[]")
+                 | Cons 'a "'a list"            (infixr "#" 65);
+
+text{*\noindent
+The datatype\index{*datatype} \isaindexbold{list} introduces two
+constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
+empty list and the operator that adds an element to the front of a list. For
+example, the term \isa{Cons True (Cons   False Nil)} is a value of type
+\isa{bool~list}, namely the list with the elements \isa{True} and
+\isa{False}. Because this notation becomes unwieldy very quickly, the
+datatype declaration is annotated with an alternative syntax: instead of
+\isa{Nil} and \isa{Cons~$x$~$xs$} we can write
+\isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
+\isa{$x$~\#~$xs$}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
+alternative syntax is the standard syntax. Thus the list \isa{Cons True
+(Cons False Nil)} becomes \isa{True \# False \# []}. The annotation
+\isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
+the right, i.e.\ the term \isa{$x$ \# $y$ \# $z$} is read as \isa{$x$
+\# ($y$ \# $z$)} and not as \isa{($x$ \# $y$) \# $z$}.
+
+\begin{warn}
+  Syntax annotations are a powerful but completely optional feature. You
+  could drop them from theory \texttt{ToyList} and go back to the identifiers
+  \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
+  that their syntax is highly customized. We recommend that novices should
+  not use syntax annotations in their own theories.
+\end{warn}
+Next, two functions \isa{app} and \isaindexbold{rev} are declared:
+*}
+
+consts app :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list"   (infixr "@" 65)
+       rev :: "'a list \\<Rightarrow> 'a list";
+
+text{*
+\noindent
+In contrast to ML, Isabelle insists on explicit declarations of all functions
+(keyword \isacommand{consts}).  (Apart from the declaration-before-use
+restriction, the order of items in a theory file is unconstrained.) Function
+\isa{app} is annotated with concrete syntax too. Instead of the prefix
+syntax \isa{app~$xs$~$ys$} the infix
+\isa{$xs$~\at~$ys$}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
+form. Both functions are defined recursively:
+*}
+
+primrec
+"[] @ ys       = ys"
+"(x # xs) @ ys = x # (xs @ ys)";
+
+primrec
+"rev []        = []"
+"rev (x # xs)  = (rev xs) @ (x # [])";
+
+text{*
+\noindent
+The equations for \isa{app} and \isa{rev} hardly need comments:
+\isa{app} appends two lists and \isa{rev} reverses a list.  The keyword
+\isacommand{primrec}\index{*primrec} indicates that the recursion is of a
+particularly primitive kind where each recursive call peels off a datatype
+constructor from one of the arguments (see \S\ref{sec:datatype}).  Thus the
+recursion always terminates, i.e.\ the function is \bfindex{total}.
+
+The termination requirement is absolutely essential in HOL, a logic of total
+functions. If we were to drop it, inconsistencies would quickly arise: the
+``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
+$f(n)$ on both sides.
+% However, this is a subtle issue that we cannot discuss here further.
+
+\begin{warn}
+  As we have indicated, the desire for total functions is not a gratuitously
+  imposed restriction but an essential characteristic of HOL. It is only
+  because of totality that reasoning in HOL is comparatively easy.  More
+  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
+  function definitions whose totality has not been proved) because they
+  quickly lead to inconsistencies. Instead, fixed constructs for introducing
+  types and functions are offered (such as \isacommand{datatype} and
+  \isacommand{primrec}) which are guaranteed to preserve consistency.
+\end{warn}
+
+A remark about syntax.  The textual definition of a theory follows a fixed
+syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
+Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
+Embedded in this syntax are the types and formulae of HOL, whose syntax is
+extensible, e.g.\ by new user-defined infix operators
+(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
+HOL-specific (terms and types) should be enclosed in
+\texttt{"}\dots\texttt{"}. 
+To lessen this burden, quotation marks around a single identifier can be
+dropped, unless the identifier happens to be a keyword, as in
+*}
+
+consts "end" :: "'a list \\<Rightarrow> 'a"
+
+text{*\noindent
+When Isabelle prints a syntax error message, it refers to the HOL syntax as
+the \bfindex{inner syntax}.
+
+
+\section{An introductory proof}
+\label{sec:intro-proof}
+
+Assuming you have input the declarations and definitions of \texttt{ToyList}
+presented so far, we are ready to prove a few simple theorems. This will
+illustrate not just the basic proof commands but also the typical proof
+process.
+
+\subsubsection*{Main goal: \texttt{rev(rev xs) = xs}}
+
+Our goal is to show that reversing a list twice produces the original
+list. The input line
+*}
+
+theorem rev_rev [simp]: "rev(rev xs) = xs";
+
+txt{*\noindent\index{*theorem|bold}\index{*simp (attribute)|bold}
+\begin{itemize}
+\item
+establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
+\item
+gives that theorem the name \isa{rev_rev} by which it can be referred to,
+\item
+and tells Isabelle (via \isa{[simp]}) to use the theorem (once it has been
+proved) as a simplification rule, i.e.\ all future proofs involving
+simplification will replace occurrences of \isa{rev(rev xs)} by
+\isa{xs}.
+
+The name and the simplification attribute are optional.
+\end{itemize}
+Isabelle's response is to print
+\begin{isabellepar}%
+proof(prove):~step~0\isanewline
+\isanewline
+goal~(theorem~rev\_rev):\isanewline
+rev~(rev~xs)~=~xs\isanewline
+~1.~rev~(rev~xs)~=~xs
+\end{isabellepar}%
+The first three lines tell us that we are 0 steps into the proof of
+theorem \isa{rev_rev}; for compactness reasons we rarely show these
+initial lines in this tutorial. The remaining lines display the current
+proof state.
+Until we have finished a proof, the proof state always looks like this:
+\begin{isabellepar}%
+$G$\isanewline
+~1.~$G\sb{1}$\isanewline
+~~\vdots~~\isanewline
+~$n$.~$G\sb{n}$
+\end{isabellepar}%
+where $G$
+is the overall goal that we are trying to prove, and the numbered lines
+contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
+establish $G$. At \isa{step 0} there is only one subgoal, which is
+identical with the overall goal.  Normally $G$ is constant and only serves as
+a reminder. Hence we rarely show it in this tutorial.
+
+Let us now get back to \isa{rev(rev xs) = xs}. Properties of recursively
+defined functions are best established by induction. In this case there is
+not much choice except to induct on \isa{xs}:
+*}
+
+apply(induct_tac xs);
+
+txt{*\noindent\index{*induct_tac}%
+This tells Isabelle to perform induction on variable \isa{xs}. The suffix
+\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
+By default, induction acts on the first subgoal. The new proof state contains
+two subgoals, namely the base case (\isa{Nil}) and the induction step
+(\isa{Cons}):
+\begin{isabellepar}%
+~1.~rev~(rev~[])~=~[]\isanewline
+~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list%
+\end{isabellepar}%
+
+The induction step is an example of the general format of a subgoal:
+\begin{isabellepar}%
+~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
+\end{isabellepar}%
+The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
+ignored most of the time, or simply treated as a list of variables local to
+this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
+The {\it assumptions} are the local assumptions for this subgoal and {\it
+  conclusion} is the actual proposition to be proved. Typical proof steps
+that add new assumptions are induction or case distinction. In our example
+the only assumption is the induction hypothesis \isa{rev (rev list) =
+  list}, where \isa{list} is a variable name chosen by Isabelle. If there
+are multiple assumptions, they are enclosed in the bracket pair
+\indexboldpos{\isasymlbrakk}{$Isabrl} and
+\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
+
+%FIXME indent!
+Let us try to solve both goals automatically:
+*}
+
+apply(auto);
+
+txt{*\noindent
+This command tells Isabelle to apply a proof strategy called
+\isa{auto} to all subgoals. Essentially, \isa{auto} tries to
+``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
+to the equation \isa{rev [] = []}) and disappears; the simplified version
+of subgoal~2 becomes the new subgoal~1:
+\begin{isabellepar}%
+~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
+\end{isabellepar}%
+In order to simplify this subgoal further, a lemma suggests itself.
+*}
+(*<*)
+oops
+(*>*)
+
+text{*
+\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
+
+After abandoning the above proof attempt (at the shell level type
+\isa{oops}) we start a new proof:
+*}
+
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
+
+txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
+\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
+the importance we attach to a proposition. In general, we use the words
+\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
+interchangeably.
+
+%FIXME indent!
+There are two variables that we could induct on: \isa{xs} and
+\isa{ys}. Because \isa{\at} is defined by recursion on
+the first argument, \isa{xs} is the correct one:
+*}
+
+apply(induct_tac xs);
+
+txt{*\noindent
+This time not even the base case is solved automatically:
+*}
+
+apply(auto);
+
+txt{*
+\begin{isabellepar}%
+~1.~rev~ys~=~rev~ys~@~[]\isanewline
+~2. \dots
+\end{isabellepar}%
+We need to cancel this proof attempt and prove another simple lemma first.
+In the future the step of cancelling an incomplete proof before embarking on
+the proof of a lemma often remains implicit.
+*}
+(*<*)
+oops
+(*>*)
+
+text{*
+\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}}
+
+This time the canonical proof procedure
+*}
+
+lemma app_Nil2 [simp]: "xs @ [] = xs";
+apply(induct_tac xs);
+apply(auto);
+
+txt{*
+\noindent
+leads to the desired message \isa{No subgoals!}:
+\begin{isabellepar}%
+xs~@~[]~=~xs\isanewline
+No~subgoals!
+\end{isabellepar}%
+
+We still need to confirm that the proof is now finished:
+*}
+
+.
+
+text{*\noindent\indexbold{$Isar@\texttt{.}}%
+As a result of that final dot, Isabelle associates the lemma
+just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
+printed out after the final dot) the free variable \isa{xs} has been
+replaced by the unknown \isa{?xs}, just as explained in
+\S\ref{sec:variables}.
+
+Going back to the proof of the first lemma
+*}
+
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
+apply(induct_tac xs);
+apply(auto);
+
+txt{*
+\noindent
+we find that this time \isa{auto} solves the base case, but the
+induction step merely simplifies to
+\begin{isabellepar}
+~1.~{\isasymAnd}a~list.\isanewline
+~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
+~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
+\end{isabellepar}%
+Now we need to remember that \isa{\at} associates to the right, and that
+\isa{\#} and \isa{\at} have the same priority (namely the \isa{65}
+in their \isacommand{infixr} annotation). Thus the conclusion really is
+\begin{isabellepar}%
+~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))%
+\end{isabellepar}%
+and the missing lemma is associativity of \isa{\at}.
+
+\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
+
+Abandoning the previous proof, the canonical proof procedure
+*}
+
+
+txt_raw{*\begin{comment}*}
+oops
+text_raw{*\end{comment}*}
+
+lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
+apply(induct_tac xs);
+apply(auto).;
+
+text{*
+\noindent
+succeeds without further ado.
+
+Now we can go back and prove the first lemma
+*}
+
+lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
+apply(induct_tac xs);
+apply(auto).;
+
+text{*\noindent
+and then solve our main theorem:
+*}
+
+theorem rev_rev [simp]: "rev(rev xs) = xs";
+apply(induct_tac xs);
+apply(auto).;
+
+text{*\noindent
+The final \isa{end} tells Isabelle to close the current theory because
+we are finished with its development:
+*}
+
+end

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/ToyList/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,3 @@
+\documentclass{article}
+\begin{document}
+\end{document}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/ToyList2/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,1 @@
+use_thy "ToyList";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Trie/Option2.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,9 @@
+(*<*)
+theory Option2 = Main:;
+(*>*)
+
+datatype 'a option = None | Some 'a
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Trie/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,2 @@
+use_thy "Option2";
+use_thy "Trie";

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Trie/Trie.thy	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,144 @@
+(*<*)
+theory Trie = Main:;
+(*>*)
+
+text{*
+To minimize running time, each node of a trie should contain an array that maps
+letters to subtries. We have chosen a (sometimes) more space efficient
+representation where the subtries are held in an association list, i.e.\ a
+list of (letter,trie) pairs.  Abstracting over the alphabet \isa{'a} and the
+values \isa{'v} we define a trie as follows:
+*}
+
+datatype ('a,'v)trie = Trie  "'v option"  "('a * ('a,'v)trie)list";
+
+text{*\noindent
+The first component is the optional value, the second component the
+association list of subtries.  This is an example of nested recursion involving products,
+which is fine because products are datatypes as well.
+We define two selector functions:
+*}
+
+consts value :: "('a,'v)trie \\<Rightarrow> 'v option"
+       alist :: "('a,'v)trie \\<Rightarrow> ('a * ('a,'v)trie)list";
+primrec "value(Trie ov al) = ov";
+primrec "alist(Trie ov al) = al";
+
+text{*\noindent
+Association lists come with a generic lookup function:
+*}
+
+consts   assoc :: "('key * 'val)list \\<Rightarrow> 'key \\<Rightarrow> 'val option";
+primrec "assoc [] x = None"
+        "assoc (p#ps) x =
+           (let (a,b) = p in if a=x then Some b else assoc ps x)";
+
+text{*
+Now we can define the lookup function for tries. It descends into the trie
+examining the letters of the search string one by one. As
+recursion on lists is simpler than on tries, let us express this as primitive
+recursion on the search string argument:
+*}
+
+consts   lookup :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v option";
+primrec "lookup t [] = value t"
+        "lookup t (a#as) = (case assoc (alist t) a of
+                              None \\<Rightarrow> None
+                            | Some at \\<Rightarrow> lookup at as)";
+
+text{*
+As a first simple property we prove that looking up a string in the empty
+trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
+distinguishes the two cases whether the search string is empty or not:
+*}
+
+lemma [simp]: "lookup (Trie None []) as = None";
+apply(cases "as", auto).;
+
+text{*
+Things begin to get interesting with the definition of an update function
+that adds a new (string,value) pair to a trie, overwriting the old value
+associated with that string:
+*}
+
+consts update :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v \\<Rightarrow> ('a,'v)trie";
+primrec
+  "update t []     v = Trie (Some v) (alist t)"
+  "update t (a#as) v =
+     (let tt = (case assoc (alist t) a of
+                  None \\<Rightarrow> Trie None [] | Some at \\<Rightarrow> at)
+      in Trie (value t) ((a,update tt as v)#alist t))";
+
+text{*\noindent
+The base case is obvious. In the recursive case the subtrie
+\isa{tt} associated with the first letter \isa{a} is extracted,
+recursively updated, and then placed in front of the association list.
+The old subtrie associated with \isa{a} is still in the association list
+but no longer accessible via \isa{assoc}. Clearly, there is room here for
+optimizations!
+
+Before we start on any proofs about \isa{update} we tell the simplifier to
+expand all \isa{let}s and to split all \isa{case}-constructs over
+options:
+*}
+
+theorems [simp] = Let_def;
+theorems [split] = option.split;
+
+text{*\noindent
+The reason becomes clear when looking (probably after a failed proof
+attempt) at the body of \isa{update}: it contains both
+\isa{let} and a case distinction over type \isa{option}.
+
+Our main goal is to prove the correct interaction of \isa{update} and
+\isa{lookup}:
+*}
+
+theorem "\\<forall>t v bs. lookup (update t as v) bs =
+                    (if as=bs then Some v else lookup t bs)";
+
+txt{*\noindent
+Our plan is to induct on \isa{as}; hence the remaining variables are
+quantified. From the definitions it is clear that induction on either
+\isa{as} or \isa{bs} is required. The choice of \isa{as} is merely
+guided by the intuition that simplification of \isa{lookup} might be easier
+if \isa{update} has already been simplified, which can only happen if
+\isa{as} is instantiated.
+The start of the proof is completely conventional:
+*}
+
+apply(induct_tac "as", auto);
+
+txt{*\noindent
+Unfortunately, this time we are left with three intimidating looking subgoals:
+\begin{isabellepar}%
+~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
+~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
+~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
+\end{isabellepar}%
+Clearly, if we want to make headway we have to instantiate \isa{bs} as
+well now. It turns out that instead of induction, case distinction
+suffices:
+*}
+
+apply(case_tac[!] bs);
+apply(auto).;
+
+text{*\noindent
+Both \isaindex{case_tac} and \isaindex{induct_tac}
+take an optional first argument that specifies the range of subgoals they are
+applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual
+subgoal number are also allowed.
+
+This proof may look surprisingly straightforward. However, note that this
+comes at a cost: the proof script is unreadable because the
+intermediate proof states are invisible, and we rely on the (possibly
+brittle) magic of \isa{auto} (after the induction) to split the remaining
+goals up in such a way that case distinction on \isa{bs} makes sense and
+solves the proof. Part~\ref{Isar} shows you how to write readable and stable
+proofs.
+*}
+
+(*<*)
+end
+(*>*)

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Trie/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
@@ -0,0 +1,4 @@
+\documentclass{article}
+\begin{document}
+xxx
+\end{document}