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}