I wonder which files i forgot.
authornipkow
Wed Apr 19 11:56:31 2000 +0200 (2000-04-19)
changeset 874513b32661dde4
parent 8744 22fa8b16c3ae
child 8746 ccbb5e0dccdf
I wonder which files i forgot.
doc-src/TutorialI/Datatype/ABexpr.thy
doc-src/TutorialI/Datatype/Fundata.thy
doc-src/TutorialI/Datatype/Nested.thy
doc-src/TutorialI/Datatype/ROOT.ML
doc-src/TutorialI/Datatype/document/root.tex
doc-src/TutorialI/Ifexpr/Ifexpr.thy
doc-src/TutorialI/Ifexpr/ROOT.ML
doc-src/TutorialI/Ifexpr/document/root.tex
doc-src/TutorialI/Misc/Itrev.thy
doc-src/TutorialI/Misc/ROOT.ML
doc-src/TutorialI/Misc/Tree.thy
doc-src/TutorialI/Misc/arith1.thy
doc-src/TutorialI/Misc/arith2.thy
doc-src/TutorialI/Misc/arith3.thy
doc-src/TutorialI/Misc/arith4.thy
doc-src/TutorialI/Misc/asm_simp.thy
doc-src/TutorialI/Misc/case_splits.thy
doc-src/TutorialI/Misc/cases.thy
doc-src/TutorialI/Misc/cond_rewr.thy
doc-src/TutorialI/Misc/consts.thy
doc-src/TutorialI/Misc/def_rewr.thy
doc-src/TutorialI/Misc/document/root.tex
doc-src/TutorialI/Misc/fakenat.thy
doc-src/TutorialI/Misc/let_rewr.thy
doc-src/TutorialI/Misc/natsum.thy
doc-src/TutorialI/Misc/pairs.thy
doc-src/TutorialI/Misc/prime_def.thy
doc-src/TutorialI/Misc/trace_simp.thy
doc-src/TutorialI/Misc/types.thy
doc-src/TutorialI/Recdef/Induction.thy
doc-src/TutorialI/Recdef/ROOT.ML
doc-src/TutorialI/Recdef/document/root.tex
doc-src/TutorialI/Recdef/examples.thy
doc-src/TutorialI/Recdef/simplification.thy
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/ToyList/ROOT.ML
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/root.tex
doc-src/TutorialI/ToyList2/ROOT.ML
doc-src/TutorialI/Trie/Option2.thy
doc-src/TutorialI/Trie/ROOT.ML
doc-src/TutorialI/Trie/Trie.thy
doc-src/TutorialI/Trie/document/root.tex
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Wed Apr 19 11:56:31 2000 +0200
     1.3 @@ -0,0 +1,127 @@
     1.4 +(*<*)
     1.5 +theory ABexpr = Main:;
     1.6 +(*>*)
     1.7 +
     1.8 +text{*
     1.9 +Sometimes it is necessary to define two datatypes that depend on each
    1.10 +other. This is called \textbf{mutual recursion}. As an example consider a
    1.11 +language of arithmetic and boolean expressions where
    1.12 +\begin{itemize}
    1.13 +\item arithmetic expressions contain boolean expressions because there are
    1.14 +  conditional arithmetic expressions like ``if $m<n$ then $n-m$ else $m-n$'',
    1.15 +  and
    1.16 +\item boolean expressions contain arithmetic expressions because of
    1.17 +  comparisons like ``$m<n$''.
    1.18 +\end{itemize}
    1.19 +In Isabelle this becomes
    1.20 +*}
    1.21 +
    1.22 +datatype 'a aexp = IF   "'a bexp" "'a aexp" "'a aexp"
    1.23 +                 | Sum  "'a aexp" "'a aexp"
    1.24 +                 | Diff "'a aexp" "'a aexp"
    1.25 +                 | Var 'a
    1.26 +                 | Num nat
    1.27 +and      'a bexp = Less "'a aexp" "'a aexp"
    1.28 +                 | And  "'a bexp" "'a bexp"
    1.29 +                 | Neg  "'a bexp";
    1.30 +
    1.31 +text{*\noindent
    1.32 +Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler},
    1.33 +except that we have fixed the values to be of type \isa{nat} and that we
    1.34 +have fixed the two binary operations \isa{Sum} and \isa{Diff}. Boolean
    1.35 +expressions can be arithmetic comparisons, conjunctions and negations.
    1.36 +The semantics is fixed via two evaluation functions
    1.37 +*}
    1.38 +
    1.39 +consts  evala :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a aexp \\<Rightarrow> nat"
    1.40 +        evalb :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a bexp \\<Rightarrow> bool";
    1.41 +
    1.42 +text{*\noindent
    1.43 +that take an environment (a mapping from variables \isa{'a} to values
    1.44 +\isa{nat}) and an expression and return its arithmetic/boolean
    1.45 +value. Since the datatypes are mutually recursive, so are functions that
    1.46 +operate on them. Hence they need to be defined in a single \isacommand{primrec}
    1.47 +section:
    1.48 +*}
    1.49 +
    1.50 +primrec
    1.51 +  "evala env (IF b a1 a2) =
    1.52 +     (if evalb env b then evala env a1 else evala env a2)"
    1.53 +  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
    1.54 +  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
    1.55 +  "evala env (Var v) = env v"
    1.56 +  "evala env (Num n) = n"
    1.57 +
    1.58 +  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
    1.59 +  "evalb env (And b1 b2) = (evalb env b1 \\<and> evalb env b2)"
    1.60 +  "evalb env (Neg b) = (\\<not> evalb env b)"
    1.61 +
    1.62 +text{*\noindent
    1.63 +In the same fashion we also define two functions that perform substitution:
    1.64 +*}
    1.65 +
    1.66 +consts substa :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a aexp \\<Rightarrow> 'b aexp"
    1.67 +       substb :: "('a \\<Rightarrow> 'b aexp) \\<Rightarrow> 'a bexp \\<Rightarrow> 'b bexp";
    1.68 +
    1.69 +text{*\noindent
    1.70 +The first argument is a function mapping variables to expressions, the
    1.71 +substitution. It is applied to all variables in the second argument. As a
    1.72 +result, the type of variables in the expression may change from \isa{'a}
    1.73 +to \isa{'b}. Note that there are only arithmetic and no boolean variables.
    1.74 +*}
    1.75 +
    1.76 +primrec
    1.77 +  "substa s (IF b a1 a2) =
    1.78 +     IF (substb s b) (substa s a1) (substa s a2)"
    1.79 +  "substa s (Sum a1 a2) = Sum (substa s a1) (substa s a2)"
    1.80 +  "substa s (Diff a1 a2) = Diff (substa s a1) (substa s a2)"
    1.81 +  "substa s (Var v) = s v"
    1.82 +  "substa s (Num n) = Num n"
    1.83 +
    1.84 +  "substb s (Less a1 a2) = Less (substa s a1) (substa s a2)"
    1.85 +  "substb s (And b1 b2) = And (substb s b1) (substb s b2)"
    1.86 +  "substb s (Neg b) = Neg (substb s b)";
    1.87 +
    1.88 +text{*
    1.89 +Now we can prove a fundamental theorem about the interaction between
    1.90 +evaluation and substitution: applying a substitution $s$ to an expression $a$
    1.91 +and evaluating the result in an environment $env$ yields the same result as
    1.92 +evaluation $a$ in the environment that maps every variable $x$ to the value
    1.93 +of $s(x)$ under $env$. If you try to prove this separately for arithmetic or
    1.94 +boolean expressions (by induction), you find that you always need the other
    1.95 +theorem in the induction step. Therefore you need to state and prove both
    1.96 +theorems simultaneously:
    1.97 +*}
    1.98 +
    1.99 +lemma "evala env (substa s a) = evala (\\<lambda>x. evala env (s x)) a \\<and>
   1.100 +        evalb env (substb s b) = evalb (\\<lambda>x. evala env (s x)) b";
   1.101 +apply(induct_tac a and b);
   1.102 +
   1.103 +txt{*\noindent
   1.104 +The resulting 8 goals (one for each constructor) are proved in one fell swoop:
   1.105 +*}
   1.106 +
   1.107 +apply auto.;
   1.108 +
   1.109 +text{*
   1.110 +In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$,
   1.111 +an inductive proof expects a goal of the form
   1.112 +\[ P@1(x@1)\ \land \dots \land P@n(x@n) \]
   1.113 +where each variable $x@i$ is of type $\tau@i$. Induction is started by
   1.114 +\begin{ttbox}
   1.115 +apply(induct_tac \(x@1\) \texttt{and} \(\dots\) \texttt{and} \(x@n\));
   1.116 +\end{ttbox}
   1.117 +
   1.118 +\begin{exercise}
   1.119 +  Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that
   1.120 +  replaces \isa{IF}s with complex boolean conditions by nested
   1.121 +  \isa{IF}s where each condition is a \isa{Less} --- \isa{And} and
   1.122 +  \isa{Neg} should be eliminated completely. Prove that \isa{norma}
   1.123 +  preserves the value of an expression and that the result of \isa{norma}
   1.124 +  is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in
   1.125 +  it.  ({\em Hint:} proceed as in \S\ref{sec:boolex}).
   1.126 +\end{exercise}
   1.127 +*}
   1.128 +(*<*)
   1.129 +end
   1.130 +(*>*)
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy	Wed Apr 19 11:56:31 2000 +0200
     2.3 @@ -0,0 +1,53 @@
     2.4 +(*<*)
     2.5 +theory Fundata = Main:
     2.6 +(*>*)
     2.7 +datatype ('a,'i)bigtree = Tip | Branch 'a "'i \\<Rightarrow> ('a,'i)bigtree"
     2.8 +
     2.9 +text{*\noindent Parameter \isa{'a} is the type of values stored in
    2.10 +the \isa{Branch}es of the tree, whereas \isa{'i} is the index
    2.11 +type over which the tree branches. If \isa{'i} is instantiated to
    2.12 +\isa{bool}, the result is a binary tree; if it is instantiated to
    2.13 +\isa{nat}, we have an infinitely branching tree because each node
    2.14 +has as many subtrees as there are natural numbers. How can we possibly
    2.15 +write down such a tree? Using functional notation! For example, the *}
    2.16 +
    2.17 +term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))";
    2.18 +
    2.19 +text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose
    2.20 +root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
    2.21 +has merely \isa{Tip}s as further subtrees.
    2.22 +
    2.23 +Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:
    2.24 +*}
    2.25 +
    2.26 +consts map_bt :: "('a \\<Rightarrow> 'b) \\<Rightarrow> ('a,'i)bigtree \\<Rightarrow> ('b,'i)bigtree"
    2.27 +primrec
    2.28 +"map_bt f Tip          = Tip"
    2.29 +"map_bt f (Branch a F) = Branch (f a) (\\<lambda>i. map_bt f (F i))"
    2.30 +
    2.31 +text{*\noindent This is a valid \isacommand{primrec} definition because the
    2.32 +recursive calls of \isa{map_bt} involve only subtrees obtained from
    2.33 +\isa{F}, i.e.\ the left-hand side. Thus termination is assured.  The
    2.34 +seasoned functional programmer might have written \isa{map_bt~f~o~F} instead
    2.35 +of \isa{\isasymlambda{}i.~map_bt~f~(F~i)}, but the former is not accepted by
    2.36 +Isabelle because the termination proof is not as obvious since
    2.37 +\isa{map_bt} is only partially applied.
    2.38 +
    2.39 +The following lemma has a canonical proof  *}
    2.40 +
    2.41 +lemma "map_bt g (map_bt f T) = map_bt (g o f) T";
    2.42 +apply(induct_tac "T", auto).
    2.43 +
    2.44 +text{*\noindent
    2.45 +but it is worth taking a look at the proof state after the induction step
    2.46 +to understand what the presence of the function type entails:
    2.47 +\begin{isabellepar}%
    2.48 +~1.~map\_bt~g~(map\_bt~f~Tip)~=~map\_bt~(g~{\isasymcirc}~f)~Tip\isanewline
    2.49 +~2.~{\isasymAnd}a~F.\isanewline
    2.50 +~~~~~~{\isasymforall}x.~map\_bt~g~(map\_bt~f~(F~x))~=~map\_bt~(g~{\isasymcirc}~f)~(F~x)~{\isasymLongrightarrow}\isanewline
    2.51 +~~~~~~map\_bt~g~(map\_bt~f~(Branch~a~F))~=~map\_bt~(g~{\isasymcirc}~f)~(Branch~a~F)%
    2.52 +\end{isabellepar}%
    2.53 +*}
    2.54 +(*<*)
    2.55 +end
    2.56 +(*>*)
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/doc-src/TutorialI/Datatype/Nested.thy	Wed Apr 19 11:56:31 2000 +0200
     3.3 @@ -0,0 +1,90 @@
     3.4 +(*<*)
     3.5 +theory Nested = Main:;
     3.6 +(*>*)
     3.7 +
     3.8 +text{*
     3.9 +So far, all datatypes had the property that on the right-hand side of their
    3.10 +definition they occurred only at the top-level, i.e.\ directly below a
    3.11 +constructor. This is not the case any longer for the following model of terms
    3.12 +where function symbols can be applied to a list of arguments:
    3.13 +*}
    3.14 +
    3.15 +datatype ('a,'b)"term" = Var 'a | App 'b "('a,'b)term list";
    3.16 +
    3.17 +text{*\noindent
    3.18 +Note that we need to quote \isa{term} on the left to avoid confusion with
    3.19 +the command \isacommand{term}.
    3.20 +Parameter \isa{'a} is the type of variables and \isa{'b} the type of
    3.21 +function symbols.
    3.22 +A mathematical term like $f(x,g(y))$ becomes \isa{App f [Var x, App g
    3.23 +  [Var y]]}, where \isa{f}, \isa{g}, \isa{x}, \isa{y} are
    3.24 +suitable values, e.g.\ numbers or strings.
    3.25 +
    3.26 +What complicates the definition of \isa{term} is the nested occurrence of
    3.27 +\isa{term} inside \isa{list} on the right-hand side. In principle,
    3.28 +nested recursion can be eliminated in favour of mutual recursion by unfolding
    3.29 +the offending datatypes, here \isa{list}. The result for \isa{term}
    3.30 +would be something like
    3.31 +\begin{ttbox}
    3.32 +\input{Datatype/tunfoldeddata}\end{ttbox}
    3.33 +Although we do not recommend this unfolding to the user, it shows how to
    3.34 +simulate nested recursion by mutual recursion.
    3.35 +Now we return to the initial definition of \isa{term} using
    3.36 +nested recursion.
    3.37 +
    3.38 +Let us define a substitution function on terms. Because terms involve term
    3.39 +lists, we need to define two substitution functions simultaneously:
    3.40 +*}
    3.41 +
    3.42 +consts
    3.43 +subst :: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term      \\<Rightarrow> ('a,'b)term"
    3.44 +substs:: "('a\\<Rightarrow>('a,'b)term) \\<Rightarrow> ('a,'b)term list \\<Rightarrow> ('a,'b)term list";
    3.45 +
    3.46 +primrec
    3.47 +  "subst s (Var x) = s x"
    3.48 +  "subst s (App f ts) = App f (substs s ts)"
    3.49 +
    3.50 +  "substs s [] = []"
    3.51 +  "substs s (t # ts) = subst s t # substs s ts";
    3.52 +
    3.53 +text{*\noindent
    3.54 +Similarly, when proving a statement about terms inductively, we need
    3.55 +to prove a related statement about term lists simultaneously. For example,
    3.56 +the fact that the identity substitution does not change a term needs to be
    3.57 +strengthened and proved as follows:
    3.58 +*}
    3.59 +
    3.60 +lemma "subst  Var t  = (t ::('a,'b)term)  \\<and>
    3.61 +        substs Var ts = (ts::('a,'b)term list)";
    3.62 +apply(induct_tac t and ts, auto).;
    3.63 +
    3.64 +text{*\noindent
    3.65 +Note that \isa{Var} is the identity substitution because by definition it
    3.66 +leaves variables unchanged: \isa{subst Var (Var $x$) = Var $x$}. Note also
    3.67 +that the type annotations are necessary because otherwise there is nothing in
    3.68 +the goal to enforce that both halves of the goal talk about the same type
    3.69 +parameters \isa{('a,'b)}. As a result, induction would fail
    3.70 +because the two halves of the goal would be unrelated.
    3.71 +
    3.72 +\begin{exercise}
    3.73 +The fact that substitution distributes over composition can be expressed
    3.74 +roughly as follows:
    3.75 +\begin{ttbox}
    3.76 +subst (f o g) t = subst f (subst g t)
    3.77 +\end{ttbox}
    3.78 +Correct this statement (you will find that it does not type-check),
    3.79 +strengthen it, and prove it. (Note: \ttindexbold{o} is function composition;
    3.80 +its definition is found in theorem \isa{o_def}).
    3.81 +\end{exercise}
    3.82 +
    3.83 +Of course, you may also combine mutual and nested recursion. For example,
    3.84 +constructor \isa{Sum} in \S\ref{sec:datatype-mut-rec} could take a list of
    3.85 +expressions as its argument: \isa{Sum "'a aexp list"}.
    3.86 +*}
    3.87 +(*<*)
    3.88 +
    3.89 +lemma "subst s (App f ts) = App f (map (subst s) ts)";
    3.90 +apply(induct_tac ts, auto).;
    3.91 +
    3.92 +end
    3.93 +(*>*)
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/doc-src/TutorialI/Datatype/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
     4.3 @@ -0,0 +1,3 @@
     4.4 +use_thy "ABexpr";
     4.5 +use_thy "Nested";
     4.6 +use_thy "Fundata";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/doc-src/TutorialI/Datatype/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
     5.3 @@ -0,0 +1,4 @@
     5.4 +\documentclass{article}
     5.5 +\begin{document}
     5.6 +xxx
     5.7 +\end{document}
     6.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     6.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Wed Apr 19 11:56:31 2000 +0200
     6.3 @@ -0,0 +1,164 @@
     6.4 +(*<*)
     6.5 +theory Ifexpr = Main:;
     6.6 +(*>*)
     6.7 +
     6.8 +text{*
     6.9 +\subsubsection{How can we model boolean expressions?}
    6.10 +
    6.11 +We want to represent boolean expressions built up from variables and
    6.12 +constants by negation and conjunction. The following datatype serves exactly
    6.13 +that purpose:
    6.14 +*}
    6.15 +
    6.16 +datatype boolex = Const bool | Var nat | Neg boolex
    6.17 +                | And boolex boolex;
    6.18 +
    6.19 +text{*\noindent
    6.20 +The two constants are represented by \isa{Const~True} and
    6.21 +\isa{Const~False}. Variables are represented by terms of the form
    6.22 +\isa{Var~$n$}, where $n$ is a natural number (type \isa{nat}).
    6.23 +For example, the formula $P@0 \land \neg P@1$ is represented by the term
    6.24 +\isa{And~(Var~0)~(Neg(Var~1))}.
    6.25 +
    6.26 +\subsubsection{What is the value of a boolean expression?}
    6.27 +
    6.28 +The value of a boolean expression depends on the value of its variables.
    6.29 +Hence the function \isa{value} takes an additional parameter, an {\em
    6.30 +  environment} of type \isa{nat \isasymFun\ bool}, which maps variables to
    6.31 +their values:
    6.32 +*}
    6.33 +
    6.34 +consts value :: "boolex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
    6.35 +primrec
    6.36 +"value (Const b) env = b"
    6.37 +"value (Var x)   env = env x"
    6.38 +"value (Neg b)   env = (\\<not> value b env)"
    6.39 +"value (And b c) env = (value b env \\<and> value c env)";
    6.40 +
    6.41 +text{*\noindent
    6.42 +\subsubsection{If-expressions}
    6.43 +
    6.44 +An alternative and often more efficient (because in a certain sense
    6.45 +canonical) representation are so-called \emph{If-expressions} built up
    6.46 +from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
    6.47 +(\isa{IF}):
    6.48 +*}
    6.49 +
    6.50 +datatype ifex = CIF bool | VIF nat | IF ifex ifex ifex;
    6.51 +
    6.52 +text{*\noindent
    6.53 +The evaluation if If-expressions proceeds as for \isa{boolex}:
    6.54 +*}
    6.55 +
    6.56 +consts valif :: "ifex \\<Rightarrow> (nat \\<Rightarrow> bool) \\<Rightarrow> bool";
    6.57 +primrec
    6.58 +"valif (CIF b)    env = b"
    6.59 +"valif (VIF x)    env = env x"
    6.60 +"valif (IF b t e) env = (if valif b env then valif t env
    6.61 +                                        else valif e env)";
    6.62 +
    6.63 +text{*
    6.64 +\subsubsection{Transformation into and of If-expressions}
    6.65 +
    6.66 +The type \isa{boolex} is close to the customary representation of logical
    6.67 +formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
    6.68 +translate from \isa{boolex} into \isa{ifex}:
    6.69 +*}
    6.70 +
    6.71 +consts bool2if :: "boolex \\<Rightarrow> ifex";
    6.72 +primrec
    6.73 +"bool2if (Const b) = CIF b"
    6.74 +"bool2if (Var x)   = VIF x"
    6.75 +"bool2if (Neg b)   = IF (bool2if b) (CIF False) (CIF True)"
    6.76 +"bool2if (And b c) = IF (bool2if b) (bool2if c) (CIF False)";
    6.77 +
    6.78 +text{*\noindent
    6.79 +At last, we have something we can verify: that \isa{bool2if} preserves the
    6.80 +value of its argument:
    6.81 +*}
    6.82 +
    6.83 +lemma "valif (bool2if b) env = value b env";
    6.84 +
    6.85 +txt{*\noindent
    6.86 +The proof is canonical:
    6.87 +*}
    6.88 +
    6.89 +apply(induct_tac b);
    6.90 +apply(auto).;
    6.91 +
    6.92 +text{*\noindent
    6.93 +In fact, all proofs in this case study look exactly like this. Hence we do
    6.94 +not show them below.
    6.95 +
    6.96 +More interesting is the transformation of If-expressions into a normal form
    6.97 +where the first argument of \isa{IF} cannot be another \isa{IF} but
    6.98 +must be a constant or variable. Such a normal form can be computed by
    6.99 +repeatedly replacing a subterm of the form \isa{IF~(IF~b~x~y)~z~u} by
   6.100 +\isa{IF b (IF x z u) (IF y z u)}, which has the same value. The following
   6.101 +primitive recursive functions perform this task:
   6.102 +*}
   6.103 +
   6.104 +consts normif :: "ifex \\<Rightarrow> ifex \\<Rightarrow> ifex \\<Rightarrow> ifex";
   6.105 +primrec
   6.106 +"normif (CIF b)    t e = IF (CIF b) t e"
   6.107 +"normif (VIF x)    t e = IF (VIF x) t e"
   6.108 +"normif (IF b t e) u f = normif b (normif t u f) (normif e u f)";
   6.109 +
   6.110 +consts norm :: "ifex \\<Rightarrow> ifex";
   6.111 +primrec
   6.112 +"norm (CIF b)    = CIF b"
   6.113 +"norm (VIF x)    = VIF x"
   6.114 +"norm (IF b t e) = normif b (norm t) (norm e)";
   6.115 +
   6.116 +text{*\noindent
   6.117 +Their interplay is a bit tricky, and we leave it to the reader to develop an
   6.118 +intuitive understanding. Fortunately, Isabelle can help us to verify that the
   6.119 +transformation preserves the value of the expression:
   6.120 +*}
   6.121 +
   6.122 +theorem "valif (norm b) env = valif b env";(*<*)oops;(*>*)
   6.123 +
   6.124 +text{*\noindent
   6.125 +The proof is canonical, provided we first show the following simplification
   6.126 +lemma (which also helps to understand what \isa{normif} does):
   6.127 +*}
   6.128 +
   6.129 +lemma [simp]:
   6.130 +  "\\<forall>t e. valif (normif b t e) env = valif (IF b t e) env";
   6.131 +(*<*)
   6.132 +apply(induct_tac b);
   6.133 +apply(auto).;
   6.134 +
   6.135 +theorem "valif (norm b) env = valif b env";
   6.136 +apply(induct_tac b);
   6.137 +apply(auto).;
   6.138 +(*>*)
   6.139 +text{*\noindent
   6.140 +Note that the lemma does not have a name, but is implicitly used in the proof
   6.141 +of the theorem shown above because of the \isa{[simp]} attribute.
   6.142 +
   6.143 +But how can we be sure that \isa{norm} really produces a normal form in
   6.144 +the above sense? We define a function that tests If-expressions for normality
   6.145 +*}
   6.146 +
   6.147 +consts normal :: "ifex \\<Rightarrow> bool";
   6.148 +primrec
   6.149 +"normal(CIF b) = True"
   6.150 +"normal(VIF x) = True"
   6.151 +"normal(IF b t e) = (normal t \\<and> normal e \\<and>
   6.152 +     (case b of CIF b \\<Rightarrow> True | VIF x \\<Rightarrow> True | IF x y z \\<Rightarrow> False))";
   6.153 +
   6.154 +text{*\noindent
   6.155 +and prove \isa{normal(norm b)}. Of course, this requires a lemma about
   6.156 +normality of \isa{normif}:
   6.157 +*}
   6.158 +
   6.159 +lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*)
   6.160 +apply(induct_tac b);
   6.161 +apply(auto).;
   6.162 +
   6.163 +theorem "normal(norm b)";
   6.164 +apply(induct_tac b);
   6.165 +apply(auto).;
   6.166 +
   6.167 +end(*>*)
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/doc-src/TutorialI/Ifexpr/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
     7.3 @@ -0,0 +1,1 @@
     7.4 +use_thy "Ifexpr";
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/doc-src/TutorialI/Ifexpr/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
     8.3 @@ -0,0 +1,4 @@
     8.4 +\documentclass{article}
     8.5 +\begin{document}
     8.6 +xxx
     8.7 +\end{document}
     9.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     9.2 +++ b/doc-src/TutorialI/Misc/Itrev.thy	Wed Apr 19 11:56:31 2000 +0200
     9.3 @@ -0,0 +1,90 @@
     9.4 +(*<*)
     9.5 +theory Itrev = Main:;
     9.6 +(*>*)
     9.7 +
     9.8 +text{*
     9.9 +We define a tail-recursive version of list-reversal,
    9.10 +i.e.\ one that can be compiled into a loop:
    9.11 +*}
    9.12 +
    9.13 +consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list";
    9.14 +primrec
    9.15 +"itrev []     ys = ys"
    9.16 +"itrev (x#xs) ys = itrev xs (x#ys)";
    9.17 +
    9.18 +text{*\noindent
    9.19 +The behaviour of \isa{itrev} is simple: it reverses its first argument by
    9.20 +stacking its elements onto the second argument, and returning that second
    9.21 +argument when the first one becomes empty.
    9.22 +We need to show that \isa{itrev} does indeed reverse its first argument
    9.23 +provided the second one is empty:
    9.24 +*}
    9.25 +
    9.26 +lemma "itrev xs [] = rev xs";
    9.27 +
    9.28 +txt{*\noindent
    9.29 +There is no choice as to the induction variable, and we immediately simplify:
    9.30 +*}
    9.31 +
    9.32 +apply(induct_tac xs, auto);
    9.33 +
    9.34 +txt{*\noindent
    9.35 +Unfortunately, this is not a complete success:
    9.36 +\begin{isabellepar}%
    9.37 +~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]%
    9.38 +\end{isabellepar}%
    9.39 +Just as predicted above, the overall goal, and hence the induction
    9.40 +hypothesis, is too weak to solve the induction step because of the fixed
    9.41 +\isa{[]}. The corresponding heuristic:
    9.42 +\begin{quote}
    9.43 +{\em 3. Generalize goals for induction by replacing constants by variables.}
    9.44 +\end{quote}
    9.45 +
    9.46 +Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is
    9.47 +just not true---the correct generalization is
    9.48 +*}
    9.49 +(*<*)oops;(*>*)
    9.50 +lemma "itrev xs ys = rev xs @ ys";
    9.51 +
    9.52 +txt{*\noindent
    9.53 +If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to
    9.54 +\isa{rev xs}, just as required.
    9.55 +
    9.56 +In this particular instance it was easy to guess the right generalization,
    9.57 +but in more complex situations a good deal of creativity is needed. This is
    9.58 +the main source of complications in inductive proofs.
    9.59 +
    9.60 +Although we now have two variables, only \isa{xs} is suitable for
    9.61 +induction, and we repeat our above proof attempt. Unfortunately, we are still
    9.62 +not there:
    9.63 +\begin{isabellepar}%
    9.64 +~1.~{\isasymAnd}a~list.\isanewline
    9.65 +~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline
    9.66 +~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys%
    9.67 +\end{isabellepar}%
    9.68 +The induction hypothesis is still too weak, but this time it takes no
    9.69 +intuition to generalize: the problem is that \isa{ys} is fixed throughout
    9.70 +the subgoal, but the induction hypothesis needs to be applied with
    9.71 +\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem
    9.72 +for all \isa{ys} instead of a fixed one:
    9.73 +*}
    9.74 +(*<*)oops;(*>*)
    9.75 +lemma "\\<forall>ys. itrev xs ys = rev xs @ ys";
    9.76 +
    9.77 +txt{*\noindent
    9.78 +This time induction on \isa{xs} followed by simplification succeeds. This
    9.79 +leads to another heuristic for generalization:
    9.80 +\begin{quote}
    9.81 +{\em 4. Generalize goals for induction by universally quantifying all free
    9.82 +variables {\em(except the induction variable itself!)}.}
    9.83 +\end{quote}
    9.84 +This prevents trivial failures like the above and does not change the
    9.85 +provability of the goal. Because it is not always required, and may even
    9.86 +complicate matters in some cases, this heuristic is often not
    9.87 +applied blindly.
    9.88 +*}
    9.89 +
    9.90 +(*<*)
    9.91 +oops;
    9.92 +end
    9.93 +(*>*)
    10.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    10.2 +++ b/doc-src/TutorialI/Misc/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
    10.3 @@ -0,0 +1,18 @@
    10.4 +use_thy "Tree";
    10.5 +use_thy "cases";
    10.6 +use_thy "fakenat";
    10.7 +use_thy "natsum";
    10.8 +use_thy "arith1";
    10.9 +use_thy "arith2";
   10.10 +use_thy "arith3";
   10.11 +use_thy "arith4";
   10.12 +use_thy "pairs";
   10.13 +use_thy "types";
   10.14 +use_thy "prime_def";
   10.15 +use_thy "def_rewr";
   10.16 +use_thy "let_rewr";
   10.17 +use_thy "cond_rewr";
   10.18 +use_thy "case_splits";
   10.19 +use_thy "trace_simp";
   10.20 +use_thy "Itrev";
   10.21 +use_thy "asm_simp";
    11.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    11.2 +++ b/doc-src/TutorialI/Misc/Tree.thy	Wed Apr 19 11:56:31 2000 +0200
    11.3 @@ -0,0 +1,27 @@
    11.4 +(*<*)
    11.5 +theory Tree = Main:
    11.6 +(*>*)
    11.7 +
    11.8 +text{*\noindent
    11.9 +Define the datatype of binary trees
   11.10 +*}
   11.11 +
   11.12 +datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
   11.13 +
   11.14 +consts mirror :: "'a tree \\<Rightarrow> 'a tree";
   11.15 +primrec
   11.16 +"mirror Tip = Tip"
   11.17 +"mirror (Node l x r) = Node (mirror l) x (mirror r)";(*>*)
   11.18 +
   11.19 +text{*\noindent
   11.20 +and a function \isa{mirror} that mirrors a binary tree
   11.21 +by swapping subtrees (recursively). Prove
   11.22 +*}
   11.23 +
   11.24 +lemma mirror_mirror: "mirror(mirror t) = t";
   11.25 +(*<*)
   11.26 +apply(induct_tac t);
   11.27 +apply(auto).;
   11.28 +
   11.29 +end
   11.30 +(*>*)
    12.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    12.2 +++ b/doc-src/TutorialI/Misc/arith1.thy	Wed Apr 19 11:56:31 2000 +0200
    12.3 @@ -0,0 +1,8 @@
    12.4 +(*<*)
    12.5 +theory arith1 = Main:;
    12.6 +(*>*)
    12.7 +lemma "\\<lbrakk> \\<not> m < n; m < n+1 \\<rbrakk> \\<Longrightarrow> m = n";
    12.8 +(**)(*<*)
    12.9 +apply(auto).;
   12.10 +end
   12.11 +(*>*)
    13.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    13.2 +++ b/doc-src/TutorialI/Misc/arith2.thy	Wed Apr 19 11:56:31 2000 +0200
    13.3 @@ -0,0 +1,8 @@
    13.4 +(*<*)
    13.5 +theory arith2 = Main:;
    13.6 +(*>*)
    13.7 +lemma "min i (max j (k*k)) = max (min (k*k) i) (min i (j::nat))";
    13.8 +apply(arith).;
    13.9 +(**)(*<*)
   13.10 +end
   13.11 +(*>*)
    14.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    14.2 +++ b/doc-src/TutorialI/Misc/arith3.thy	Wed Apr 19 11:56:31 2000 +0200
    14.3 @@ -0,0 +1,8 @@
    14.4 +(*<*)
    14.5 +theory arith3 = Main:;
    14.6 +(*>*)
    14.7 +lemma "n*n = n \\<Longrightarrow> n=0 \\<or> n=1";
    14.8 +(**)(*<*)
    14.9 +oops;
   14.10 +end
   14.11 +(*>*)
    15.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    15.2 +++ b/doc-src/TutorialI/Misc/arith4.thy	Wed Apr 19 11:56:31 2000 +0200
    15.3 @@ -0,0 +1,8 @@
    15.4 +(*<*)
    15.5 +theory arith4 = Main:;
    15.6 +(*>*)
    15.7 +lemma "\\<not> m < n \\<and> m < n+1 \\<Longrightarrow> m = n";
    15.8 +(**)(*<*)
    15.9 +oops;
   15.10 +end
   15.11 +(*>*)
    16.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    16.2 +++ b/doc-src/TutorialI/Misc/asm_simp.thy	Wed Apr 19 11:56:31 2000 +0200
    16.3 @@ -0,0 +1,49 @@
    16.4 +(*<*)
    16.5 +theory asm_simp = Main:;
    16.6 +
    16.7 +(*>*)text{*
    16.8 +By default, assumptions are part of the simplification process: they are used
    16.9 +as simplification rules and are simplified themselves. For example:
   16.10 +*}
   16.11 +
   16.12 +lemma "\\<lbrakk> xs @ zs = ys @ xs; [] @ xs = [] @ [] \\<rbrakk> \\<Longrightarrow> ys = zs";
   16.13 +apply simp.;
   16.14 +
   16.15 +text{*\noindent
   16.16 +The second assumption simplifies to \isa{xs = []}, which in turn
   16.17 +simplifies the first assumption to \isa{zs = ys}, thus reducing the
   16.18 +conclusion to \isa{ys = ys} and hence to \isa{True}.
   16.19 +
   16.20 +In some cases this may be too much of a good thing and may lead to
   16.21 +nontermination:
   16.22 +*}
   16.23 +
   16.24 +lemma "\\<forall>x. f x = g (f (g x)) \\<Longrightarrow> f [] = f [] @ []";
   16.25 +
   16.26 +txt{*\noindent
   16.27 +cannot be solved by an unmodified application of \isa{simp} because the
   16.28 +simplification rule \isa{f x = g(f(g x))} extracted from the assumption
   16.29 +does not terminate. Isabelle notices certain simple forms of
   16.30 +nontermination but not this one. The problem can be circumvented by
   16.31 +explicitly telling the simplifier to ignore the assumptions:
   16.32 +*}
   16.33 +
   16.34 +apply(simp no_asm:).;
   16.35 +
   16.36 +text{*\noindent
   16.37 +There are three modifiers that influence the treatment of assumptions:
   16.38 +\begin{description}
   16.39 +\item[\isaindexbold{no_asm:}] means that assumptions are completely ignored.
   16.40 +\item[\isaindexbold{no_asm_simp:}] means that the assumptions are not simplified but
   16.41 +  are used in the simplification of the conclusion.
   16.42 +\item[\isaindexbold{no_asm_use:}] means that the assumptions are simplified
   16.43 +but are not
   16.44 +  used in the simplification of each other or the conclusion.
   16.45 +\end{description}
   16.46 +Neither \isa{no_asm_simp:} nor \isa{no_asm_use:} allow to simplify the above
   16.47 +problematic subgoal.
   16.48 +
   16.49 +Note that only one of the above modifiers is allowed, and it must precede all
   16.50 +other modifiers.
   16.51 +*}
   16.52 +(*<*)end(*>*)
    17.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    17.2 +++ b/doc-src/TutorialI/Misc/case_splits.thy	Wed Apr 19 11:56:31 2000 +0200
    17.3 @@ -0,0 +1,85 @@
    17.4 +(*<*)
    17.5 +theory case_splits = Main:;
    17.6 +(*>*)
    17.7 +
    17.8 +text{*
    17.9 +Goals containing \isaindex{if}-expressions are usually proved by case
   17.10 +distinction on the condition of the \isa{if}. For example the goal
   17.11 +*}
   17.12 +
   17.13 +lemma "\\<forall>xs. if xs = [] then rev xs = [] else rev xs \\<noteq> []";
   17.14 +
   17.15 +txt{*\noindent
   17.16 +can be split into
   17.17 +\begin{isabellepar}%
   17.18 +~1.~{\isasymforall}xs.~(xs~=~[]~{\isasymlongrightarrow}~rev~xs~=~[])~{\isasymand}~(xs~{\isasymnoteq}~[]~{\isasymlongrightarrow}~rev~xs~{\isasymnoteq}~[])%
   17.19 +\end{isabellepar}%
   17.20 +by a degenerate form of simplification
   17.21 +*}
   17.22 +
   17.23 +apply(simp only: split: split_if);
   17.24 +(*<*)oops;(*>*)
   17.25 +
   17.26 +text{*\noindent
   17.27 +where no simplification rules are included (\isa{only:} is followed by the
   17.28 +empty list of theorems) but the rule \isaindexbold{split_if} for
   17.29 +splitting \isa{if}s is added (via the modifier \isa{split:}). Because
   17.30 +case-splitting on \isa{if}s is almost always the right proof strategy, the
   17.31 +simplifier performs it automatically. Try \isacommand{apply}\isa{(simp)}
   17.32 +on the initial goal above.
   17.33 +
   17.34 +This splitting idea generalizes from \isa{if} to \isaindex{case}:
   17.35 +*}
   17.36 +
   17.37 +lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
   17.38 +txt{*\noindent
   17.39 +becomes
   17.40 +\begin{isabellepar}%
   17.41 +~1.~(xs~=~[]~{\isasymlongrightarrow}~zs~=~xs~@~zs)~{\isasymand}\isanewline
   17.42 +~~~~({\isasymforall}a~list.~xs~=~a~\#~list~{\isasymlongrightarrow}~a~\#~list~@~zs~=~xs~@~zs)%
   17.43 +\end{isabellepar}%
   17.44 +by typing
   17.45 +*}
   17.46 +
   17.47 +apply(simp only: split: list.split);
   17.48 +(*<*)oops;(*>*)
   17.49 +
   17.50 +text{*\noindent
   17.51 +In contrast to \isa{if}-expressions, the simplifier does not split
   17.52 +\isa{case}-expressions by default because this can lead to nontermination
   17.53 +in case of recursive datatypes. Again, if the \isa{only:} modifier is
   17.54 +dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)}
   17.55 +alone will not do:
   17.56 +*}
   17.57 +(*<*)
   17.58 +lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
   17.59 +(*>*)
   17.60 +apply(simp split: list.split).;
   17.61 +
   17.62 +text{*
   17.63 +In general, every datatype $t$ comes with a theorem
   17.64 +\isa{$t$.split} which can be declared to be a \bfindex{split rule} either
   17.65 +locally as above, or by giving it the \isa{split} attribute globally:
   17.66 +*}
   17.67 +
   17.68 +theorems [split] = list.split;
   17.69 +
   17.70 +text{*\noindent
   17.71 +The \isa{split} attribute can be removed with the \isa{del} modifier,
   17.72 +either locally
   17.73 +*}
   17.74 +(*<*)
   17.75 +lemma "dummy=dummy";
   17.76 +(*>*)
   17.77 +apply(simp split del: split_if);
   17.78 +(*<*)
   17.79 +oops;
   17.80 +(*>*)
   17.81 +text{*\noindent
   17.82 +or globally:
   17.83 +*}
   17.84 +theorems [split del] = list.split;
   17.85 +
   17.86 +(*<*)
   17.87 +end
   17.88 +(*>*)
    18.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    18.2 +++ b/doc-src/TutorialI/Misc/cases.thy	Wed Apr 19 11:56:31 2000 +0200
    18.3 @@ -0,0 +1,19 @@
    18.4 +(*<*)
    18.5 +theory "cases" = Main:;
    18.6 +(*>*)
    18.7 +
    18.8 +lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
    18.9 +apply(case_tac xs);
   18.10 +
   18.11 +txt{*
   18.12 +\begin{isabellepar}%
   18.13 +~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
   18.14 +~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
   18.15 +\end{isabellepar}%
   18.16 +*}
   18.17 +
   18.18 +apply(auto).;
   18.19 +(**)
   18.20 +(*<*)
   18.21 +end
   18.22 +(*>*)
    19.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    19.2 +++ b/doc-src/TutorialI/Misc/cond_rewr.thy	Wed Apr 19 11:56:31 2000 +0200
    19.3 @@ -0,0 +1,35 @@
    19.4 +(*<*)
    19.5 +theory cond_rewr = Main:;
    19.6 +(*>*)
    19.7 +
    19.8 +text{*
    19.9 +So far all examples of rewrite rules were equations. The simplifier also
   19.10 +accepts \emph{conditional} equations, for example
   19.11 +*}
   19.12 +
   19.13 +lemma hd_Cons_tl[simp]: "xs \\<noteq> []  \\<Longrightarrow>  hd xs # tl xs = xs";
   19.14 +apply(case_tac xs, simp, simp).;
   19.15 +
   19.16 +text{*\noindent
   19.17 +Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a
   19.18 +sequence of methods. Assuming that the simplification rule
   19.19 +*}(*<*)term(*>*) "(rev xs = []) = (xs = [])";
   19.20 +text{*\noindent
   19.21 +is present as well,
   19.22 +*}
   19.23 +
   19.24 +lemma "xs \\<noteq> [] \\<Longrightarrow> hd(rev xs) # tl(rev xs) = rev xs";
   19.25 +(*<*)
   19.26 +apply(simp).
   19.27 +(*>*)
   19.28 +text{*\noindent
   19.29 +is proved by simplification:
   19.30 +the conditional equation \isa{hd_Cons_tl} above
   19.31 +can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs}
   19.32 +because the corresponding precondition \isa{rev xs \isasymnoteq\ []}
   19.33 +simplifies to \isa{xs \isasymnoteq\ []}, which is exactly the local
   19.34 +assumption of the subgoal.
   19.35 +*}
   19.36 +(*<*)
   19.37 +end
   19.38 +(*>*)
    20.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    20.2 +++ b/doc-src/TutorialI/Misc/consts.thy	Wed Apr 19 11:56:31 2000 +0200
    20.3 @@ -0,0 +1,5 @@
    20.4 +(*<*)theory "consts" = Main:;
    20.5 +(*>*)consts nand :: gate
    20.6 +            exor :: gate(*<*)
    20.7 +end
    20.8 +(*>*)
    21.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    21.2 +++ b/doc-src/TutorialI/Misc/def_rewr.thy	Wed Apr 19 11:56:31 2000 +0200
    21.3 @@ -0,0 +1,46 @@
    21.4 +(*<*)
    21.5 +theory def_rewr = Main:;
    21.6 +
    21.7 +(*>*)text{*\noindent Constant definitions (\S\ref{sec:ConstDefinitions}) can
    21.8 +be used as simplification rules, but by default they are not.  Hence the
    21.9 +simplifier does not expand them automatically, just as it should be:
   21.10 +definitions are introduced for the purpose of abbreviating complex
   21.11 +concepts. Of course we need to expand the definitions initially to derive
   21.12 +enough lemmas that characterize the concept sufficiently for us to forget the
   21.13 +original definition. For example, given
   21.14 +*}
   21.15 +
   21.16 +constdefs exor :: "bool \\<Rightarrow> bool \\<Rightarrow> bool"
   21.17 +         "exor A B \\<equiv> (A \\<and> \\<not>B) \\<or> (\\<not>A \\<and> B)";
   21.18 +
   21.19 +text{*\noindent
   21.20 +we may want to prove
   21.21 +*}
   21.22 +
   21.23 +lemma "exor A (\\<not>A)";
   21.24 +
   21.25 +txt{*\noindent
   21.26 +There is a special method for \emph{unfolding} definitions, which we need to
   21.27 +get started:\indexbold{*unfold}\indexbold{definition!unfolding}
   21.28 +*}
   21.29 +
   21.30 +apply(unfold exor_def);
   21.31 +
   21.32 +txt{*\noindent
   21.33 +It unfolds the given list of definitions (here merely one) in all subgoals:
   21.34 +\begin{isabellepar}%
   21.35 +~1.~A~{\isasymand}~{\isasymnot}~{\isasymnot}~A~{\isasymor}~{\isasymnot}~A~{\isasymand}~{\isasymnot}~A%
   21.36 +\end{isabellepar}%
   21.37 +The resulting goal can be proved by simplification.
   21.38 +
   21.39 +In case we want to expand a definition in the middle of a proof, we can
   21.40 +simply include it locally:*}(*<*)oops;lemma "exor A (\\<not>A)";(*>*)
   21.41 +apply(simp add: exor_def);(*<*).(*>*)
   21.42 +
   21.43 +text{*\noindent
   21.44 +In fact, this one command proves the above lemma directly.
   21.45 +
   21.46 +You should normally not turn a definition permanently into a simplification
   21.47 +rule because this defeats the whole purpose of an abbreviation.
   21.48 +*}
   21.49 +(*<*)end(*>*)
    22.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    22.2 +++ b/doc-src/TutorialI/Misc/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
    22.3 @@ -0,0 +1,4 @@
    22.4 +\documentclass{article}
    22.5 +\begin{document}
    22.6 +xxx
    22.7 +\end{document}
    23.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    23.2 +++ b/doc-src/TutorialI/Misc/fakenat.thy	Wed Apr 19 11:56:31 2000 +0200
    23.3 @@ -0,0 +1,13 @@
    23.4 +(*<*)
    23.5 +theory fakenat = Main:;
    23.6 +(*>*)
    23.7 +
    23.8 +text{*\noindent
    23.9 +The type \isaindexbold{nat} of natural numbers is predefined and
   23.10 +behaves like
   23.11 +*}
   23.12 +
   23.13 +datatype nat = "0" | Suc nat
   23.14 +(*<*)
   23.15 +end
   23.16 +(*>*)
    24.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    24.2 +++ b/doc-src/TutorialI/Misc/let_rewr.thy	Wed Apr 19 11:56:31 2000 +0200
    24.3 @@ -0,0 +1,14 @@
    24.4 +(*<*)
    24.5 +theory let_rewr = Main:;
    24.6 +(*>*)
    24.7 +lemma "(let xs = [] in xs@ys@xs) = ys";
    24.8 +apply(simp add: Let_def).;
    24.9 +
   24.10 +text{*
   24.11 +If, in a particular context, there is no danger of a combinatorial explosion
   24.12 +of nested \texttt{let}s one could even add \texttt{Let_def} permanently:
   24.13 +*}
   24.14 +theorems [simp] = Let_def;
   24.15 +(*<*)
   24.16 +end
   24.17 +(*>*)
    25.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    25.2 +++ b/doc-src/TutorialI/Misc/natsum.thy	Wed Apr 19 11:56:31 2000 +0200
    25.3 @@ -0,0 +1,28 @@
    25.4 +(*<*)
    25.5 +theory natsum = Main:;
    25.6 +(*>*)
    25.7 +text{*\noindent
    25.8 +In particular, there are \isa{case}-expressions, for example
    25.9 +*}
   25.10 +
   25.11 +(*<*)term(*>*) "case n of 0 \\<Rightarrow> 0 | Suc m \\<Rightarrow> m";
   25.12 +
   25.13 +text{*\noindent
   25.14 +primitive recursion, for example
   25.15 +*}
   25.16 +
   25.17 +consts sum :: "nat \\<Rightarrow> nat";
   25.18 +primrec "sum 0 = 0"
   25.19 +        "sum (Suc n) = Suc n + sum n";
   25.20 +
   25.21 +text{*\noindent
   25.22 +and induction, for example
   25.23 +*}
   25.24 +
   25.25 +lemma "sum n + sum n = n*(Suc n)";
   25.26 +apply(induct_tac n);
   25.27 +apply(auto).;
   25.28 +
   25.29 +(*<*)
   25.30 +end
   25.31 +(*>*)
    26.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    26.2 +++ b/doc-src/TutorialI/Misc/pairs.thy	Wed Apr 19 11:56:31 2000 +0200
    26.3 @@ -0,0 +1,8 @@
    26.4 +(*<*)
    26.5 +theory pairs = Main:;
    26.6 +term(*>*) "let (x,y) = f z in (y,x)";
    26.7 +(*<*)
    26.8 +term(*>*) "case xs of [] \\<Rightarrow> 0 | (x,y)#zs \\<Rightarrow> x+y"
    26.9 +(**)(*<*)
   26.10 +end
   26.11 +(*>*)
    27.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    27.2 +++ b/doc-src/TutorialI/Misc/prime_def.thy	Wed Apr 19 11:56:31 2000 +0200
    27.3 @@ -0,0 +1,18 @@
    27.4 +(*<*)
    27.5 +theory prime_def = Main:;
    27.6 +consts prime :: "nat \\<Rightarrow> bool"
    27.7 +(*>*)
    27.8 +(*<*)term(*>*)
    27.9 +
   27.10 +    "prime(p) \\<equiv> 1 < p \\<and> ((m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))";
   27.11 +text{*\noindent\small
   27.12 +where \isa{dvd} means ``divides''.
   27.13 +Isabelle rejects this ``definition'' because of the extra \isa{m} on the
   27.14 +right-hand side, which would introduce an inconsistency. (Why?) What you
   27.15 +should have written is
   27.16 +*}
   27.17 +(*<*)term(*>*)
   27.18 + "prime(p) \\<equiv> 1 < p \\<and> (\\<forall>m. (m dvd p) \\<longrightarrow> (m=1 \\<or> m=p))"
   27.19 +(*<*)
   27.20 +end
   27.21 +(*>*)
    28.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    28.2 +++ b/doc-src/TutorialI/Misc/trace_simp.thy	Wed Apr 19 11:56:31 2000 +0200
    28.3 @@ -0,0 +1,46 @@
    28.4 +(*<*)
    28.5 +theory trace_simp = Main:;
    28.6 +(*>*)
    28.7 +
    28.8 +text{*
    28.9 +Using the simplifier effectively may take a bit of experimentation.  Set the
   28.10 +\ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going
   28.11 +on:
   28.12 +*}
   28.13 +ML "set trace_simp";
   28.14 +lemma "rev [a] = []";
   28.15 +apply(simp);
   28.16 +
   28.17 +txt{*\noindent
   28.18 +produces the trace
   28.19 +
   28.20 +\begin{ttbox}
   28.21 +Applying instance of rewrite rule:
   28.22 +rev (?x1 \# ?xs1) == rev ?xs1 @ [?x1]
   28.23 +Rewriting:
   28.24 +rev [x] == rev [] @ [x]
   28.25 +Applying instance of rewrite rule:
   28.26 +rev [] == []
   28.27 +Rewriting:
   28.28 +rev [] == []
   28.29 +Applying instance of rewrite rule:
   28.30 +[] @ ?y == ?y
   28.31 +Rewriting:
   28.32 +[] @ [x] == [x]
   28.33 +Applying instance of rewrite rule:
   28.34 +?x3 \# ?t3 = ?t3 == False
   28.35 +Rewriting:
   28.36 +[x] = [] == False
   28.37 +\end{ttbox}
   28.38 +
   28.39 +In more complicated cases, the trace can quite lenghty, especially since
   28.40 +invocations of the simplifier are often nested (e.g.\ when solving conditions
   28.41 +of rewrite rules). Thus it is advisable to reset it:
   28.42 +*}
   28.43 +
   28.44 +ML "reset trace_simp";
   28.45 +
   28.46 +(*<*)
   28.47 +oops;
   28.48 +end
   28.49 +(*>*)
    29.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    29.2 +++ b/doc-src/TutorialI/Misc/types.thy	Wed Apr 19 11:56:31 2000 +0200
    29.3 @@ -0,0 +1,46 @@
    29.4 +(*<*)
    29.5 +theory "types" = Main:;
    29.6 +(*>*)types number       = nat
    29.7 +      gate         = "bool \\<Rightarrow> bool \\<Rightarrow> bool"
    29.8 +      ('a,'b)alist = "('a * 'b)list";
    29.9 +
   29.10 +text{*\noindent\indexbold{*types}%
   29.11 +Internally all synonyms are fully expanded.  As a consequence Isabelle's
   29.12 +output never contains synonyms.  Their main purpose is to improve the
   29.13 +readability of theory definitions.  Synonyms can be used just like any other
   29.14 +type:
   29.15 +*}
   29.16 +
   29.17 +consts nand :: gate
   29.18 +       exor :: gate;
   29.19 +
   29.20 +text{*
   29.21 +\subsection{Constant definitions}
   29.22 +\label{sec:ConstDefinitions}
   29.23 +\indexbold{definition}
   29.24 +
   29.25 +The above constants \isa{nand} and \isa{exor} are non-recursive and can
   29.26 +therefore be defined directly by
   29.27 +*}
   29.28 +
   29.29 +defs nand_def: "nand A B \\<equiv> \\<not>(A \\<and> B)"
   29.30 +     exor_def: "exor A B \\<equiv> A \\<and> \\<not>B \\<or> \\<not>A \\<and> B";
   29.31 +
   29.32 +text{*\noindent%
   29.33 +where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
   29.34 +\isa{exor_def} are arbitrary user-supplied names.
   29.35 +The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
   29.36 +that should only be used in constant definitions.
   29.37 +Declarations and definitions can also be merged
   29.38 +*}
   29.39 +
   29.40 +constdefs nor :: gate
   29.41 +         "nor A B \\<equiv> \\<not>(A \\<or> B)"
   29.42 +          exor2 :: gate
   29.43 +         "exor2 A B \\<equiv> (A \\<or> B) \\<and> (\\<not>A \\<or> \\<not>B)";
   29.44 +
   29.45 +text{*\noindent\indexbold{*constdefs}%
   29.46 +in which case the default name of each definition is \isa{$f$_def}, where
   29.47 +$f$ is the name of the defined constant.*}(*<*)
   29.48 +end
   29.49 +(*>*)
    30.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    30.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Wed Apr 19 11:56:31 2000 +0200
    30.3 @@ -0,0 +1,74 @@
    30.4 +(*<*)
    30.5 +theory Induction = examples + simplification:;
    30.6 +(*>*)
    30.7 +
    30.8 +text{*
    30.9 +Assuming we have defined our function such that Isabelle could prove
   30.10 +termination and that the recursion equations (or some suitable derived
   30.11 +equations) are simplification rules, we might like to prove something about
   30.12 +our function. Since the function is recursive, the natural proof principle is
   30.13 +again induction. But this time the structural form of induction that comes
   30.14 +with datatypes is unlikely to work well---otherwise we could have defined the
   30.15 +function by \isacommand{primrec}. Therefore \isacommand{recdef} automatically
   30.16 +proves a suitable induction rule $f$\isa{.induct} that follows the
   30.17 +recursion pattern of the particular function $f$. We call this
   30.18 +\textbf{recursion induction}. Roughly speaking, it
   30.19 +requires you to prove for each \isacommand{recdef} equation that the property
   30.20 +you are trying to establish holds for the left-hand side provided it holds
   30.21 +for all recursive calls on the right-hand side. Here is a simple example:
   30.22 +*}
   30.23 +
   30.24 +lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
   30.25 +
   30.26 +txt{*\noindent
   30.27 +involving the predefined \isa{map} functional on lists: \isa{map f xs}
   30.28 +is the result of applying \isa{f} to all elements of \isa{xs}. We prove
   30.29 +this lemma by recursion induction w.r.t. \isa{sep}:
   30.30 +*}
   30.31 +
   30.32 +apply(induct_tac x xs rule: sep.induct);
   30.33 +
   30.34 +txt{*\noindent
   30.35 +The resulting proof state has three subgoals corresponding to the three
   30.36 +clauses for \isa{sep}:
   30.37 +\begin{isabellepar}%
   30.38 +~1.~{\isasymAnd}a.~map~f~(sep~(a,~[]))~=~sep~(f~a,~map~f~[])\isanewline
   30.39 +~2.~{\isasymAnd}a~x.~map~f~(sep~(a,~[x]))~=~sep~(f~a,~map~f~[x])\isanewline
   30.40 +~3.~{\isasymAnd}a~x~y~zs.\isanewline
   30.41 +~~~~~~~map~f~(sep~(a,~y~\#~zs))~=~sep~(f~a,~map~f~(y~\#~zs))~{\isasymLongrightarrow}\isanewline
   30.42 +~~~~~~~map~f~(sep~(a,~x~\#~y~\#~zs))~=~sep~(f~a,~map~f~(x~\#~y~\#~zs))%
   30.43 +\end{isabellepar}%
   30.44 +The rest is pure simplification:
   30.45 +*}
   30.46 +
   30.47 +apply auto.;
   30.48 +
   30.49 +text{*
   30.50 +Try proving the above lemma by structural induction, and you find that you
   30.51 +need an additional case distinction. What is worse, the names of variables
   30.52 +are invented by Isabelle and have nothing to do with the names in the
   30.53 +definition of \isa{sep}.
   30.54 +
   30.55 +In general, the format of invoking recursion induction is
   30.56 +\begin{ttbox}
   30.57 +apply(induct_tac \(x@1 \dots x@n\) rule: \(f\).induct)
   30.58 +\end{ttbox}\index{*induct_tac}%
   30.59 +where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the
   30.60 +name of a function that takes an $n$-tuple. Usually the subgoal will
   30.61 +contain the term $f~x@1~\dots~x@n$ but this need not be the case. The
   30.62 +induction rules do not mention $f$ at all. For example \isa{sep.induct}
   30.63 +\begin{isabellepar}%
   30.64 +{\isasymlbrakk}~{\isasymAnd}a.~?P~a~[];\isanewline
   30.65 +~~{\isasymAnd}a~x.~?P~a~[x];\isanewline
   30.66 +~~{\isasymAnd}a~x~y~zs.~?P~a~(y~\#~zs)~{\isasymLongrightarrow}~?P~a~(x~\#~y~\#~zs){\isasymrbrakk}\isanewline
   30.67 +{\isasymLongrightarrow}~?P~?u~?v%
   30.68 +\end{isabellepar}%
   30.69 +merely says that in order to prove a property \isa{?P} of \isa{?u} and
   30.70 +\isa{?v} you need to prove it for the three cases where \isa{?v} is the
   30.71 +empty list, the singleton list, and the list with at least two elements
   30.72 +(in which case you may assume it holds for the tail of that list).
   30.73 +*}
   30.74 +
   30.75 +(*<*)
   30.76 +end
   30.77 +(*>*)
    31.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    31.2 +++ b/doc-src/TutorialI/Recdef/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
    31.3 @@ -0,0 +1,2 @@
    31.4 +use_thy "termination";
    31.5 +use_thy "Induction";
    32.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    32.2 +++ b/doc-src/TutorialI/Recdef/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
    32.3 @@ -0,0 +1,4 @@
    32.4 +\documentclass{article}
    32.5 +\begin{document}
    32.6 +xxx
    32.7 +\end{document}
    33.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    33.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Wed Apr 19 11:56:31 2000 +0200
    33.3 @@ -0,0 +1,92 @@
    33.4 +(*<*)
    33.5 +theory examples = Main:;
    33.6 +(*>*)
    33.7 +
    33.8 +text{*
    33.9 +Here is a simple example, the Fibonacci function:
   33.10 +*}
   33.11 +
   33.12 +consts fib :: "nat \\<Rightarrow> nat";
   33.13 +recdef fib "measure(\\<lambda>n. n)"
   33.14 +  "fib 0 = 0"
   33.15 +  "fib 1 = 1"
   33.16 +  "fib (Suc(Suc x)) = fib x + fib (Suc x)";
   33.17 +
   33.18 +text{*\noindent
   33.19 +The definition of \isa{fib} is accompanied by a \bfindex{measure function}
   33.20 +\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
   33.21 +natural number. The requirement is that in each equation the measure of the
   33.22 +argument on the left-hand side is strictly greater than the measure of the
   33.23 +argument of each recursive call. In the case of \isa{fib} this is
   33.24 +obviously true because the measure function is the identity and
   33.25 +\isa{Suc(Suc~x)} is strictly greater than both \isa{x} and
   33.26 +\isa{Suc~x}.
   33.27 +
   33.28 +Slightly more interesting is the insertion of a fixed element
   33.29 +between any two elements of a list:
   33.30 +*}
   33.31 +
   33.32 +consts sep :: "'a * 'a list \\<Rightarrow> 'a list";
   33.33 +recdef sep "measure (\\<lambda>(a,xs). length xs)"
   33.34 +  "sep(a, [])     = []"
   33.35 +  "sep(a, [x])    = [x]"
   33.36 +  "sep(a, x#y#zs) = x # a # sep(a,y#zs)";
   33.37 +
   33.38 +text{*\noindent
   33.39 +This time the measure is the length of the list, which decreases with the
   33.40 +recursive call; the first component of the argument tuple is irrelevant.
   33.41 +
   33.42 +Pattern matching need not be exhaustive:
   33.43 +*}
   33.44 +
   33.45 +consts last :: "'a list \\<Rightarrow> 'a";
   33.46 +recdef last "measure (\\<lambda>xs. length xs)"
   33.47 +  "last [x]      = x"
   33.48 +  "last (x#y#zs) = last (y#zs)";
   33.49 +
   33.50 +text{*
   33.51 +Overlapping patterns are disambiguated by taking the order of equations into
   33.52 +account, just as in functional programming:
   33.53 +*}
   33.54 +
   33.55 +consts sep1 :: "'a * 'a list \\<Rightarrow> 'a list";
   33.56 +recdef sep1 "measure (\\<lambda>(a,xs). length xs)"
   33.57 +  "sep1(a, x#y#zs) = x # a # sep1(a,y#zs)"
   33.58 +  "sep1(a, xs)     = xs";
   33.59 +
   33.60 +text{*\noindent
   33.61 +This defines exactly the same function as \isa{sep} above, i.e.\
   33.62 +\isa{sep1 = sep}.
   33.63 +
   33.64 +\begin{warn}
   33.65 +  \isacommand{recdef} only takes the first argument of a (curried)
   33.66 +  recursive function into account. This means both the termination measure
   33.67 +  and pattern matching can only use that first argument. In general, you will
   33.68 +  therefore have to combine several arguments into a tuple. In case only one
   33.69 +  argument is relevant for termination, you can also rearrange the order of
   33.70 +  arguments as in the following definition:
   33.71 +\end{warn}
   33.72 +*}
   33.73 +consts sep2 :: "'a list \\<Rightarrow> 'a \\<Rightarrow> 'a list";
   33.74 +recdef sep2 "measure length"
   33.75 +  "sep2 (x#y#zs) = (\\<lambda>a. x # a # sep2 zs a)"
   33.76 +  "sep2 xs       = (\\<lambda>a. xs)";
   33.77 +
   33.78 +text{*
   33.79 +Because of its pattern-matching syntax, \isacommand{recdef} is also useful
   33.80 +for the definition of non-recursive functions:
   33.81 +*}
   33.82 +
   33.83 +consts swap12 :: "'a list \\<Rightarrow> 'a list";
   33.84 +recdef swap12 "{}"
   33.85 +  "swap12 (x#y#zs) = y#x#zs"
   33.86 +  "swap12 zs       = zs";
   33.87 +
   33.88 +text{*\noindent
   33.89 +In the non-recursive case the termination measure degenerates to the empty
   33.90 +set \isa{\{\}}.
   33.91 +*}
   33.92 +
   33.93 +(*<*)
   33.94 +end
   33.95 +(*>*)
    34.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    34.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Wed Apr 19 11:56:31 2000 +0200
    34.3 @@ -0,0 +1,105 @@
    34.4 +(*<*)
    34.5 +theory simplification = Main:;
    34.6 +(*>*)
    34.7 +
    34.8 +text{*
    34.9 +Once we have succeeded in proving all termination conditions, the recursion
   34.10 +equations become simplification rules, just as with
   34.11 +\isacommand{primrec}. In most cases this works fine, but there is a subtle
   34.12 +problem that must be mentioned: simplification may not
   34.13 +terminate because of automatic splitting of \isa{if}.
   34.14 +Let us look at an example:
   34.15 +*}
   34.16 +
   34.17 +consts gcd :: "nat*nat \\<Rightarrow> nat";
   34.18 +recdef gcd "measure (\\<lambda>(m,n).n)"
   34.19 +  "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))";
   34.20 +
   34.21 +text{*\noindent
   34.22 +According to the measure function, the second argument should decrease with
   34.23 +each recursive call. The resulting termination condition
   34.24 +*}
   34.25 +
   34.26 +(*<*)term(*>*) "n \\<noteq> 0 \\<Longrightarrow> m mod n < n";
   34.27 +
   34.28 +text{*\noindent
   34.29 +is provded automatically because it is already present as a lemma in the
   34.30 +arithmetic library. Thus the recursion equation becomes a simplification
   34.31 +rule. Of course the equation is nonterminating if we are allowed to unfold
   34.32 +the recursive call inside the \isa{else} branch, which is why programming
   34.33 +languages and our simplifier don't do that. Unfortunately the simplifier does
   34.34 +something else which leads to the same problem: it splits \isa{if}s if the
   34.35 +condition simplifies to neither \isa{True} nor \isa{False}. For
   34.36 +example, simplification reduces
   34.37 +*}
   34.38 +
   34.39 +(*<*)term(*>*) "gcd(m,n) = k";
   34.40 +
   34.41 +text{*\noindent
   34.42 +in one step to
   34.43 +*}
   34.44 +
   34.45 +(*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k";
   34.46 +
   34.47 +text{*\noindent
   34.48 +where the condition cannot be reduced further, and splitting leads to
   34.49 +*}
   34.50 +
   34.51 +(*<*)term(*>*) "(n=0 \\<longrightarrow> m=k) \\<and> (n\\<noteq>0 \\<longrightarrow> gcd(n, m mod n)=k)";
   34.52 +
   34.53 +text{*\noindent
   34.54 +Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
   34.55 +an \isa{if}, this leads to an infinite chain of simplification steps.
   34.56 +Fortunately, this problem can be avoided in many different ways.
   34.57 +
   34.58 +Of course the most radical solution is to disable the offending
   34.59 +\isa{split_if} as shown in the section on case splits in
   34.60 +\S\ref{sec:SimpFeatures}.
   34.61 +However, we do not recommend this because it means you will often have to
   34.62 +invoke the rule explicitly when \isa{if} is involved.
   34.63 +
   34.64 +If possible, the definition should be given by pattern matching on the left
   34.65 +rather than \isa{if} on the right. In the case of \isa{gcd} the
   34.66 +following alternative definition suggests itself:
   34.67 +*}
   34.68 +
   34.69 +consts gcd1 :: "nat*nat \\<Rightarrow> nat";
   34.70 +recdef gcd1 "measure (\\<lambda>(m,n).n)"
   34.71 +  "gcd1 (m, 0) = m"
   34.72 +  "gcd1 (m, n) = gcd1(n, m mod n)";
   34.73 +
   34.74 +
   34.75 +text{*\noindent
   34.76 +Note that the order of equations is important and hides the side condition
   34.77 +\isa{n \isasymnoteq\ 0}. Unfortunately, in general the case distinction
   34.78 +may not be expressible by pattern matching.
   34.79 +
   34.80 +A very simple alternative is to replace \isa{if} by \isa{case}, which
   34.81 +is also available for \isa{bool} but is not split automatically:
   34.82 +*}
   34.83 +
   34.84 +consts gcd2 :: "nat*nat \\<Rightarrow> nat";
   34.85 +recdef gcd2 "measure (\\<lambda>(m,n).n)"
   34.86 +  "gcd2(m,n) = (case n=0 of True \\<Rightarrow> m | False \\<Rightarrow> gcd2(n,m mod n))";
   34.87 +
   34.88 +text{*\noindent
   34.89 +In fact, this is probably the neatest solution next to pattern matching.
   34.90 +
   34.91 +A final alternative is to replace the offending simplification rules by
   34.92 +derived conditional ones. For \isa{gcd} it means we have to prove
   34.93 +*}
   34.94 +
   34.95 +lemma [simp]: "gcd (m, 0) = m";
   34.96 +apply(simp).;
   34.97 +lemma [simp]: "n \\<noteq> 0 \\<Longrightarrow> gcd(m, n) = gcd(n, m mod n)";
   34.98 +apply(simp).;
   34.99 +
  34.100 +text{*\noindent
  34.101 +after which we can disable the original simplification rule:
  34.102 +*}
  34.103 +
  34.104 +lemmas [simp del] = gcd.simps;
  34.105 +
  34.106 +(*<*)
  34.107 +end
  34.108 +(*>*)
    35.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    35.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Wed Apr 19 11:56:31 2000 +0200
    35.3 @@ -0,0 +1,102 @@
    35.4 +(*<*)
    35.5 +theory termination = Main:;
    35.6 +(*>*)
    35.7 +
    35.8 +text{*
    35.9 +When a function is defined via \isacommand{recdef}, Isabelle tries to prove
   35.10 +its termination with the help of the user-supplied measure.  All of the above
   35.11 +examples are simple enough that Isabelle can prove automatically that the
   35.12 +measure of the argument goes down in each recursive call. In that case
   35.13 +$f$.\isa{simps} contains the defining equations (or variants derived from
   35.14 +them) as theorems. For example, look (via \isacommand{thm}) at
   35.15 +\isa{sep.simps} and \isa{sep1.simps} to see that they define the same
   35.16 +function. What is more, those equations are automatically declared as
   35.17 +simplification rules.
   35.18 +
   35.19 +In general, Isabelle may not be able to prove all termination condition
   35.20 +(there is one for each recursive call) automatically. For example,
   35.21 +termination of the following artificial function
   35.22 +*}
   35.23 +
   35.24 +consts f :: "nat*nat \\<Rightarrow> nat";
   35.25 +recdef f "measure(\\<lambda>(x,y). x-y)"
   35.26 +  "f(x,y) = (if x \\<le> y then x else f(x,y+1))";
   35.27 +
   35.28 +text{*\noindent
   35.29 +is not proved automatically (although maybe it should be). Isabelle prints a
   35.30 +kind of error message showing you what it was unable to prove. You will then
   35.31 +have to prove it as a separate lemma before you attempt the definition
   35.32 +of your function once more. In our case the required lemma is the obvious one:
   35.33 +*}
   35.34 +
   35.35 +lemma termi_lem[simp]: "\\<not> x \\<le> y \\<Longrightarrow> x - Suc y < x - y";
   35.36 +
   35.37 +txt{*\noindent
   35.38 +It was not proved automatically because of the special nature of \isa{-}
   35.39 +on \isa{nat}. This requires more arithmetic than is tried by default:
   35.40 +*}
   35.41 +
   35.42 +apply(arith).;
   35.43 +
   35.44 +text{*\noindent
   35.45 +Because \isacommand{recdef}'s the termination prover involves simplification,
   35.46 +we have declared our lemma a simplification rule. Therefore our second
   35.47 +attempt to define our function will automatically take it into account:
   35.48 +*}
   35.49 +
   35.50 +consts g :: "nat*nat \\<Rightarrow> nat";
   35.51 +recdef g "measure(\\<lambda>(x,y). x-y)"
   35.52 +  "g(x,y) = (if x \\<le> y then x else g(x,y+1))";
   35.53 +
   35.54 +text{*\noindent
   35.55 +This time everything works fine. Now \isa{g.simps} contains precisely the
   35.56 +stated recursion equation for \isa{g} and they are simplification
   35.57 +rules. Thus we can automatically prove
   35.58 +*}
   35.59 +
   35.60 +theorem wow: "g(1,0) = g(1,1)";
   35.61 +apply(simp).;
   35.62 +
   35.63 +text{*\noindent
   35.64 +More exciting theorems require induction, which is discussed below.
   35.65 +
   35.66 +Because lemma \isa{termi_lem} above was only turned into a
   35.67 +simplification rule for the sake of the termination proof, we may want to
   35.68 +disable it again:
   35.69 +*}
   35.70 +
   35.71 +lemmas [simp del] = termi_lem;
   35.72 +
   35.73 +text{*
   35.74 +The attentive reader may wonder why we chose to call our function \isa{g}
   35.75 +rather than \isa{f} the second time around. The reason is that, despite
   35.76 +the failed termination proof, the definition of \isa{f} did not
   35.77 +fail (and thus we could not define it a second time). However, all theorems
   35.78 +about \isa{f}, for example \isa{f.simps}, carry as a precondition the
   35.79 +unproved termination condition. Moreover, the theorems \isa{f.simps} are
   35.80 +not simplification rules. However, this mechanism allows a delayed proof of
   35.81 +termination: instead of proving \isa{termi_lem} up front, we could prove
   35.82 +it later on and then use it to remove the preconditions from the theorems
   35.83 +about \isa{f}. In most cases this is more cumbersome than proving things
   35.84 +up front
   35.85 +%FIXME, with one exception: nested recursion.
   35.86 +
   35.87 +Although all the above examples employ measure functions, \isacommand{recdef}
   35.88 +allows arbitrary wellfounded relations. For example, termination of
   35.89 +Ackermann's function requires the lexicographic product \isa{<*lex*>}:
   35.90 +*}
   35.91 +
   35.92 +consts ack :: "nat*nat \\<Rightarrow> nat";
   35.93 +recdef ack "measure(%m. m) <*lex*> measure(%n. n)"
   35.94 +  "ack(0,n)         = Suc n"
   35.95 +  "ack(Suc m,0)     = ack(m, 1)"
   35.96 +  "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
   35.97 +
   35.98 +text{*\noindent
   35.99 +For details see the manual~\cite{isabelle-HOL} and the examples in the
  35.100 +library.
  35.101 +*}
  35.102 +
  35.103 +(*<*)
  35.104 +end
  35.105 +(*>*)
    36.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    36.2 +++ b/doc-src/TutorialI/ToyList/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
    36.3 @@ -0,0 +1,2 @@
    36.4 +use_thy "ToyList";
    36.5 +
    37.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    37.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Wed Apr 19 11:56:31 2000 +0200
    37.3 @@ -0,0 +1,354 @@
    37.4 +theory ToyList = PreList:
    37.5 +
    37.6 +text{*\noindent
    37.7 +HOL already has a predefined theory of lists called \texttt{List} ---
    37.8 +\texttt{ToyList} is merely a small fragment of it chosen as an example. In
    37.9 +contrast to what is recommended in \S\ref{sec:Basic:Theories},
   37.10 +\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a
   37.11 +theory that contains pretty much everything but lists, thus avoiding
   37.12 +ambiguities caused by defining lists twice.
   37.13 +*}
   37.14 +
   37.15 +datatype 'a list = Nil                          ("[]")
   37.16 +                 | Cons 'a "'a list"            (infixr "#" 65);
   37.17 +
   37.18 +text{*\noindent
   37.19 +The datatype\index{*datatype} \isaindexbold{list} introduces two
   37.20 +constructors \isaindexbold{Nil} and \isaindexbold{Cons}, the
   37.21 +empty list and the operator that adds an element to the front of a list. For
   37.22 +example, the term \isa{Cons True (Cons   False Nil)} is a value of type
   37.23 +\isa{bool~list}, namely the list with the elements \isa{True} and
   37.24 +\isa{False}. Because this notation becomes unwieldy very quickly, the
   37.25 +datatype declaration is annotated with an alternative syntax: instead of
   37.26 +\isa{Nil} and \isa{Cons~$x$~$xs$} we can write
   37.27 +\isa{[]}\index{$HOL2list@\texttt{[]}|bold} and
   37.28 +\isa{$x$~\#~$xs$}\index{$HOL2list@\texttt{\#}|bold}. In fact, this
   37.29 +alternative syntax is the standard syntax. Thus the list \isa{Cons True
   37.30 +(Cons False Nil)} becomes \isa{True \# False \# []}. The annotation
   37.31 +\isacommand{infixr}\indexbold{*infixr} means that \isa{\#} associates to
   37.32 +the right, i.e.\ the term \isa{$x$ \# $y$ \# $z$} is read as \isa{$x$
   37.33 +\# ($y$ \# $z$)} and not as \isa{($x$ \# $y$) \# $z$}.
   37.34 +
   37.35 +\begin{warn}
   37.36 +  Syntax annotations are a powerful but completely optional feature. You
   37.37 +  could drop them from theory \texttt{ToyList} and go back to the identifiers
   37.38 +  \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
   37.39 +  that their syntax is highly customized. We recommend that novices should
   37.40 +  not use syntax annotations in their own theories.
   37.41 +\end{warn}
   37.42 +Next, two functions \isa{app} and \isaindexbold{rev} are declared:
   37.43 +*}
   37.44 +
   37.45 +consts app :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list"   (infixr "@" 65)
   37.46 +       rev :: "'a list \\<Rightarrow> 'a list";
   37.47 +
   37.48 +text{*
   37.49 +\noindent
   37.50 +In contrast to ML, Isabelle insists on explicit declarations of all functions
   37.51 +(keyword \isacommand{consts}).  (Apart from the declaration-before-use
   37.52 +restriction, the order of items in a theory file is unconstrained.) Function
   37.53 +\isa{app} is annotated with concrete syntax too. Instead of the prefix
   37.54 +syntax \isa{app~$xs$~$ys$} the infix
   37.55 +\isa{$xs$~\at~$ys$}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred
   37.56 +form. Both functions are defined recursively:
   37.57 +*}
   37.58 +
   37.59 +primrec
   37.60 +"[] @ ys       = ys"
   37.61 +"(x # xs) @ ys = x # (xs @ ys)";
   37.62 +
   37.63 +primrec
   37.64 +"rev []        = []"
   37.65 +"rev (x # xs)  = (rev xs) @ (x # [])";
   37.66 +
   37.67 +text{*
   37.68 +\noindent
   37.69 +The equations for \isa{app} and \isa{rev} hardly need comments:
   37.70 +\isa{app} appends two lists and \isa{rev} reverses a list.  The keyword
   37.71 +\isacommand{primrec}\index{*primrec} indicates that the recursion is of a
   37.72 +particularly primitive kind where each recursive call peels off a datatype
   37.73 +constructor from one of the arguments (see \S\ref{sec:datatype}).  Thus the
   37.74 +recursion always terminates, i.e.\ the function is \bfindex{total}.
   37.75 +
   37.76 +The termination requirement is absolutely essential in HOL, a logic of total
   37.77 +functions. If we were to drop it, inconsistencies would quickly arise: the
   37.78 +``definition'' $f(n) = f(n)+1$ immediately leads to $0 = 1$ by subtracting
   37.79 +$f(n)$ on both sides.
   37.80 +% However, this is a subtle issue that we cannot discuss here further.
   37.81 +
   37.82 +\begin{warn}
   37.83 +  As we have indicated, the desire for total functions is not a gratuitously
   37.84 +  imposed restriction but an essential characteristic of HOL. It is only
   37.85 +  because of totality that reasoning in HOL is comparatively easy.  More
   37.86 +  generally, the philosophy in HOL is not to allow arbitrary axioms (such as
   37.87 +  function definitions whose totality has not been proved) because they
   37.88 +  quickly lead to inconsistencies. Instead, fixed constructs for introducing
   37.89 +  types and functions are offered (such as \isacommand{datatype} and
   37.90 +  \isacommand{primrec}) which are guaranteed to preserve consistency.
   37.91 +\end{warn}
   37.92 +
   37.93 +A remark about syntax.  The textual definition of a theory follows a fixed
   37.94 +syntax with keywords like \isacommand{datatype} and \isacommand{end} (see
   37.95 +Fig.~\ref{fig:keywords} in Appendix~\ref{sec:Appendix} for a full list).
   37.96 +Embedded in this syntax are the types and formulae of HOL, whose syntax is
   37.97 +extensible, e.g.\ by new user-defined infix operators
   37.98 +(see~\ref{sec:infix-syntax}). To distinguish the two levels, everything
   37.99 +HOL-specific (terms and types) should be enclosed in
  37.100 +\texttt{"}\dots\texttt{"}. 
  37.101 +To lessen this burden, quotation marks around a single identifier can be
  37.102 +dropped, unless the identifier happens to be a keyword, as in
  37.103 +*}
  37.104 +
  37.105 +consts "end" :: "'a list \\<Rightarrow> 'a"
  37.106 +
  37.107 +text{*\noindent
  37.108 +When Isabelle prints a syntax error message, it refers to the HOL syntax as
  37.109 +the \bfindex{inner syntax}.
  37.110 +
  37.111 +
  37.112 +\section{An introductory proof}
  37.113 +\label{sec:intro-proof}
  37.114 +
  37.115 +Assuming you have input the declarations and definitions of \texttt{ToyList}
  37.116 +presented so far, we are ready to prove a few simple theorems. This will
  37.117 +illustrate not just the basic proof commands but also the typical proof
  37.118 +process.
  37.119 +
  37.120 +\subsubsection*{Main goal: \texttt{rev(rev xs) = xs}}
  37.121 +
  37.122 +Our goal is to show that reversing a list twice produces the original
  37.123 +list. The input line
  37.124 +*}
  37.125 +
  37.126 +theorem rev_rev [simp]: "rev(rev xs) = xs";
  37.127 +
  37.128 +txt{*\noindent\index{*theorem|bold}\index{*simp (attribute)|bold}
  37.129 +\begin{itemize}
  37.130 +\item
  37.131 +establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
  37.132 +\item
  37.133 +gives that theorem the name \isa{rev_rev} by which it can be referred to,
  37.134 +\item
  37.135 +and tells Isabelle (via \isa{[simp]}) to use the theorem (once it has been
  37.136 +proved) as a simplification rule, i.e.\ all future proofs involving
  37.137 +simplification will replace occurrences of \isa{rev(rev xs)} by
  37.138 +\isa{xs}.
  37.139 +
  37.140 +The name and the simplification attribute are optional.
  37.141 +\end{itemize}
  37.142 +Isabelle's response is to print
  37.143 +\begin{isabellepar}%
  37.144 +proof(prove):~step~0\isanewline
  37.145 +\isanewline
  37.146 +goal~(theorem~rev\_rev):\isanewline
  37.147 +rev~(rev~xs)~=~xs\isanewline
  37.148 +~1.~rev~(rev~xs)~=~xs
  37.149 +\end{isabellepar}%
  37.150 +The first three lines tell us that we are 0 steps into the proof of
  37.151 +theorem \isa{rev_rev}; for compactness reasons we rarely show these
  37.152 +initial lines in this tutorial. The remaining lines display the current
  37.153 +proof state.
  37.154 +Until we have finished a proof, the proof state always looks like this:
  37.155 +\begin{isabellepar}%
  37.156 +$G$\isanewline
  37.157 +~1.~$G\sb{1}$\isanewline
  37.158 +~~\vdots~~\isanewline
  37.159 +~$n$.~$G\sb{n}$
  37.160 +\end{isabellepar}%
  37.161 +where $G$
  37.162 +is the overall goal that we are trying to prove, and the numbered lines
  37.163 +contain the subgoals $G\sb{1}$, \dots, $G\sb{n}$ that we need to prove to
  37.164 +establish $G$. At \isa{step 0} there is only one subgoal, which is
  37.165 +identical with the overall goal.  Normally $G$ is constant and only serves as
  37.166 +a reminder. Hence we rarely show it in this tutorial.
  37.167 +
  37.168 +Let us now get back to \isa{rev(rev xs) = xs}. Properties of recursively
  37.169 +defined functions are best established by induction. In this case there is
  37.170 +not much choice except to induct on \isa{xs}:
  37.171 +*}
  37.172 +
  37.173 +apply(induct_tac xs);
  37.174 +
  37.175 +txt{*\noindent\index{*induct_tac}%
  37.176 +This tells Isabelle to perform induction on variable \isa{xs}. The suffix
  37.177 +\isa{tac} stands for ``tactic'', a synonym for ``theorem proving function''.
  37.178 +By default, induction acts on the first subgoal. The new proof state contains
  37.179 +two subgoals, namely the base case (\isa{Nil}) and the induction step
  37.180 +(\isa{Cons}):
  37.181 +\begin{isabellepar}%
  37.182 +~1.~rev~(rev~[])~=~[]\isanewline
  37.183 +~2.~{\isasymAnd}a~list.~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev(a~\#~list))~=~a~\#~list%
  37.184 +\end{isabellepar}%
  37.185 +
  37.186 +The induction step is an example of the general format of a subgoal:
  37.187 +\begin{isabellepar}%
  37.188 +~$i$.~{\indexboldpos{\isasymAnd}{$IsaAnd}}$x\sb{1}$~\dots~$x\sb{n}$.~{\it assumptions}~{\isasymLongrightarrow}~{\it conclusion}
  37.189 +\end{isabellepar}%
  37.190 +The prefix of bound variables \isasymAnd$x\sb{1}$~\dots~$x\sb{n}$ can be
  37.191 +ignored most of the time, or simply treated as a list of variables local to
  37.192 +this subgoal. Their deeper significance is explained in \S\ref{sec:PCproofs}.
  37.193 +The {\it assumptions} are the local assumptions for this subgoal and {\it
  37.194 +  conclusion} is the actual proposition to be proved. Typical proof steps
  37.195 +that add new assumptions are induction or case distinction. In our example
  37.196 +the only assumption is the induction hypothesis \isa{rev (rev list) =
  37.197 +  list}, where \isa{list} is a variable name chosen by Isabelle. If there
  37.198 +are multiple assumptions, they are enclosed in the bracket pair
  37.199 +\indexboldpos{\isasymlbrakk}{$Isabrl} and
  37.200 +\indexboldpos{\isasymrbrakk}{$Isabrr} and separated by semicolons.
  37.201 +
  37.202 +%FIXME indent!
  37.203 +Let us try to solve both goals automatically:
  37.204 +*}
  37.205 +
  37.206 +apply(auto);
  37.207 +
  37.208 +txt{*\noindent
  37.209 +This command tells Isabelle to apply a proof strategy called
  37.210 +\isa{auto} to all subgoals. Essentially, \isa{auto} tries to
  37.211 +``simplify'' the subgoals.  In our case, subgoal~1 is solved completely (thanks
  37.212 +to the equation \isa{rev [] = []}) and disappears; the simplified version
  37.213 +of subgoal~2 becomes the new subgoal~1:
  37.214 +\begin{isabellepar}%
  37.215 +~1.~\dots~rev(rev~list)~=~list~{\isasymLongrightarrow}~rev(rev~list~@~a~\#~[])~=~a~\#~list
  37.216 +\end{isabellepar}%
  37.217 +In order to simplify this subgoal further, a lemma suggests itself.
  37.218 +*}
  37.219 +(*<*)
  37.220 +oops
  37.221 +(*>*)
  37.222 +
  37.223 +text{*
  37.224 +\subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
  37.225 +
  37.226 +After abandoning the above proof attempt (at the shell level type
  37.227 +\isa{oops}) we start a new proof:
  37.228 +*}
  37.229 +
  37.230 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
  37.231 +
  37.232 +txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and
  37.233 +\isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate
  37.234 +the importance we attach to a proposition. In general, we use the words
  37.235 +\emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
  37.236 +interchangeably.
  37.237 +
  37.238 +%FIXME indent!
  37.239 +There are two variables that we could induct on: \isa{xs} and
  37.240 +\isa{ys}. Because \isa{\at} is defined by recursion on
  37.241 +the first argument, \isa{xs} is the correct one:
  37.242 +*}
  37.243 +
  37.244 +apply(induct_tac xs);
  37.245 +
  37.246 +txt{*\noindent
  37.247 +This time not even the base case is solved automatically:
  37.248 +*}
  37.249 +
  37.250 +apply(auto);
  37.251 +
  37.252 +txt{*
  37.253 +\begin{isabellepar}%
  37.254 +~1.~rev~ys~=~rev~ys~@~[]\isanewline
  37.255 +~2. \dots
  37.256 +\end{isabellepar}%
  37.257 +We need to cancel this proof attempt and prove another simple lemma first.
  37.258 +In the future the step of cancelling an incomplete proof before embarking on
  37.259 +the proof of a lemma often remains implicit.
  37.260 +*}
  37.261 +(*<*)
  37.262 +oops
  37.263 +(*>*)
  37.264 +
  37.265 +text{*
  37.266 +\subsubsection*{Second lemma: \texttt{xs \at~[] = xs}}
  37.267 +
  37.268 +This time the canonical proof procedure
  37.269 +*}
  37.270 +
  37.271 +lemma app_Nil2 [simp]: "xs @ [] = xs";
  37.272 +apply(induct_tac xs);
  37.273 +apply(auto);
  37.274 +
  37.275 +txt{*
  37.276 +\noindent
  37.277 +leads to the desired message \isa{No subgoals!}:
  37.278 +\begin{isabellepar}%
  37.279 +xs~@~[]~=~xs\isanewline
  37.280 +No~subgoals!
  37.281 +\end{isabellepar}%
  37.282 +
  37.283 +We still need to confirm that the proof is now finished:
  37.284 +*}
  37.285 +
  37.286 +.
  37.287 +
  37.288 +text{*\noindent\indexbold{$Isar@\texttt{.}}%
  37.289 +As a result of that final dot, Isabelle associates the lemma
  37.290 +just proved with its name. Notice that in the lemma \isa{app_Nil2} (as
  37.291 +printed out after the final dot) the free variable \isa{xs} has been
  37.292 +replaced by the unknown \isa{?xs}, just as explained in
  37.293 +\S\ref{sec:variables}.
  37.294 +
  37.295 +Going back to the proof of the first lemma
  37.296 +*}
  37.297 +
  37.298 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
  37.299 +apply(induct_tac xs);
  37.300 +apply(auto);
  37.301 +
  37.302 +txt{*
  37.303 +\noindent
  37.304 +we find that this time \isa{auto} solves the base case, but the
  37.305 +induction step merely simplifies to
  37.306 +\begin{isabellepar}
  37.307 +~1.~{\isasymAnd}a~list.\isanewline
  37.308 +~~~~~~~rev~(list~@~ys)~=~rev~ys~@~rev~list~{\isasymLongrightarrow}\isanewline
  37.309 +~~~~~~~(rev~ys~@~rev~list)~@~a~\#~[]~=~rev~ys~@~rev~list~@~a~\#~[]
  37.310 +\end{isabellepar}%
  37.311 +Now we need to remember that \isa{\at} associates to the right, and that
  37.312 +\isa{\#} and \isa{\at} have the same priority (namely the \isa{65}
  37.313 +in their \isacommand{infixr} annotation). Thus the conclusion really is
  37.314 +\begin{isabellepar}%
  37.315 +~~~~~(rev~ys~@~rev~list)~@~(a~\#~[])~=~rev~ys~@~(rev~list~@~(a~\#~[]))%
  37.316 +\end{isabellepar}%
  37.317 +and the missing lemma is associativity of \isa{\at}.
  37.318 +
  37.319 +\subsubsection*{Third lemma: \texttt{(xs \at~ys) \at~zs = xs \at~(ys \at~zs)}}
  37.320 +
  37.321 +Abandoning the previous proof, the canonical proof procedure
  37.322 +*}
  37.323 +
  37.324 +
  37.325 +txt_raw{*\begin{comment}*}
  37.326 +oops
  37.327 +text_raw{*\end{comment}*}
  37.328 +
  37.329 +lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)";
  37.330 +apply(induct_tac xs);
  37.331 +apply(auto).;
  37.332 +
  37.333 +text{*
  37.334 +\noindent
  37.335 +succeeds without further ado.
  37.336 +
  37.337 +Now we can go back and prove the first lemma
  37.338 +*}
  37.339 +
  37.340 +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
  37.341 +apply(induct_tac xs);
  37.342 +apply(auto).;
  37.343 +
  37.344 +text{*\noindent
  37.345 +and then solve our main theorem:
  37.346 +*}
  37.347 +
  37.348 +theorem rev_rev [simp]: "rev(rev xs) = xs";
  37.349 +apply(induct_tac xs);
  37.350 +apply(auto).;
  37.351 +
  37.352 +text{*\noindent
  37.353 +The final \isa{end} tells Isabelle to close the current theory because
  37.354 +we are finished with its development:
  37.355 +*}
  37.356 +
  37.357 +end
    38.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    38.2 +++ b/doc-src/TutorialI/ToyList/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
    38.3 @@ -0,0 +1,3 @@
    38.4 +\documentclass{article}
    38.5 +\begin{document}
    38.6 +\end{document}
    39.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    39.2 +++ b/doc-src/TutorialI/ToyList2/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
    39.3 @@ -0,0 +1,1 @@
    39.4 +use_thy "ToyList";
    40.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    40.2 +++ b/doc-src/TutorialI/Trie/Option2.thy	Wed Apr 19 11:56:31 2000 +0200
    40.3 @@ -0,0 +1,9 @@
    40.4 +(*<*)
    40.5 +theory Option2 = Main:;
    40.6 +(*>*)
    40.7 +
    40.8 +datatype 'a option = None | Some 'a
    40.9 +
   40.10 +(*<*)
   40.11 +end
   40.12 +(*>*)
    41.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    41.2 +++ b/doc-src/TutorialI/Trie/ROOT.ML	Wed Apr 19 11:56:31 2000 +0200
    41.3 @@ -0,0 +1,2 @@
    41.4 +use_thy "Option2";
    41.5 +use_thy "Trie";
    42.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    42.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Wed Apr 19 11:56:31 2000 +0200
    42.3 @@ -0,0 +1,144 @@
    42.4 +(*<*)
    42.5 +theory Trie = Main:;
    42.6 +(*>*)
    42.7 +
    42.8 +text{*
    42.9 +To minimize running time, each node of a trie should contain an array that maps
   42.10 +letters to subtries. We have chosen a (sometimes) more space efficient
   42.11 +representation where the subtries are held in an association list, i.e.\ a
   42.12 +list of (letter,trie) pairs.  Abstracting over the alphabet \isa{'a} and the
   42.13 +values \isa{'v} we define a trie as follows:
   42.14 +*}
   42.15 +
   42.16 +datatype ('a,'v)trie = Trie  "'v option"  "('a * ('a,'v)trie)list";
   42.17 +
   42.18 +text{*\noindent
   42.19 +The first component is the optional value, the second component the
   42.20 +association list of subtries.  This is an example of nested recursion involving products,
   42.21 +which is fine because products are datatypes as well.
   42.22 +We define two selector functions:
   42.23 +*}
   42.24 +
   42.25 +consts value :: "('a,'v)trie \\<Rightarrow> 'v option"
   42.26 +       alist :: "('a,'v)trie \\<Rightarrow> ('a * ('a,'v)trie)list";
   42.27 +primrec "value(Trie ov al) = ov";
   42.28 +primrec "alist(Trie ov al) = al";
   42.29 +
   42.30 +text{*\noindent
   42.31 +Association lists come with a generic lookup function:
   42.32 +*}
   42.33 +
   42.34 +consts   assoc :: "('key * 'val)list \\<Rightarrow> 'key \\<Rightarrow> 'val option";
   42.35 +primrec "assoc [] x = None"
   42.36 +        "assoc (p#ps) x =
   42.37 +           (let (a,b) = p in if a=x then Some b else assoc ps x)";
   42.38 +
   42.39 +text{*
   42.40 +Now we can define the lookup function for tries. It descends into the trie
   42.41 +examining the letters of the search string one by one. As
   42.42 +recursion on lists is simpler than on tries, let us express this as primitive
   42.43 +recursion on the search string argument:
   42.44 +*}
   42.45 +
   42.46 +consts   lookup :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v option";
   42.47 +primrec "lookup t [] = value t"
   42.48 +        "lookup t (a#as) = (case assoc (alist t) a of
   42.49 +                              None \\<Rightarrow> None
   42.50 +                            | Some at \\<Rightarrow> lookup at as)";
   42.51 +
   42.52 +text{*
   42.53 +As a first simple property we prove that looking up a string in the empty
   42.54 +trie \isa{Trie~None~[]} always returns \isa{None}. The proof merely
   42.55 +distinguishes the two cases whether the search string is empty or not:
   42.56 +*}
   42.57 +
   42.58 +lemma [simp]: "lookup (Trie None []) as = None";
   42.59 +apply(cases "as", auto).;
   42.60 +
   42.61 +text{*
   42.62 +Things begin to get interesting with the definition of an update function
   42.63 +that adds a new (string,value) pair to a trie, overwriting the old value
   42.64 +associated with that string:
   42.65 +*}
   42.66 +
   42.67 +consts update :: "('a,'v)trie \\<Rightarrow> 'a list \\<Rightarrow> 'v \\<Rightarrow> ('a,'v)trie";
   42.68 +primrec
   42.69 +  "update t []     v = Trie (Some v) (alist t)"
   42.70 +  "update t (a#as) v =
   42.71 +     (let tt = (case assoc (alist t) a of
   42.72 +                  None \\<Rightarrow> Trie None [] | Some at \\<Rightarrow> at)
   42.73 +      in Trie (value t) ((a,update tt as v)#alist t))";
   42.74 +
   42.75 +text{*\noindent
   42.76 +The base case is obvious. In the recursive case the subtrie
   42.77 +\isa{tt} associated with the first letter \isa{a} is extracted,
   42.78 +recursively updated, and then placed in front of the association list.
   42.79 +The old subtrie associated with \isa{a} is still in the association list
   42.80 +but no longer accessible via \isa{assoc}. Clearly, there is room here for
   42.81 +optimizations!
   42.82 +
   42.83 +Before we start on any proofs about \isa{update} we tell the simplifier to
   42.84 +expand all \isa{let}s and to split all \isa{case}-constructs over
   42.85 +options:
   42.86 +*}
   42.87 +
   42.88 +theorems [simp] = Let_def;
   42.89 +theorems [split] = option.split;
   42.90 +
   42.91 +text{*\noindent
   42.92 +The reason becomes clear when looking (probably after a failed proof
   42.93 +attempt) at the body of \isa{update}: it contains both
   42.94 +\isa{let} and a case distinction over type \isa{option}.
   42.95 +
   42.96 +Our main goal is to prove the correct interaction of \isa{update} and
   42.97 +\isa{lookup}:
   42.98 +*}
   42.99 +
  42.100 +theorem "\\<forall>t v bs. lookup (update t as v) bs =
  42.101 +                    (if as=bs then Some v else lookup t bs)";
  42.102 +
  42.103 +txt{*\noindent
  42.104 +Our plan is to induct on \isa{as}; hence the remaining variables are
  42.105 +quantified. From the definitions it is clear that induction on either
  42.106 +\isa{as} or \isa{bs} is required. The choice of \isa{as} is merely
  42.107 +guided by the intuition that simplification of \isa{lookup} might be easier
  42.108 +if \isa{update} has already been simplified, which can only happen if
  42.109 +\isa{as} is instantiated.
  42.110 +The start of the proof is completely conventional:
  42.111 +*}
  42.112 +
  42.113 +apply(induct_tac "as", auto);
  42.114 +
  42.115 +txt{*\noindent
  42.116 +Unfortunately, this time we are left with three intimidating looking subgoals:
  42.117 +\begin{isabellepar}%
  42.118 +~1.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
  42.119 +~2.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs\isanewline
  42.120 +~3.~\dots~{\isasymLongrightarrow}~lookup~\dots~bs~=~lookup~t~bs%
  42.121 +\end{isabellepar}%
  42.122 +Clearly, if we want to make headway we have to instantiate \isa{bs} as
  42.123 +well now. It turns out that instead of induction, case distinction
  42.124 +suffices:
  42.125 +*}
  42.126 +
  42.127 +apply(case_tac[!] bs);
  42.128 +apply(auto).;
  42.129 +
  42.130 +text{*\noindent
  42.131 +Both \isaindex{case_tac} and \isaindex{induct_tac}
  42.132 +take an optional first argument that specifies the range of subgoals they are
  42.133 +applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual
  42.134 +subgoal number are also allowed.
  42.135 +
  42.136 +This proof may look surprisingly straightforward. However, note that this
  42.137 +comes at a cost: the proof script is unreadable because the
  42.138 +intermediate proof states are invisible, and we rely on the (possibly
  42.139 +brittle) magic of \isa{auto} (after the induction) to split the remaining
  42.140 +goals up in such a way that case distinction on \isa{bs} makes sense and
  42.141 +solves the proof. Part~\ref{Isar} shows you how to write readable and stable
  42.142 +proofs.
  42.143 +*}
  42.144 +
  42.145 +(*<*)
  42.146 +end
  42.147 +(*>*)
    43.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
    43.2 +++ b/doc-src/TutorialI/Trie/document/root.tex	Wed Apr 19 11:56:31 2000 +0200
    43.3 @@ -0,0 +1,4 @@
    43.4 +\documentclass{article}
    43.5 +\begin{document}
    43.6 +xxx
    43.7 +\end{document}