summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Wed, 19 Apr 2000 11:56:31 +0200 | |

changeset 8745 | 13b32661dde4 |

parent 8744 | 22fa8b16c3ae |

child 8746 | ccbb5e0dccdf |

I wonder which files i forgot.

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

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

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

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

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

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

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

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

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Misc/Itrev.thy Wed Apr 19 11:56:31 2000 +0200 @@ -0,0 +1,90 @@ +(*<*) +theory Itrev = Main:; +(*>*) + +text{* +We define a tail-recursive version of list-reversal, +i.e.\ one that can be compiled into a loop: +*} + +consts itrev :: "'a list \\<Rightarrow> 'a list \\<Rightarrow> 'a list"; +primrec +"itrev [] ys = ys" +"itrev (x#xs) ys = itrev xs (x#ys)"; + +text{*\noindent +The behaviour of \isa{itrev} is simple: it reverses its first argument by +stacking its elements onto the second argument, and returning that second +argument when the first one becomes empty. +We need to show that \isa{itrev} does indeed reverse its first argument +provided the second one is empty: +*} + +lemma "itrev xs [] = rev xs"; + +txt{*\noindent +There is no choice as to the induction variable, and we immediately simplify: +*} + +apply(induct_tac xs, auto); + +txt{*\noindent +Unfortunately, this is not a complete success: +\begin{isabellepar}% +~1.~\dots~itrev~list~[]~=~rev~list~{\isasymLongrightarrow}~itrev~list~[a]~=~rev~list~@~[a]% +\end{isabellepar}% +Just as predicted above, the overall goal, and hence the induction +hypothesis, is too weak to solve the induction step because of the fixed +\isa{[]}. The corresponding heuristic: +\begin{quote} +{\em 3. Generalize goals for induction by replacing constants by variables.} +\end{quote} + +Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is +just not true---the correct generalization is +*} +(*<*)oops;(*>*) +lemma "itrev xs ys = rev xs @ ys"; + +txt{*\noindent +If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to +\isa{rev xs}, just as required. + +In this particular instance it was easy to guess the right generalization, +but in more complex situations a good deal of creativity is needed. This is +the main source of complications in inductive proofs. + +Although we now have two variables, only \isa{xs} is suitable for +induction, and we repeat our above proof attempt. Unfortunately, we are still +not there: +\begin{isabellepar}% +~1.~{\isasymAnd}a~list.\isanewline +~~~~~~~itrev~list~ys~=~rev~list~@~ys~{\isasymLongrightarrow}\isanewline +~~~~~~~itrev~list~(a~\#~ys)~=~rev~list~@~a~\#~ys% +\end{isabellepar}% +The induction hypothesis is still too weak, but this time it takes no +intuition to generalize: the problem is that \isa{ys} is fixed throughout +the subgoal, but the induction hypothesis needs to be applied with +\isa{a \# ys} instead of \isa{ys}. Hence we prove the theorem +for all \isa{ys} instead of a fixed one: +*} +(*<*)oops;(*>*) +lemma "\\<forall>ys. itrev xs ys = rev xs @ ys"; + +txt{*\noindent +This time induction on \isa{xs} followed by simplification succeeds. This +leads to another heuristic for generalization: +\begin{quote} +{\em 4. Generalize goals for induction by universally quantifying all free +variables {\em(except the induction variable itself!)}.} +\end{quote} +This prevents trivial failures like the above and does not change the +provability of the goal. Because it is not always required, and may even +complicate matters in some cases, this heuristic is often not +applied blindly. +*} + +(*<*) +oops; +end +(*>*)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/TutorialI/Recdef/termination.thy Wed Apr 19 11:56:31 2000 +0200 @@ -0,0 +1,102 @@ +(*<*) +theory termination = Main:; +(*>*) + +text{* +When a function is defined via \isacommand{recdef}, Isabelle tries to prove +its termination with the help of the user-supplied measure. All of the above +examples are simple enough that Isabelle can prove automatically that the +measure of the argument goes down in each recursive call. In that case +$f$.\isa{simps} contains the defining equations (or variants derived from +them) as theorems. For example, look (via \isacommand{thm}) at +\isa{sep.simps} and \isa{sep1.simps} to see that they define the same +function. What is more, those equations are automatically declared as +simplification rules. + +In general, Isabelle may not be able to prove all termination condition +(there is one for each recursive call) automatically. For example, +termination of the following artificial function +*} + +consts f :: "nat*nat \\<Rightarrow> nat"; +recdef f "measure(\\<lambda>(x,y). x-y)" + "f(x,y) = (if x \\<le> y then x else f(x,y+1))"; + +text{*\noindent +is not proved automatically (although maybe it should be). Isabelle prints a +kind of error message showing you what it was unable to prove. You will then +have to prove it as a separate lemma before you attempt the definition +of your function once more. In our case the required lemma is the obvious one: +*} + +lemma termi_lem[simp]: "\\<not> x \\<le> y \\<Longrightarrow> x - Suc y < x - y"; + +txt{*\noindent +It was not proved automatically because of the special nature of \isa{-} +on \isa{nat}. This requires more arithmetic than is tried by default: +*} + +apply(arith).; + +text{*\noindent +Because \isacommand{recdef}'s the termination prover involves simplification, +we have declared our lemma a simplification rule. Therefore our second +attempt to define our function will automatically take it into account: +*} + +consts g :: "nat*nat \\<Rightarrow> nat"; +recdef g "measure(\\<lambda>(x,y). x-y)" + "g(x,y) = (if x \\<le> y then x else g(x,y+1))"; + +text{*\noindent +This time everything works fine. Now \isa{g.simps} contains precisely the +stated recursion equation for \isa{g} and they are simplification +rules. Thus we can automatically prove +*} + +theorem wow: "g(1,0) = g(1,1)"; +apply(simp).; + +text{*\noindent +More exciting theorems require induction, which is discussed below. + +Because lemma \isa{termi_lem} above was only turned into a +simplification rule for the sake of the termination proof, we may want to +disable it again: +*} + +lemmas [simp del] = termi_lem; + +text{* +The attentive reader may wonder why we chose to call our function \isa{g} +rather than \isa{f} the second time around. The reason is that, despite +the failed termination proof, the definition of \isa{f} did not +fail (and thus we could not define it a second time). However, all theorems +about \isa{f}, for example \isa{f.simps}, carry as a precondition the +unproved termination condition. Moreover, the theorems \isa{f.simps} are +not simplification rules. However, this mechanism allows a delayed proof of +termination: instead of proving \isa{termi_lem} up front, we could prove +it later on and then use it to remove the preconditions from the theorems +about \isa{f}. In most cases this is more cumbersome than proving things +up front +%FIXME, with one exception: nested recursion. + +Although all the above examples employ measure functions, \isacommand{recdef} +allows arbitrary wellfounded relations. For example, termination of +Ackermann's function requires the lexicographic product \isa{<*lex*>}: +*} + +consts ack :: "nat*nat \\<Rightarrow> nat"; +recdef ack "measure(%m. m) <*lex*> measure(%n. n)" + "ack(0,n) = Suc n" + "ack(Suc m,0) = ack(m, 1)" + "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))"; + +text{*\noindent +For details see the manual~\cite{isabelle-HOL} and the examples in the +library. +*} + +(*<*) +end +(*>*)

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

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

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

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

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

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

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