# HG changeset patch # User nipkow # Date 965568413 -7200 # Node ID d17c0b34d5c86c85dd9b5440d52d3627684e48a6 # Parent 02c51ca9c5310cd6a612ffe6d82516f96d569854 *** empty log message *** diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Sun Aug 06 15:26:53 2000 +0200 @@ -10,10 +10,10 @@ a fixed set of binary operations: instead the expression contains the appropriate function itself.% \end{isamarkuptext}% -\isacommand{types}~'v~binop~=~{"}'v~{\isasymRightarrow}~'v~{\isasymRightarrow}~'v{"}\isanewline -\isacommand{datatype}~('a,'v)expr~=~Cex~'v\isanewline -~~~~~~~~~~~~~~~~~~~~~|~Vex~'a\isanewline -~~~~~~~~~~~~~~~~~~~~~|~Bex~{"}'v~binop{"}~~{"}('a,'v)expr{"}~~{"}('a,'v)expr{"}% +\isacommand{types}\ 'v\ binop\ =\ {"}'v\ {\isasymRightarrow}\ 'v\ {\isasymRightarrow}\ 'v{"}\isanewline +\isacommand{datatype}\ ('a,'v)expr\ =\ Cex\ 'v\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Vex\ 'a\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Bex\ {"}'v\ binop{"}\ \ {"}('a,'v)expr{"}\ \ {"}('a,'v)expr{"}% \begin{isamarkuptext}% \noindent The three constructors represent constants, variables and the application of @@ -22,20 +22,20 @@ The value of an expression w.r.t.\ an environment that maps variables to values is easily defined:% \end{isamarkuptext}% -\isacommand{consts}~value~::~{"}('a,'v)expr~{\isasymRightarrow}~('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~'v{"}\isanewline +\isacommand{consts}\ value\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ 'v)\ {\isasymRightarrow}\ 'v{"}\isanewline \isacommand{primrec}\isanewline -{"}value~(Cex~v)~env~=~v{"}\isanewline -{"}value~(Vex~a)~env~=~env~a{"}\isanewline -{"}value~(Bex~f~e1~e2)~env~=~f~(value~e1~env)~(value~e2~env){"}% +{"}value\ (Cex\ v)\ env\ =\ v{"}\isanewline +{"}value\ (Vex\ a)\ env\ =\ env\ a{"}\isanewline +{"}value\ (Bex\ f\ e1\ e2)\ env\ =\ f\ (value\ e1\ env)\ (value\ e2\ env){"}% \begin{isamarkuptext}% The stack machine has three instructions: load a constant value onto the stack, load the contents of a certain address onto the stack, and apply a binary operation to the two topmost elements of the stack, replacing them by the result. As for \isa{expr}, addresses and values are type parameters:% \end{isamarkuptext}% -\isacommand{datatype}~('a,'v)~instr~=~Const~'v\isanewline -~~~~~~~~~~~~~~~~~~~~~~~|~Load~'a\isanewline -~~~~~~~~~~~~~~~~~~~~~~~|~Apply~{"}'v~binop{"}% +\isacommand{datatype}\ ('a,'v)\ instr\ =\ Const\ 'v\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Load\ 'a\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Apply\ {"}'v\ binop{"}% \begin{isamarkuptext}% The execution of the stack machine is modelled by a function \isa{exec} that takes a list of instructions, a store (modelled as a @@ -44,13 +44,13 @@ and returns the stack at the end of the execution---the store remains unchanged:% \end{isamarkuptext}% -\isacommand{consts}~exec~::~{"}('a,'v)instr~list~{\isasymRightarrow}~('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~'v~list{"}\isanewline +\isacommand{consts}\ exec\ ::\ {"}('a,'v)instr\ list\ {\isasymRightarrow}\ ('a{\isasymRightarrow}'v)\ {\isasymRightarrow}\ 'v\ list\ {\isasymRightarrow}\ 'v\ list{"}\isanewline \isacommand{primrec}\isanewline -{"}exec~[]~s~vs~=~vs{"}\isanewline -{"}exec~(i\#is)~s~vs~=~(case~i~of\isanewline -~~~~Const~v~~{\isasymRightarrow}~exec~is~s~(v\#vs)\isanewline -~~|~Load~a~~~{\isasymRightarrow}~exec~is~s~((s~a)\#vs)\isanewline -~~|~Apply~f~~{\isasymRightarrow}~exec~is~s~((f~(hd~vs)~(hd(tl~vs)))\#(tl(tl~vs)))){"}% +{"}exec\ []\ s\ vs\ =\ vs{"}\isanewline +{"}exec\ (i\#is)\ s\ vs\ =\ (case\ i\ of\isanewline +\ \ \ \ Const\ v\ \ {\isasymRightarrow}\ exec\ is\ s\ (v\#vs)\isanewline +\ \ |\ Load\ a\ \ \ {\isasymRightarrow}\ exec\ is\ s\ ((s\ a)\#vs)\isanewline +\ \ |\ Apply\ f\ \ {\isasymRightarrow}\ exec\ is\ s\ ((f\ (hd\ vs)\ (hd(tl\ vs)))\#(tl(tl\ vs)))){"}% \begin{isamarkuptext}% \noindent Recall that \isa{hd} and \isa{tl} @@ -64,29 +64,29 @@ The compiler is a function from expressions to a list of instructions. Its definition is pretty much obvious:% \end{isamarkuptext}% -\isacommand{consts}~comp~::~{"}('a,'v)expr~{\isasymRightarrow}~('a,'v)instr~list{"}\isanewline +\isacommand{consts}\ comp\ ::\ {"}('a,'v)expr\ {\isasymRightarrow}\ ('a,'v)instr\ list{"}\isanewline \isacommand{primrec}\isanewline -{"}comp~(Cex~v)~~~~~~~=~[Const~v]{"}\isanewline -{"}comp~(Vex~a)~~~~~~~=~[Load~a]{"}\isanewline -{"}comp~(Bex~f~e1~e2)~=~(comp~e2)~@~(comp~e1)~@~[Apply~f]{"}% +{"}comp\ (Cex\ v)\ \ \ \ \ \ \ =\ [Const\ v]{"}\isanewline +{"}comp\ (Vex\ a)\ \ \ \ \ \ \ =\ [Load\ a]{"}\isanewline +{"}comp\ (Bex\ f\ e1\ e2)\ =\ (comp\ e2)\ @\ (comp\ e1)\ @\ [Apply\ f]{"}% \begin{isamarkuptext}% Now we have to prove the correctness of the compiler, i.e.\ that the execution of a compiled expression results in the value of the expression:% \end{isamarkuptext}% -\isacommand{theorem}~{"}exec~(comp~e)~s~[]~=~[value~e~s]{"}% +\isacommand{theorem}\ {"}exec\ (comp\ e)\ s\ []\ =\ [value\ e\ s]{"}% \begin{isamarkuptext}% \noindent This theorem needs to be generalized to% \end{isamarkuptext}% -\isacommand{theorem}~{"}{\isasymforall}vs.~exec~(comp~e)~s~vs~=~(value~e~s)~\#~vs{"}% +\isacommand{theorem}\ {"}{\isasymforall}vs.\ exec\ (comp\ e)\ s\ vs\ =\ (value\ e\ s)\ \#\ vs{"}% \begin{isamarkuptxt}% \noindent which is proved by induction on \isa{e} followed by simplification, once we have the following lemma about executing the concatenation of two instruction sequences:% \end{isamarkuptxt}% -\isacommand{lemma}~exec\_app[simp]:\isanewline -~~{"}{\isasymforall}vs.~exec~(xs@ys)~s~vs~=~exec~ys~s~(exec~xs~s~vs){"}% +\isacommand{lemma}\ exec\_app[simp]:\isanewline +\ \ {"}{\isasymforall}vs.\ exec\ (xs@ys)\ s\ vs\ =\ exec\ ys\ s\ (exec\ xs\ s\ vs){"}% \begin{isamarkuptxt}% \noindent This requires induction on \isa{xs} and ordinary simplification for the @@ -94,14 +94,14 @@ that contains two \isa{case}-expressions over instructions. Thus we add automatic case splitting as well, which finishes the proof:% \end{isamarkuptxt}% -\isacommand{by}(induct\_tac~xs,~simp,~simp~split:~instr.split)% +\isacommand{by}(induct\_tac\ xs,\ simp,\ simp\ split:\ instr.split)% \begin{isamarkuptext}% \noindent Note that because \isaindex{auto} performs simplification, it can also be modified in the same way \isa{simp} can. Thus the proof can be rewritten as% \end{isamarkuptext}% -\isacommand{by}(induct\_tac~xs,~auto~split:~instr.split)% +\isacommand{by}(induct\_tac\ xs,\ auto\ split:\ instr.split)% \begin{isamarkuptext}% \noindent Although this is more compact, it is less clear for the reader of the proof. diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Datatype/ABexpr.thy --- a/doc-src/TutorialI/Datatype/ABexpr.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy Sun Aug 06 15:26:53 2000 +0200 @@ -113,7 +113,7 @@ \end{ttbox} \begin{exercise} - Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that + Define a function \isa{norma} of type @{typ"'a aexp => '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} diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Datatype/Fundata.thy --- a/doc-src/TutorialI/Datatype/Fundata.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Sun Aug 06 15:26:53 2000 +0200 @@ -9,11 +9,11 @@ \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 (\\i. Branch i (\\n. Tip))"; - -text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose +write down such a tree? Using functional notation! For example, the term +\begin{quote} +@{term[display]"Branch 0 (%i. Branch i (%n. Tip))"} +\end{quote} +of type @{typ"(nat,nat)bigtree"} is the tree whose root is labeled with 0 and whose $i$th subtree is labeled with $i$ and has merely \isa{Tip}s as further subtrees. @@ -28,8 +28,8 @@ 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 +seasoned functional programmer might have written @{term"map_bt f o F"} +instead of @{term"%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. diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Datatype/Nested.thy --- a/doc-src/TutorialI/Datatype/Nested.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Datatype/Nested.thy Sun Aug 06 15:26:53 2000 +0200 @@ -16,8 +16,8 @@ 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 +A mathematical term like $f(x,g(y))$ becomes @{term"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 @@ -64,7 +64,7 @@ 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 +leaves variables unchanged: @{term"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 @@ -86,9 +86,5 @@ expressions as its argument: \isa{Sum "'a aexp list"}. *} (*<*) - -lemma "subst s (App f ts) = App f (map (subst s) ts)"; -by(induct_tac ts, auto); - end (*>*) diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Datatype/document/ABexpr.tex --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Sun Aug 06 15:26:53 2000 +0200 @@ -13,14 +13,14 @@ \end{itemize} In Isabelle this becomes% \end{isamarkuptext}% -\isacommand{datatype}~'a~aexp~=~IF~~~{"}'a~bexp{"}~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline -~~~~~~~~~~~~~~~~~|~Sum~~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline -~~~~~~~~~~~~~~~~~|~Diff~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline -~~~~~~~~~~~~~~~~~|~Var~'a\isanewline -~~~~~~~~~~~~~~~~~|~Num~nat\isanewline -\isakeyword{and}~~~~~~'a~bexp~=~Less~{"}'a~aexp{"}~{"}'a~aexp{"}\isanewline -~~~~~~~~~~~~~~~~~|~And~~{"}'a~bexp{"}~{"}'a~bexp{"}\isanewline -~~~~~~~~~~~~~~~~~|~Neg~~{"}'a~bexp{"}% +\isacommand{datatype}\ 'a\ aexp\ =\ IF\ \ \ {"}'a\ bexp{"}\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Sum\ \ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Diff\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Var\ 'a\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Num\ nat\isanewline +\isakeyword{and}\ \ \ \ \ \ 'a\ bexp\ =\ Less\ {"}'a\ aexp{"}\ {"}'a\ aexp{"}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ \ {"}'a\ bexp{"}\ {"}'a\ bexp{"}\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Neg\ \ {"}'a\ bexp{"}% \begin{isamarkuptext}% \noindent Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, @@ -29,8 +29,8 @@ expressions can be arithmetic comparisons, conjunctions and negations. The semantics is fixed via two evaluation functions% \end{isamarkuptext}% -\isacommand{consts}~~evala~::~{"}'a~aexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~nat{"}\isanewline -~~~~~~~~evalb~::~{"}'a~bexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~bool{"}% +\isacommand{consts}\ \ evala\ ::\ {"}'a\ aexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ nat{"}\isanewline +\ \ \ \ \ \ \ \ evalb\ ::\ {"}'a\ bexp\ {\isasymRightarrow}\ ('a\ {\isasymRightarrow}\ nat)\ {\isasymRightarrow}\ bool{"}% \begin{isamarkuptext}% \noindent that take an expression and an environment (a mapping from variables \isa{'a} to values @@ -40,22 +40,22 @@ section:% \end{isamarkuptext}% \isacommand{primrec}\isanewline -~~{"}evala~(IF~b~a1~a2)~env~=\isanewline -~~~~~(if~evalb~b~env~then~evala~a1~env~else~evala~a2~env){"}\isanewline -~~{"}evala~(Sum~a1~a2)~env~=~evala~a1~env~+~evala~a2~env{"}\isanewline -~~{"}evala~(Diff~a1~a2)~env~=~evala~a1~env~-~evala~a2~env{"}\isanewline -~~{"}evala~(Var~v)~env~=~env~v{"}\isanewline -~~{"}evala~(Num~n)~env~=~n{"}\isanewline +\ \ {"}evala\ (IF\ b\ a1\ a2)\ env\ =\isanewline +\ \ \ \ \ (if\ evalb\ b\ env\ then\ evala\ a1\ env\ else\ evala\ a2\ env){"}\isanewline +\ \ {"}evala\ (Sum\ a1\ a2)\ env\ =\ evala\ a1\ env\ +\ evala\ a2\ env{"}\isanewline +\ \ {"}evala\ (Diff\ a1\ a2)\ env\ =\ evala\ a1\ env\ -\ evala\ a2\ env{"}\isanewline +\ \ {"}evala\ (Var\ v)\ env\ =\ env\ v{"}\isanewline +\ \ {"}evala\ (Num\ n)\ env\ =\ n{"}\isanewline \isanewline -~~{"}evalb~(Less~a1~a2)~env~=~(evala~a1~env~<~evala~a2~env){"}\isanewline -~~{"}evalb~(And~b1~b2)~env~=~(evalb~b1~env~{\isasymand}~evalb~b2~env){"}\isanewline -~~{"}evalb~(Neg~b)~env~=~({\isasymnot}~evalb~b~env){"}% +\ \ {"}evalb\ (Less\ a1\ a2)\ env\ =\ (evala\ a1\ env\ <\ evala\ a2\ env){"}\isanewline +\ \ {"}evalb\ (And\ b1\ b2)\ env\ =\ (evalb\ b1\ env\ {\isasymand}\ evalb\ b2\ env){"}\isanewline +\ \ {"}evalb\ (Neg\ b)\ env\ =\ ({\isasymnot}\ evalb\ b\ env){"}% \begin{isamarkuptext}% \noindent In the same fashion we also define two functions that perform substitution:% \end{isamarkuptext}% -\isacommand{consts}~substa~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~'b~aexp{"}\isanewline -~~~~~~~substb~::~{"}('a~{\isasymRightarrow}~'b~aexp)~{\isasymRightarrow}~'a~bexp~{\isasymRightarrow}~'b~bexp{"}% +\isacommand{consts}\ substa\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ aexp\ {\isasymRightarrow}\ 'b\ aexp{"}\isanewline +\ \ \ \ \ \ \ substb\ ::\ {"}('a\ {\isasymRightarrow}\ 'b\ aexp)\ {\isasymRightarrow}\ 'a\ bexp\ {\isasymRightarrow}\ 'b\ bexp{"}% \begin{isamarkuptext}% \noindent The first argument is a function mapping variables to expressions, the @@ -64,16 +64,16 @@ to \isa{'b}. Note that there are only arithmetic and no boolean variables.% \end{isamarkuptext}% \isacommand{primrec}\isanewline -~~{"}substa~s~(IF~b~a1~a2)~=\isanewline -~~~~~IF~(substb~s~b)~(substa~s~a1)~(substa~s~a2){"}\isanewline -~~{"}substa~s~(Sum~a1~a2)~=~Sum~(substa~s~a1)~(substa~s~a2){"}\isanewline -~~{"}substa~s~(Diff~a1~a2)~=~Diff~(substa~s~a1)~(substa~s~a2){"}\isanewline -~~{"}substa~s~(Var~v)~=~s~v{"}\isanewline -~~{"}substa~s~(Num~n)~=~Num~n{"}\isanewline +\ \ {"}substa\ s\ (IF\ b\ a1\ a2)\ =\isanewline +\ \ \ \ \ IF\ (substb\ s\ b)\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline +\ \ {"}substa\ s\ (Sum\ a1\ a2)\ =\ Sum\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline +\ \ {"}substa\ s\ (Diff\ a1\ a2)\ =\ Diff\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline +\ \ {"}substa\ s\ (Var\ v)\ =\ s\ v{"}\isanewline +\ \ {"}substa\ s\ (Num\ n)\ =\ Num\ n{"}\isanewline \isanewline -~~{"}substb~s~(Less~a1~a2)~=~Less~(substa~s~a1)~(substa~s~a2){"}\isanewline -~~{"}substb~s~(And~b1~b2)~=~And~(substb~s~b1)~(substb~s~b2){"}\isanewline -~~{"}substb~s~(Neg~b)~=~Neg~(substb~s~b){"}% +\ \ {"}substb\ s\ (Less\ a1\ a2)\ =\ Less\ (substa\ s\ a1)\ (substa\ s\ a2){"}\isanewline +\ \ {"}substb\ s\ (And\ b1\ b2)\ =\ And\ (substb\ s\ b1)\ (substb\ s\ b2){"}\isanewline +\ \ {"}substb\ s\ (Neg\ b)\ =\ Neg\ (substb\ s\ b){"}% \begin{isamarkuptext}% Now we can prove a fundamental theorem about the interaction between evaluation and substitution: applying a substitution $s$ to an expression $a$ @@ -84,14 +84,14 @@ theorem in the induction step. Therefore you need to state and prove both theorems simultaneously:% \end{isamarkuptext}% -\isacommand{lemma}~{"}evala~(substa~s~a)~env~=~evala~a~({\isasymlambda}x.~evala~(s~x)~env)~{\isasymand}\isanewline -~~~~~~~~evalb~(substb~s~b)~env~=~evalb~b~({\isasymlambda}x.~evala~(s~x)~env){"}\isanewline -\isacommand{apply}(induct\_tac~a~\isakeyword{and}~b)% +\isacommand{lemma}\ {"}evala\ (substa\ s\ a)\ env\ =\ evala\ a\ ({\isasymlambda}x.\ evala\ (s\ x)\ env)\ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ evalb\ (substb\ s\ b)\ env\ =\ evalb\ b\ ({\isasymlambda}x.\ evala\ (s\ x)\ env){"}\isanewline +\isacommand{apply}(induct\_tac\ a\ \isakeyword{and}\ b)% \begin{isamarkuptxt}% \noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:% \end{isamarkuptxt}% -\isacommand{by}~auto% +\isacommand{by}\ auto% \begin{isamarkuptext}% In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, an inductive proof expects a goal of the form @@ -102,7 +102,7 @@ \end{ttbox} \begin{exercise} - Define a function \isa{norma} of type \isa{'a aexp \isasymFun\ 'a aexp} that + Define a function \isa{norma} of type \isa{'a\ aexp\ {\isasymRightarrow}\ '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} diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{datatype}~('a,'i)bigtree~=~Tip~|~Branch~'a~{"}'i~{\isasymRightarrow}~('a,'i)bigtree{"}% +\isacommand{datatype}\ ('a,'i)bigtree\ =\ Tip\ |\ Branch\ 'a\ {"}'i\ {\isasymRightarrow}\ ('a,'i)bigtree{"}% \begin{isamarkuptext}% \noindent Parameter \isa{'a} is the type of values stored in the \isa{Branch}es of the tree, whereas \isa{'i} is the index @@ -7,33 +7,37 @@ \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% -\end{isamarkuptext}% -\isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}% -\begin{isamarkuptext}% -\noindent of type \isa{(nat,nat)bigtree} is the tree whose +write down such a tree? Using functional notation! For example, the term +\begin{quote} + +\begin{isabelle}% +Branch\ 0\ ({\isasymlambda}i.\ Branch\ i\ ({\isasymlambda}n.\ Tip)) +\end{isabelle}% + +\end{quote} +of type \isa{(nat,\ nat)\ bigtree} is the tree whose root is labeled with 0 and whose $i$th subtree is labeled with $i$ and has merely \isa{Tip}s as further subtrees. Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:% \end{isamarkuptext}% -\isacommand{consts}~map\_bt~::~{"}('a~{\isasymRightarrow}~'b)~{\isasymRightarrow}~('a,'i)bigtree~{\isasymRightarrow}~('b,'i)bigtree{"}\isanewline +\isacommand{consts}\ map\_bt\ ::\ {"}('a\ {\isasymRightarrow}\ 'b)\ {\isasymRightarrow}\ ('a,'i)bigtree\ {\isasymRightarrow}\ ('b,'i)bigtree{"}\isanewline \isacommand{primrec}\isanewline -{"}map\_bt~f~Tip~~~~~~~~~~=~Tip{"}\isanewline -{"}map\_bt~f~(Branch~a~F)~=~Branch~(f~a)~({\isasymlambda}i.~map\_bt~f~(F~i)){"}% +{"}map\_bt\ f\ Tip\ \ \ \ \ \ \ \ \ \ =\ Tip{"}\isanewline +{"}map\_bt\ f\ (Branch\ a\ F)\ =\ Branch\ (f\ a)\ ({\isasymlambda}i.\ map\_bt\ f\ (F\ i)){"}% \begin{isamarkuptext}% \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 +seasoned functional programmer might have written \isa{map\_bt\ f\ {\isasymcirc}\ 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% \end{isamarkuptext}% -\isacommand{lemma}~{"}map\_bt~(g~o~f)~T~=~map\_bt~g~(map\_bt~f~T){"}\isanewline -\isacommand{apply}(induct\_tac~{"}T{"},~auto)\isacommand{.}% +\isacommand{lemma}\ {"}map\_bt\ (g\ o\ f)\ T\ =\ map\_bt\ g\ (map\_bt\ f\ T){"}\isanewline +\isacommand{apply}(induct\_tac\ {"}T{"},\ auto)\isacommand{.}% \begin{isamarkuptext}% \noindent but it is worth taking a look at the proof state after the induction step diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Sun Aug 06 15:26:53 2000 +0200 @@ -6,15 +6,14 @@ 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:% \end{isamarkuptext}% -\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term~list{"}% +\isacommand{datatype}\ ('a,'b){"}term{"}\ =\ Var\ 'a\ |\ App\ 'b\ {"}('a,'b)term\ list{"}% \begin{isamarkuptext}% \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 +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 @@ -37,15 +36,15 @@ lists, we need to define two substitution functions simultaneously:% \end{isamarkuptext}% \isacommand{consts}\isanewline -subst~::~{"}('a{\isasymRightarrow}('a,'b)term)~{\isasymRightarrow}~('a,'b)term~~~~~~{\isasymRightarrow}~('a,'b)term{"}\isanewline -substs::~{"}('a{\isasymRightarrow}('a,'b)term)~{\isasymRightarrow}~('a,'b)term~list~{\isasymRightarrow}~('a,'b)term~list{"}\isanewline +subst\ ::\ {"}('a{\isasymRightarrow}('a,'b)term)\ {\isasymRightarrow}\ ('a,'b)term\ \ \ \ \ \ {\isasymRightarrow}\ ('a,'b)term{"}\isanewline +substs::\ {"}('a{\isasymRightarrow}('a,'b)term)\ {\isasymRightarrow}\ ('a,'b)term\ list\ {\isasymRightarrow}\ ('a,'b)term\ list{"}\isanewline \isanewline \isacommand{primrec}\isanewline -~~{"}subst~s~(Var~x)~=~s~x{"}\isanewline -~~{"}subst~s~(App~f~ts)~=~App~f~(substs~s~ts){"}\isanewline +\ \ {"}subst\ s\ (Var\ x)\ =\ s\ x{"}\isanewline +\ \ {"}subst\ s\ (App\ f\ ts)\ =\ App\ f\ (substs\ s\ ts){"}\isanewline \isanewline -~~{"}substs~s~[]~=~[]{"}\isanewline -~~{"}substs~s~(t~\#~ts)~=~subst~s~t~\#~substs~s~ts{"}% +\ \ {"}substs\ s\ []\ =\ []{"}\isanewline +\ \ {"}substs\ s\ (t\ \#\ ts)\ =\ subst\ s\ t\ \#\ substs\ s\ ts{"}% \begin{isamarkuptext}% \noindent Similarly, when proving a statement about terms inductively, we need @@ -53,13 +52,13 @@ the fact that the identity substitution does not change a term needs to be strengthened and proved as follows:% \end{isamarkuptext}% -\isacommand{lemma}~{"}subst~~Var~t~~=~(t~::('a,'b)term)~~{\isasymand}\isanewline -~~~~~~~~substs~Var~ts~=~(ts::('a,'b)term~list){"}\isanewline -\isacommand{by}(induct\_tac~t~\isakeyword{and}~ts,~auto)% +\isacommand{lemma}\ {"}subst\ \ Var\ t\ \ =\ (t\ ::('a,'b)term)\ \ {\isasymand}\isanewline +\ \ \ \ \ \ \ \ substs\ Var\ ts\ =\ (ts::('a,'b)term\ list){"}\isanewline +\isacommand{by}(induct\_tac\ t\ \isakeyword{and}\ ts,\ auto)% \begin{isamarkuptext}% \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 +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 diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Datatype/document/unfoldnested.tex --- a/doc-src/TutorialI/Datatype/document/unfoldnested.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/unfoldnested.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,6 +1,6 @@ \begin{isabelle}% -\isacommand{datatype}~('a,'b){"}term{"}~=~Var~'a~|~App~'b~{"}('a,'b)term\_list{"}\isanewline -\isakeyword{and}~('a,'b)term\_list~=~Nil~|~Cons~{"}('a,'b)term{"}~{"}('a,'b)term\_list{"}\end{isabelle}% +\isacommand{datatype}\ ('a,'b){"}term{"}\ =\ Var\ 'a\ |\ App\ 'b\ {"}('a,'b)term\_list{"}\isanewline +\isakeyword{and}\ ('a,'b)term\_list\ =\ Nil\ |\ Cons\ {"}('a,'b)term{"}\ {"}('a,'b)term\_list{"}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Ifexpr/Ifexpr.thy --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Sun Aug 06 15:26:53 2000 +0200 @@ -14,17 +14,17 @@ | 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}). +The two constants are represented by @{term"Const True"} and +@{term"Const False"}. Variables are represented by terms of the form +@{term"Var n"}, where @{term"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))}. +@{term"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 + environment} of type @{typ"nat => bool"}, which maps variables to their values: *} @@ -93,8 +93,8 @@ 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 +repeatedly replacing a subterm of the form @{term"IF (IF b x y) z u"} by +@{term"IF b (IF x z u) (IF y z u)"}, which has the same value. The following primitive recursive functions perform this task: *} diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Sun Aug 06 15:26:53 2000 +0200 @@ -7,29 +7,29 @@ constants by negation and conjunction. The following datatype serves exactly that purpose:% \end{isamarkuptext}% -\isacommand{datatype}~boolex~=~Const~bool~|~Var~nat~|~Neg~boolex\isanewline -~~~~~~~~~~~~~~~~|~And~boolex~boolex% +\isacommand{datatype}\ boolex\ =\ Const\ bool\ |\ Var\ nat\ |\ Neg\ boolex\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ And\ boolex\ boolex% \begin{isamarkuptext}% \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}). +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 \isa{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))}. +\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 + environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their values:% \end{isamarkuptext}% -\isacommand{consts}~value~::~{"}boolex~{\isasymRightarrow}~(nat~{\isasymRightarrow}~bool)~{\isasymRightarrow}~bool{"}\isanewline +\isacommand{consts}\ value\ ::\ {"}boolex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline \isacommand{primrec}\isanewline -{"}value~(Const~b)~env~=~b{"}\isanewline -{"}value~(Var~x)~~~env~=~env~x{"}\isanewline -{"}value~(Neg~b)~~~env~=~({\isasymnot}~value~b~env){"}\isanewline -{"}value~(And~b~c)~env~=~(value~b~env~{\isasymand}~value~c~env){"}% +{"}value\ (Const\ b)\ env\ =\ b{"}\isanewline +{"}value\ (Var\ x)\ \ \ env\ =\ env\ x{"}\isanewline +{"}value\ (Neg\ b)\ \ \ env\ =\ ({\isasymnot}\ value\ b\ env){"}\isanewline +{"}value\ (And\ b\ c)\ env\ =\ (value\ b\ env\ {\isasymand}\ value\ c\ env){"}% \begin{isamarkuptext}% \noindent \subsubsection{If-expressions} @@ -39,17 +39,17 @@ from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals (\isa{IF}):% \end{isamarkuptext}% -\isacommand{datatype}~ifex~=~CIF~bool~|~VIF~nat~|~IF~ifex~ifex~ifex% +\isacommand{datatype}\ ifex\ =\ CIF\ bool\ |\ VIF\ nat\ |\ IF\ ifex\ ifex\ ifex% \begin{isamarkuptext}% \noindent The evaluation if If-expressions proceeds as for \isa{boolex}:% \end{isamarkuptext}% -\isacommand{consts}~valif~::~{"}ifex~{\isasymRightarrow}~(nat~{\isasymRightarrow}~bool)~{\isasymRightarrow}~bool{"}\isanewline +\isacommand{consts}\ valif\ ::\ {"}ifex\ {\isasymRightarrow}\ (nat\ {\isasymRightarrow}\ bool)\ {\isasymRightarrow}\ bool{"}\isanewline \isacommand{primrec}\isanewline -{"}valif~(CIF~b)~~~~env~=~b{"}\isanewline -{"}valif~(VIF~x)~~~~env~=~env~x{"}\isanewline -{"}valif~(IF~b~t~e)~env~=~(if~valif~b~env~then~valif~t~env\isanewline -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~else~valif~e~env){"}% +{"}valif\ (CIF\ b)\ \ \ \ env\ =\ b{"}\isanewline +{"}valif\ (VIF\ x)\ \ \ \ env\ =\ env\ x{"}\isanewline +{"}valif\ (IF\ b\ t\ e)\ env\ =\ (if\ valif\ b\ env\ then\ valif\ t\ env\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env){"}% \begin{isamarkuptext}% \subsubsection{Transformation into and of If-expressions} @@ -57,23 +57,23 @@ formulae, whereas \isa{ifex} is designed for efficiency. It is easy to translate from \isa{boolex} into \isa{ifex}:% \end{isamarkuptext}% -\isacommand{consts}~bool2if~::~{"}boolex~{\isasymRightarrow}~ifex{"}\isanewline +\isacommand{consts}\ bool2if\ ::\ {"}boolex\ {\isasymRightarrow}\ ifex{"}\isanewline \isacommand{primrec}\isanewline -{"}bool2if~(Const~b)~=~CIF~b{"}\isanewline -{"}bool2if~(Var~x)~~~=~VIF~x{"}\isanewline -{"}bool2if~(Neg~b)~~~=~IF~(bool2if~b)~(CIF~False)~(CIF~True){"}\isanewline -{"}bool2if~(And~b~c)~=~IF~(bool2if~b)~(bool2if~c)~(CIF~False){"}% +{"}bool2if\ (Const\ b)\ =\ CIF\ b{"}\isanewline +{"}bool2if\ (Var\ x)\ \ \ =\ VIF\ x{"}\isanewline +{"}bool2if\ (Neg\ b)\ \ \ =\ IF\ (bool2if\ b)\ (CIF\ False)\ (CIF\ True){"}\isanewline +{"}bool2if\ (And\ b\ c)\ =\ IF\ (bool2if\ b)\ (bool2if\ c)\ (CIF\ False){"}% \begin{isamarkuptext}% \noindent At last, we have something we can verify: that \isa{bool2if} preserves the value of its argument:% \end{isamarkuptext}% -\isacommand{lemma}~{"}valif~(bool2if~b)~env~=~value~b~env{"}% +\isacommand{lemma}\ {"}valif\ (bool2if\ b)\ env\ =\ value\ b\ env{"}% \begin{isamarkuptxt}% \noindent The proof is canonical:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac~b)\isanewline +\isacommand{apply}(induct\_tac\ b)\isanewline \isacommand{by}(auto)% \begin{isamarkuptext}% \noindent @@ -83,35 +83,35 @@ 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 +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:% \end{isamarkuptext}% -\isacommand{consts}~normif~::~{"}ifex~{\isasymRightarrow}~ifex~{\isasymRightarrow}~ifex~{\isasymRightarrow}~ifex{"}\isanewline +\isacommand{consts}\ normif\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{"}\isanewline \isacommand{primrec}\isanewline -{"}normif~(CIF~b)~~~~t~e~=~IF~(CIF~b)~t~e{"}\isanewline -{"}normif~(VIF~x)~~~~t~e~=~IF~(VIF~x)~t~e{"}\isanewline -{"}normif~(IF~b~t~e)~u~f~=~normif~b~(normif~t~u~f)~(normif~e~u~f){"}\isanewline +{"}normif\ (CIF\ b)\ \ \ \ t\ e\ =\ IF\ (CIF\ b)\ t\ e{"}\isanewline +{"}normif\ (VIF\ x)\ \ \ \ t\ e\ =\ IF\ (VIF\ x)\ t\ e{"}\isanewline +{"}normif\ (IF\ b\ t\ e)\ u\ f\ =\ normif\ b\ (normif\ t\ u\ f)\ (normif\ e\ u\ f){"}\isanewline \isanewline -\isacommand{consts}~norm~::~{"}ifex~{\isasymRightarrow}~ifex{"}\isanewline +\isacommand{consts}\ norm\ ::\ {"}ifex\ {\isasymRightarrow}\ ifex{"}\isanewline \isacommand{primrec}\isanewline -{"}norm~(CIF~b)~~~~=~CIF~b{"}\isanewline -{"}norm~(VIF~x)~~~~=~VIF~x{"}\isanewline -{"}norm~(IF~b~t~e)~=~normif~b~(norm~t)~(norm~e){"}% +{"}norm\ (CIF\ b)\ \ \ \ =\ CIF\ b{"}\isanewline +{"}norm\ (VIF\ x)\ \ \ \ =\ VIF\ x{"}\isanewline +{"}norm\ (IF\ b\ t\ e)\ =\ normif\ b\ (norm\ t)\ (norm\ e){"}% \begin{isamarkuptext}% \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:% \end{isamarkuptext}% -\isacommand{theorem}~{"}valif~(norm~b)~env~=~valif~b~env{"}% +\isacommand{theorem}\ {"}valif\ (norm\ b)\ env\ =\ valif\ b\ env{"}% \begin{isamarkuptext}% \noindent The proof is canonical, provided we first show the following simplification lemma (which also helps to understand what \isa{normif} does):% \end{isamarkuptext}% -\isacommand{lemma}~[simp]:\isanewline -~~{"}{\isasymforall}t~e.~valif~(normif~b~t~e)~env~=~valif~(IF~b~t~e)~env{"}% +\isacommand{lemma}\ [simp]:\isanewline +\ \ {"}{\isasymforall}t\ e.\ valif\ (normif\ b\ t\ e)\ env\ =\ valif\ (IF\ b\ t\ e)\ env{"}% \begin{isamarkuptext}% \noindent Note that the lemma does not have a name, but is implicitly used in the proof @@ -120,18 +120,18 @@ 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% \end{isamarkuptext}% -\isacommand{consts}~normal~::~{"}ifex~{\isasymRightarrow}~bool{"}\isanewline +\isacommand{consts}\ normal\ ::\ {"}ifex\ {\isasymRightarrow}\ bool{"}\isanewline \isacommand{primrec}\isanewline -{"}normal(CIF~b)~=~True{"}\isanewline -{"}normal(VIF~x)~=~True{"}\isanewline -{"}normal(IF~b~t~e)~=~(normal~t~{\isasymand}~normal~e~{\isasymand}\isanewline -~~~~~(case~b~of~CIF~b~{\isasymRightarrow}~True~|~VIF~x~{\isasymRightarrow}~True~|~IF~x~y~z~{\isasymRightarrow}~False)){"}% +{"}normal(CIF\ b)\ =\ True{"}\isanewline +{"}normal(VIF\ x)\ =\ True{"}\isanewline +{"}normal(IF\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline +\ \ \ \ \ (case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ |\ VIF\ x\ {\isasymRightarrow}\ True\ |\ IF\ x\ y\ z\ {\isasymRightarrow}\ False)){"}% \begin{isamarkuptext}% \noindent and prove \isa{normal(norm b)}. Of course, this requires a lemma about normality of \isa{normif}:% \end{isamarkuptext}% -\isacommand{lemma}[simp]:~{"}{\isasymforall}t~e.~normal(normif~b~t~e)~=~(normal~t~{\isasymand}~normal~e){"}\end{isabelle}% +\isacommand{lemma}[simp]:\ {"}{\isasymforall}t\ e.\ normal(normif\ b\ t\ e)\ =\ (normal\ t\ {\isasymand}\ normal\ e){"}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/Itrev.thy Sun Aug 06 15:26:53 2000 +0200 @@ -50,7 +50,7 @@ txt{*\noindent If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to -\isa{rev xs}, just as required. +@{term"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 @@ -67,7 +67,7 @@ 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 +@{term"a # ys"} instead of \isa{ys}. Hence we prove the theorem for all \isa{ys} instead of a fixed one: *}; (*<*)oops;(*>*) diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/asm_simp.thy --- a/doc-src/TutorialI/Misc/asm_simp.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/asm_simp.thy Sun Aug 06 15:26:53 2000 +0200 @@ -10,9 +10,9 @@ by 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}. +The second assumption simplifies to @{term"xs = []"}, which in turn +simplifies the first assumption to @{term"zs = ys"}, thus reducing the +conclusion to @{term"ys = ys"} and hence to \isa{True}. In some cases this may be too much of a good thing and may lead to nontermination: @@ -22,7 +22,7 @@ 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 +simplification rule @{term"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: diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/case_splits.thy --- a/doc-src/TutorialI/Misc/case_splits.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/case_splits.thy Sun Aug 06 15:26:53 2000 +0200 @@ -63,7 +63,7 @@ locally as above, or by giving it the \isa{split} attribute globally: *} -theorems [split] = list.split; +lemmas [split] = list.split; text{*\noindent The \isa{split} attribute can be removed with the \isa{del} modifier, @@ -79,7 +79,7 @@ text{*\noindent or globally: *} -theorems [split del] = list.split; +lemmas [split del] = list.split; (*<*) end diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/cond_rewr.thy --- a/doc-src/TutorialI/Misc/cond_rewr.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/cond_rewr.thy Sun Aug 06 15:26:53 2000 +0200 @@ -13,8 +13,7 @@ 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 +@{term"(rev xs = []) = (xs = [])"} is present as well, *} diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Sun Aug 06 15:26:53 2000 +0200 @@ -7,10 +7,10 @@ \isa{rev} reqires an extra argument where the result is accumulated gradually, using only \isa{\#}:% \end{isamarkuptext}% -\isacommand{consts}~itrev~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline +\isacommand{consts}\ itrev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline \isacommand{primrec}\isanewline -{"}itrev~[]~~~~~ys~=~ys{"}\isanewline -{"}itrev~(x\#xs)~ys~=~itrev~xs~(x\#ys){"}% +{"}itrev\ []\ \ \ \ \ ys\ =\ ys{"}\isanewline +{"}itrev\ (x\#xs)\ ys\ =\ itrev\ xs\ (x\#ys){"}% \begin{isamarkuptext}% \noindent The behaviour of \isa{itrev} is simple: it reverses its first argument by stacking its elements onto the second argument, @@ -21,12 +21,12 @@ Naturally, we would like to show that \isa{itrev} does indeed reverse its first argument provided the second one is empty:% \end{isamarkuptext}% -\isacommand{lemma}~{"}itrev~xs~[]~=~rev~xs{"}% +\isacommand{lemma}\ {"}itrev\ xs\ []\ =\ rev\ xs{"}% \begin{isamarkuptxt}% \noindent There is no choice as to the induction variable, and we immediately simplify:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac~xs,~auto)% +\isacommand{apply}(induct\_tac\ xs,\ auto)% \begin{isamarkuptxt}% \noindent Unfortunately, this is not a complete success: @@ -43,11 +43,11 @@ Of course one cannot do this na\"{\i}vely: \isa{itrev xs ys = rev xs} is just not true---the correct generalization is% \end{isamarkuptxt}% -\isacommand{lemma}~{"}itrev~xs~ys~=~rev~xs~@~ys{"}% +\isacommand{lemma}\ {"}itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}% \begin{isamarkuptxt}% \noindent If \isa{ys} is replaced by \isa{[]}, the right-hand side simplifies to -\isa{rev xs}, just as required. +\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 @@ -64,10 +64,10 @@ 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 +\isa{a\ \#\ ys} instead of \isa{ys}. Hence we prove the theorem for all \isa{ys} instead of a fixed one:% \end{isamarkuptxt}% -\isacommand{lemma}~{"}{\isasymforall}ys.~itrev~xs~ys~=~rev~xs~@~ys{"}% +\isacommand{lemma}\ {"}{\isasymforall}ys.\ itrev\ xs\ ys\ =\ rev\ xs\ @\ ys{"}% \begin{isamarkuptxt}% \noindent This time induction on \isa{xs} followed by simplification succeeds. This diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/Tree.tex --- a/doc-src/TutorialI/Misc/document/Tree.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Sun Aug 06 15:26:53 2000 +0200 @@ -4,19 +4,19 @@ \noindent Define the datatype of binary trees% \end{isamarkuptext}% -\isacommand{datatype}~'a~tree~=~Tip~|~Node~{"}'a~tree{"}~'a~{"}'a~tree{"}% +\isacommand{datatype}\ 'a\ tree\ =\ Tip\ |\ Node\ {"}'a\ tree{"}\ 'a\ {"}'a\ tree{"}% \begin{isamarkuptext}% \noindent and a function \isa{mirror} that mirrors a binary tree by swapping subtrees (recursively). Prove% \end{isamarkuptext}% -\isacommand{lemma}~mirror\_mirror:~{"}mirror(mirror~t)~=~t{"}% +\isacommand{lemma}\ mirror\_mirror:\ {"}mirror(mirror\ t)\ =\ t{"}% \begin{isamarkuptext}% \noindent Define a function \isa{flatten} that flattens a tree into a list by traversing it in infix order. Prove% \end{isamarkuptext}% -\isacommand{lemma}~{"}flatten(mirror~t)~=~rev(flatten~t){"}\end{isabelle}% +\isacommand{lemma}\ {"}flatten(mirror\ t)\ =\ rev(flatten\ t){"}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/Tree2.tex --- a/doc-src/TutorialI/Misc/document/Tree2.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/Tree2.tex Sun Aug 06 15:26:53 2000 +0200 @@ -7,11 +7,11 @@ A linear time version of \isa{flatten} again reqires an extra argument, the accumulator:% \end{isamarkuptext}% -\isacommand{consts}~flatten2~::~{"}'a~tree~=>~'a~list~=>~'a~list{"}% +\isacommand{consts}\ flatten2\ ::\ {"}'a\ tree\ =>\ 'a\ list\ =>\ 'a\ list{"}% \begin{isamarkuptext}% \noindent Define \isa{flatten2} and prove% \end{isamarkuptext}% -\isacommand{lemma}~{"}flatten2~t~[]~=~flatten~t{"}\end{isabelle}% +\isacommand{lemma}\ {"}flatten2\ t\ []\ =\ flatten\ t{"}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/arith1.tex --- a/doc-src/TutorialI/Misc/document/arith1.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith1.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}~{"}{\isasymlbrakk}~{\isasymnot}~m~<~n;~m~<~n+1~{\isasymrbrakk}~{\isasymLongrightarrow}~m~=~n{"}\isanewline +\isacommand{lemma}\ {"}{\isasymlbrakk}\ {\isasymnot}\ m\ <\ n;\ m\ <\ n+1\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/arith2.tex --- a/doc-src/TutorialI/Misc/document/arith2.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith2.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}~{"}min~i~(max~j~(k*k))~=~max~(min~(k*k)~i)~(min~i~(j::nat)){"}\isanewline +\isacommand{lemma}\ {"}min\ i\ (max\ j\ (k*k))\ =\ max\ (min\ (k*k)\ i)\ (min\ i\ (j::nat)){"}\isanewline \isacommand{by}(arith)\isanewline \end{isabelle}% %%% Local Variables: diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/arith3.tex --- a/doc-src/TutorialI/Misc/document/arith3.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith3.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}~{"}n*n~=~n~{\isasymLongrightarrow}~n=0~{\isasymor}~n=1{"}\isanewline +\isacommand{lemma}\ {"}n*n\ =\ n\ {\isasymLongrightarrow}\ n=0\ {\isasymor}\ n=1{"}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/arith4.tex --- a/doc-src/TutorialI/Misc/document/arith4.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/arith4.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{lemma}~{"}{\isasymnot}~m~<~n~{\isasymand}~m~<~n+1~{\isasymLongrightarrow}~m~=~n{"}\isanewline +\isacommand{lemma}\ {"}{\isasymnot}\ m\ <\ n\ {\isasymand}\ m\ <\ n+1\ {\isasymLongrightarrow}\ m\ =\ n{"}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/asm_simp.tex --- a/doc-src/TutorialI/Misc/document/asm_simp.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/asm_simp.tex Sun Aug 06 15:26:53 2000 +0200 @@ -4,27 +4,27 @@ By default, assumptions are part of the simplification process: they are used as simplification rules and are simplified themselves. For example:% \end{isamarkuptext}% -\isacommand{lemma}~{"}{\isasymlbrakk}~xs~@~zs~=~ys~@~xs;~[]~@~xs~=~[]~@~[]~{\isasymrbrakk}~{\isasymLongrightarrow}~ys~=~zs{"}\isanewline -\isacommand{by}~simp% +\isacommand{lemma}\ {"}{\isasymlbrakk}\ xs\ @\ zs\ =\ ys\ @\ xs;\ []\ @\ xs\ =\ []\ @\ []\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ ys\ =\ zs{"}\isanewline +\isacommand{by}\ simp% \begin{isamarkuptext}% \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}. +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:% \end{isamarkuptext}% -\isacommand{lemma}~{"}{\isasymforall}x.~f~x~=~g~(f~(g~x))~{\isasymLongrightarrow}~f~[]~=~f~[]~@~[]{"}% +\isacommand{lemma}\ {"}{\isasymforall}x.\ f\ x\ =\ g\ (f\ (g\ x))\ {\isasymLongrightarrow}\ f\ []\ =\ f\ []\ @\ []{"}% \begin{isamarkuptxt}% \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 +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:% \end{isamarkuptxt}% -\isacommand{by}(simp~(no\_asm))% +\isacommand{by}(simp\ (no\_asm))% \begin{isamarkuptext}% \noindent There are three options that influence the treatment of assumptions: diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/case_splits.tex --- a/doc-src/TutorialI/Misc/document/case_splits.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex Sun Aug 06 15:26:53 2000 +0200 @@ -4,7 +4,7 @@ Goals containing \isaindex{if}-expressions are usually proved by case distinction on the condition of the \isa{if}. For example the goal% \end{isamarkuptext}% -\isacommand{lemma}~{"}{\isasymforall}xs.~if~xs~=~[]~then~rev~xs~=~[]~else~rev~xs~{\isasymnoteq}~[]{"}% +\isacommand{lemma}\ {"}{\isasymforall}xs.\ if\ xs\ =\ []\ then\ rev\ xs\ =\ []\ else\ rev\ xs\ {\isasymnoteq}\ []{"}% \begin{isamarkuptxt}% \noindent can be split into @@ -13,7 +13,7 @@ \end{isabellepar}% by a degenerate form of simplification% \end{isamarkuptxt}% -\isacommand{apply}(simp~only:~split:~split\_if)% +\isacommand{apply}(simp\ only:\ split:\ split\_if)% \begin{isamarkuptext}% \noindent where no simplification rules are included (\isa{only:} is followed by the @@ -25,7 +25,7 @@ This splitting idea generalizes from \isa{if} to \isaindex{case}:% \end{isamarkuptext}% -\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~zs~|~y\#ys~{\isasymRightarrow}~y\#(ys@zs))~=~xs@zs{"}% +\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ zs\ |\ y\#ys\ {\isasymRightarrow}\ y\#(ys@zs))\ =\ xs@zs{"}% \begin{isamarkuptxt}% \noindent becomes @@ -35,7 +35,7 @@ \end{isabellepar}% by typing% \end{isamarkuptxt}% -\isacommand{apply}(simp~only:~split:~list.split)% +\isacommand{apply}(simp\ only:\ split:\ list.split)% \begin{isamarkuptext}% \noindent In contrast to \isa{if}-expressions, the simplifier does not split @@ -43,7 +43,7 @@ in case of recursive datatypes. Again, if the \isa{only:} modifier is dropped, the above goal is solved,% \end{isamarkuptext}% -\isacommand{by}(simp~split:~list.split)% +\isacommand{by}(simp\ split:\ list.split)% \begin{isamarkuptext}% \noindent% which \isacommand{apply}\isa{(simp)} alone will not do. @@ -52,18 +52,18 @@ \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:% \end{isamarkuptext}% -\isacommand{theorems}~[split]~=~list.split% +\isacommand{lemmas}\ [split]\ =\ list.split% \begin{isamarkuptext}% \noindent The \isa{split} attribute can be removed with the \isa{del} modifier, either locally% \end{isamarkuptext}% -\isacommand{apply}(simp~split~del:~split\_if)% +\isacommand{apply}(simp\ split\ del:\ split\_if)% \begin{isamarkuptext}% \noindent or globally:% \end{isamarkuptext}% -\isacommand{theorems}~[split~del]~=~list.split\isanewline +\isacommand{lemmas}\ [split\ del]\ =\ list.split\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/cases.tex --- a/doc-src/TutorialI/Misc/document/cases.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cases.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% \isanewline -\isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline -\isacommand{apply}(case\_tac~xs)% +\isacommand{lemma}\ {"}(case\ xs\ of\ []\ {\isasymRightarrow}\ []\ |\ y\#ys\ {\isasymRightarrow}\ xs)\ =\ xs{"}\isanewline +\isacommand{apply}(case\_tac\ xs)% \begin{isamarkuptxt}% \noindent results in the proof state diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/cond_rewr.tex --- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Sun Aug 06 15:26:53 2000 +0200 @@ -4,19 +4,16 @@ So far all examples of rewrite rules were equations. The simplifier also accepts \emph{conditional} equations, for example% \end{isamarkuptext}% -\isacommand{lemma}~hd\_Cons\_tl[simp]:~{"}xs~{\isasymnoteq}~[]~~{\isasymLongrightarrow}~~hd~xs~\#~tl~xs~=~xs{"}\isanewline -\isacommand{by}(case\_tac~xs,~simp,~simp)% +\isacommand{lemma}\ hd\_Cons\_tl[simp]:\ {"}xs\ {\isasymnoteq}\ []\ \ {\isasymLongrightarrow}\ \ hd\ xs\ \#\ tl\ xs\ =\ xs{"}\isanewline +\isacommand{by}(case\_tac\ xs,\ simp,\ simp)% \begin{isamarkuptext}% \noindent Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a -sequence of methods. Assuming that the simplification rule% -\end{isamarkuptext}% -~{"}(rev~xs~=~[])~=~(xs~=~[]){"}% -\begin{isamarkuptext}% -\noindent +sequence of methods. Assuming that the simplification rule +\isa{(rev\ xs\ =\ [])\ =\ (xs\ =\ [])} is present as well,% \end{isamarkuptext}% -\isacommand{lemma}~{"}xs~{\isasymnoteq}~[]~{\isasymLongrightarrow}~hd(rev~xs)~\#~tl(rev~xs)~=~rev~xs{"}% +\isacommand{lemma}\ {"}xs\ {\isasymnoteq}\ []\ {\isasymLongrightarrow}\ hd(rev\ xs)\ \#\ tl(rev\ xs)\ =\ rev\ xs{"}% \begin{isamarkuptext}% \noindent is proved by plain simplification: diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/def_rewr.tex --- a/doc-src/TutorialI/Misc/document/def_rewr.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/def_rewr.tex Sun Aug 06 15:26:53 2000 +0200 @@ -9,19 +9,19 @@ enough lemmas that characterize the concept sufficiently for us to forget the original definition. For example, given% \end{isamarkuptext}% -\isacommand{constdefs}~exor~::~{"}bool~{\isasymRightarrow}~bool~{\isasymRightarrow}~bool{"}\isanewline -~~~~~~~~~{"}exor~A~B~{\isasymequiv}~(A~{\isasymand}~{\isasymnot}B)~{\isasymor}~({\isasymnot}A~{\isasymand}~B){"}% +\isacommand{constdefs}\ exor\ ::\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline +\ \ \ \ \ \ \ \ \ {"}exor\ A\ B\ {\isasymequiv}\ (A\ {\isasymand}\ {\isasymnot}B)\ {\isasymor}\ ({\isasymnot}A\ {\isasymand}\ B){"}% \begin{isamarkuptext}% \noindent we may want to prove% \end{isamarkuptext}% -\isacommand{lemma}~{"}exor~A~({\isasymnot}A){"}% +\isacommand{lemma}\ {"}exor\ A\ ({\isasymnot}A){"}% \begin{isamarkuptxt}% \noindent There is a special method for \emph{unfolding} definitions, which we need to get started:\indexbold{*unfold}\indexbold{definition!unfolding}% \end{isamarkuptxt}% -\isacommand{apply}(unfold~exor\_def)% +\isacommand{apply}(unfold\ exor\_def)% \begin{isamarkuptxt}% \noindent It unfolds the given list of definitions (here merely one) in all subgoals: @@ -33,7 +33,7 @@ In case we want to expand a definition in the middle of a proof, we can simply include it locally:% \end{isamarkuptxt}% -\isacommand{apply}(simp~add:~exor\_def)% +\isacommand{apply}(simp\ add:\ exor\_def)% \begin{isamarkuptext}% \noindent In fact, this one command proves the above lemma directly. diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/fakenat.tex --- a/doc-src/TutorialI/Misc/document/fakenat.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/fakenat.tex Sun Aug 06 15:26:53 2000 +0200 @@ -5,7 +5,7 @@ The type \isaindexbold{nat}\index{*0|bold}\index{*Suc|bold} of natural numbers is predefined and behaves like% \end{isamarkuptext}% -\isacommand{datatype}~nat~=~{"}0{"}~|~Suc~nat\end{isabelle}% +\isacommand{datatype}\ nat\ =\ 0\ |\ Suc\ nat\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/let_rewr.tex --- a/doc-src/TutorialI/Misc/document/let_rewr.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,11 +1,11 @@ \begin{isabelle}% -\isacommand{lemma}~{"}(let~xs~=~[]~in~xs@ys@xs)~=~ys{"}\isanewline -\isacommand{by}(simp~add:~Let\_def)% +\isacommand{lemma}\ {"}(let\ xs\ =\ []\ in\ xs@ys@xs)\ =\ ys{"}\isanewline +\isacommand{by}(simp\ add:\ Let\_def)% \begin{isamarkuptext}% If, in a particular context, there is no danger of a combinatorial explosion of nested \isa{let}s one could even add \isa{Let_def} permanently:% \end{isamarkuptext}% -\isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}% +\isacommand{lemmas}\ [simp]\ =\ Let\_def\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/natsum.tex --- a/doc-src/TutorialI/Misc/document/natsum.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/natsum.tex Sun Aug 06 15:26:53 2000 +0200 @@ -2,22 +2,25 @@ % \begin{isamarkuptext}% \noindent -In particular, there are \isa{case}-expressions, for example% -\end{isamarkuptext}% -~{"}case~n~of~0~{\isasymRightarrow}~0~|~Suc~m~{\isasymRightarrow}~m{"}% -\begin{isamarkuptext}% -\noindent +In particular, there are \isa{case}-expressions, for example +\begin{quote} + +\begin{isabelle}% +case\ n\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ m\ {\isasymRightarrow}\ m +\end{isabelle}% + +\end{quote} primitive recursion, for example% \end{isamarkuptext}% -\isacommand{consts}~sum~::~{"}nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{primrec}~{"}sum~0~=~0{"}\isanewline -~~~~~~~~{"}sum~(Suc~n)~=~Suc~n~+~sum~n{"}% +\isacommand{consts}\ sum\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{primrec}\ {"}sum\ 0\ =\ 0{"}\isanewline +\ \ \ \ \ \ \ \ {"}sum\ (Suc\ n)\ =\ Suc\ n\ +\ sum\ n{"}% \begin{isamarkuptext}% \noindent and induction, for example% \end{isamarkuptext}% -\isacommand{lemma}~{"}sum~n~+~sum~n~=~n*(Suc~n){"}\isanewline -\isacommand{apply}(induct\_tac~n)\isanewline +\isacommand{lemma}\ {"}sum\ n\ +\ sum\ n\ =\ n*(Suc\ n){"}\isanewline +\isacommand{apply}(induct\_tac\ n)\isanewline \isacommand{by}(auto)\isanewline \end{isabelle}% %%% Local Variables: diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/pairs.tex --- a/doc-src/TutorialI/Misc/document/pairs.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,25 @@ \begin{isabelle}% -~{"}let~(x,y)~=~f~z~in~(y,x){"}~{"}case~xs~of~[]~{\isasymRightarrow}~0~|~(x,y)\#zs~{\isasymRightarrow}~x+y{"}\isanewline +% +\begin{isamarkuptext}% +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ * + $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair +are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and +\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right: +\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and +\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ * + $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. + +It is possible to use (nested) tuples as patterns in abstractions, for +example \isa{\isasymlambda(x,y,z).x+y+z} and +\isa{\isasymlambda((x,y),z).x+y+z}. +In addition to explicit $\lambda$-abstractions, tuple patterns can be used in +most variable binding constructs. Typical examples are +\begin{quote} +\isa{let\ (x,\ y)\ =\ f\ z\ in\ (y,\ x)}\\ +\isa{case\ xs\ of\ []\ {\isasymRightarrow}\ 0\ |\ (x,\ y)\ \#\ zs\ {\isasymRightarrow}\ x\ +\ y} +\end{quote} +Further important examples are quantifiers and sets (see~\S\ref{quant-pats}).% +\end{isamarkuptext}% \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/prime_def.tex --- a/doc-src/TutorialI/Misc/document/prime_def.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/prime_def.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,6 +1,6 @@ \begin{isabelle}% \isanewline -~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~(m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}% +\ \ \ \ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ (m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}% \begin{isamarkuptext}% \noindent\small where \isa{dvd} means ``divides''. @@ -8,7 +8,7 @@ right-hand side, which would introduce an inconsistency (why?). What you should have written is% \end{isamarkuptext}% -~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}% +\ {"}prime(p)\ {\isasymequiv}\ 1\ <\ p\ {\isasymand}\ ({\isasymforall}m.\ m\ dvd\ p\ {\isasymlongrightarrow}\ (m=1\ {\isasymor}\ m=p)){"}\end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/trace_simp.tex --- a/doc-src/TutorialI/Misc/document/trace_simp.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/trace_simp.tex Sun Aug 06 15:26:53 2000 +0200 @@ -5,8 +5,8 @@ \ttindexbold{trace_simp} \rmindex{flag} to get a better idea of what is going on:% \end{isamarkuptext}% -\isacommand{ML}~{"}set~trace\_simp{"}\isanewline -\isacommand{lemma}~{"}rev~[a]~=~[]{"}\isanewline +\isacommand{ML}\ {"}set\ trace\_simp{"}\isanewline +\isacommand{lemma}\ {"}rev\ [a]\ =\ []{"}\isanewline \isacommand{apply}(simp)% \begin{isamarkuptxt}% \noindent @@ -35,7 +35,7 @@ invocations of the simplifier are often nested (e.g.\ when solving conditions of rewrite rules). Thus it is advisable to reset it:% \end{isamarkuptxt}% -\isacommand{ML}~{"}reset~trace\_simp{"}\isanewline +\isacommand{ML}\ {"}reset\ trace\_simp{"}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/document/types.tex --- a/doc-src/TutorialI/Misc/document/types.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/types.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,7 +1,7 @@ \begin{isabelle}% -\isacommand{types}~number~~~~~~~=~nat\isanewline -~~~~~~gate~~~~~~~~~=~{"}bool~{\isasymRightarrow}~bool~{\isasymRightarrow}~bool{"}\isanewline -~~~~~~('a,'b)alist~=~{"}('a~*~'b)list{"}% +\isacommand{types}\ number\ \ \ \ \ \ \ =\ nat\isanewline +\ \ \ \ \ \ gate\ \ \ \ \ \ \ \ \ =\ {"}bool\ {\isasymRightarrow}\ bool\ {\isasymRightarrow}\ bool{"}\isanewline +\ \ \ \ \ \ ('a,'b)alist\ =\ {"}('a\ *\ 'b)list{"}% \begin{isamarkuptext}% \noindent\indexbold{*types}% Internally all synonyms are fully expanded. As a consequence Isabelle's @@ -9,8 +9,8 @@ readability of theories. Synonyms can be used just like any other type:% \end{isamarkuptext}% -\isacommand{consts}~nand~::~gate\isanewline -~~~~~~~exor~::~gate% +\isacommand{consts}\ nand\ ::\ gate\isanewline +\ \ \ \ \ \ \ exor\ ::\ gate% \begin{isamarkuptext}% \subsection{Constant definitions} \label{sec:ConstDefinitions} @@ -19,20 +19,20 @@ The above constants \isa{nand} and \isa{exor} are non-recursive and can therefore be defined directly by% \end{isamarkuptext}% -\isacommand{defs}~nand\_def:~{"}nand~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymand}~B){"}\isanewline -~~~~~exor\_def:~{"}exor~A~B~{\isasymequiv}~A~{\isasymand}~{\isasymnot}B~{\isasymor}~{\isasymnot}A~{\isasymand}~B{"}% +\isacommand{defs}\ nand\_def:\ {"}nand\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymand}\ B){"}\isanewline +\ \ \ \ \ exor\_def:\ {"}exor\ A\ B\ {\isasymequiv}\ A\ {\isasymand}\ {\isasymnot}B\ {\isasymor}\ {\isasymnot}A\ {\isasymand}\ B{"}% \begin{isamarkuptext}% \noindent% where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and \isa{exor_def} are user-supplied names. The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality -that should only be used in constant definitions. +that must be used in constant definitions. Declarations and definitions can also be merged% \end{isamarkuptext}% -\isacommand{constdefs}~nor~::~gate\isanewline -~~~~~~~~~{"}nor~A~B~{\isasymequiv}~{\isasymnot}(A~{\isasymor}~B){"}\isanewline -~~~~~~~~~~exor2~::~gate\isanewline -~~~~~~~~~{"}exor2~A~B~{\isasymequiv}~(A~{\isasymor}~B)~{\isasymand}~({\isasymnot}A~{\isasymor}~{\isasymnot}B){"}% +\isacommand{constdefs}\ nor\ ::\ gate\isanewline +\ \ \ \ \ \ \ \ \ {"}nor\ A\ B\ {\isasymequiv}\ {\isasymnot}(A\ {\isasymor}\ B){"}\isanewline +\ \ \ \ \ \ \ \ \ \ exor2\ ::\ gate\isanewline +\ \ \ \ \ \ \ \ \ {"}exor2\ A\ B\ {\isasymequiv}\ (A\ {\isasymor}\ B)\ {\isasymand}\ ({\isasymnot}A\ {\isasymor}\ {\isasymnot}B){"}% \begin{isamarkuptext}% \noindent\indexbold{*constdefs}% in which case the default name of each definition is \isa{$f$_def}, where diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/fakenat.thy --- a/doc-src/TutorialI/Misc/fakenat.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/fakenat.thy Sun Aug 06 15:26:53 2000 +0200 @@ -7,7 +7,7 @@ numbers is predefined and behaves like *} -datatype nat = "0" | Suc nat +datatype nat = 0 | Suc nat (*<*) end (*>*) diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/let_rewr.thy --- a/doc-src/TutorialI/Misc/let_rewr.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/let_rewr.thy Sun Aug 06 15:26:53 2000 +0200 @@ -8,7 +8,7 @@ If, in a particular context, there is no danger of a combinatorial explosion of nested \isa{let}s one could even add \isa{Let_def} permanently: *} -theorems [simp] = Let_def; +lemmas [simp] = Let_def; (*<*) end (*>*) diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/natsum.thy --- a/doc-src/TutorialI/Misc/natsum.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/natsum.thy Sun Aug 06 15:26:53 2000 +0200 @@ -3,11 +3,9 @@ (*>*) text{*\noindent In particular, there are \isa{case}-expressions, for example -*} - -(*<*)term(*>*) "case n of 0 \\ 0 | Suc m \\ m"; - -text{*\noindent +\begin{quote} +@{term[display]"case n of 0 => 0 | Suc m => m"} +\end{quote} primitive recursion, for example *} diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/pairs.thy --- a/doc-src/TutorialI/Misc/pairs.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/pairs.thy Sun Aug 06 15:26:53 2000 +0200 @@ -1,8 +1,26 @@ (*<*) theory pairs = Main:; -term(*>*) "let (x,y) = f z in (y,x)"; +(*>*) +text{* +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ * + $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair +are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and +\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right: +\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and +\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ * + $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. + +It is possible to use (nested) tuples as patterns in abstractions, for +example \isa{\isasymlambda(x,y,z).x+y+z} and +\isa{\isasymlambda((x,y),z).x+y+z}. +In addition to explicit $\lambda$-abstractions, tuple patterns can be used in +most variable binding constructs. Typical examples are +\begin{quote} +@{term"let (x,y) = f z in (y,x)"}\\ +@{term"case xs of [] => 0 | (x,y)#zs => x+y"} +\end{quote} +Further important examples are quantifiers and sets (see~\S\ref{quant-pats}). +*} (*<*) -term(*>*) "case xs of [] \\ 0 | (x,y)#zs \\ x+y" -(**)(*<*) end (*>*) diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Misc/types.thy --- a/doc-src/TutorialI/Misc/types.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Misc/types.thy Sun Aug 06 15:26:53 2000 +0200 @@ -30,7 +30,7 @@ where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and \isa{exor_def} are user-supplied names. The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality -that should only be used in constant definitions. +that must be used in constant definitions. Declarations and definitions can also be merged *} diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Recdef/document/Induction.tex --- a/doc-src/TutorialI/Recdef/document/Induction.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Sun Aug 06 15:26:53 2000 +0200 @@ -15,14 +15,14 @@ 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% \end{isamarkuptext}% -\isacommand{lemma}~{"}map~f~(sep(x,xs))~=~sep(f~x,~map~f~xs){"}% +\isacommand{lemma}\ {"}map\ f\ (sep(x,xs))\ =\ sep(f\ x,\ map\ f\ xs){"}% \begin{isamarkuptxt}% \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}:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac~x~xs~rule:~sep.induct)% +\isacommand{apply}(induct\_tac\ x\ xs\ rule:\ sep.induct)% \begin{isamarkuptxt}% \noindent The resulting proof state has three subgoals corresponding to the three @@ -36,7 +36,7 @@ \end{isabellepar}% The rest is pure simplification:% \end{isamarkuptxt}% -\isacommand{by}~auto% +\isacommand{by}\ auto% \begin{isamarkuptext}% 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 diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Recdef/document/examples.tex --- a/doc-src/TutorialI/Recdef/document/examples.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Sun Aug 06 15:26:53 2000 +0200 @@ -3,30 +3,30 @@ \begin{isamarkuptext}% Here is a simple example, the Fibonacci function:% \end{isamarkuptext}% -\isacommand{consts}~fib~::~{"}nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{recdef}~fib~{"}measure({\isasymlambda}n.~n){"}\isanewline -~~{"}fib~0~=~0{"}\isanewline -~~{"}fib~1~=~1{"}\isanewline -~~{"}fib~(Suc(Suc~x))~=~fib~x~+~fib~(Suc~x){"}% +\isacommand{consts}\ fib\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{recdef}\ fib\ {"}measure({\isasymlambda}n.\ n){"}\isanewline +\ \ {"}fib\ 0\ =\ 0{"}\isanewline +\ \ {"}fib\ 1\ =\ 1{"}\isanewline +\ \ {"}fib\ (Suc(Suc\ x))\ =\ fib\ x\ +\ fib\ (Suc\ x){"}% \begin{isamarkuptext}% \noindent The definition of \isa{fib} is accompanied by a \bfindex{measure function} -\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a +\isa{{\isasymlambda}n.\ n} which 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}. +\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:% \end{isamarkuptext}% -\isacommand{consts}~sep~::~{"}'a~*~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline -\isacommand{recdef}~sep~{"}measure~({\isasymlambda}(a,xs).~length~xs){"}\isanewline -~~{"}sep(a,~[])~~~~~=~[]{"}\isanewline -~~{"}sep(a,~[x])~~~~=~[x]{"}\isanewline -~~{"}sep(a,~x\#y\#zs)~=~x~\#~a~\#~sep(a,y\#zs){"}% +\isacommand{consts}\ sep\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline +\isacommand{recdef}\ sep\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline +\ \ {"}sep(a,\ [])\ \ \ \ \ =\ []{"}\isanewline +\ \ {"}sep(a,\ [x])\ \ \ \ =\ [x]{"}\isanewline +\ \ {"}sep(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep(a,y\#zs){"}% \begin{isamarkuptext}% \noindent This time the measure is the length of the list, which decreases with the @@ -34,18 +34,18 @@ Pattern matching need not be exhaustive:% \end{isamarkuptext}% -\isacommand{consts}~last~::~{"}'a~list~{\isasymRightarrow}~'a{"}\isanewline -\isacommand{recdef}~last~{"}measure~({\isasymlambda}xs.~length~xs){"}\isanewline -~~{"}last~[x]~~~~~~=~x{"}\isanewline -~~{"}last~(x\#y\#zs)~=~last~(y\#zs){"}% +\isacommand{consts}\ last\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}\isanewline +\isacommand{recdef}\ last\ {"}measure\ ({\isasymlambda}xs.\ length\ xs){"}\isanewline +\ \ {"}last\ [x]\ \ \ \ \ \ =\ x{"}\isanewline +\ \ {"}last\ (x\#y\#zs)\ =\ last\ (y\#zs){"}% \begin{isamarkuptext}% Overlapping patterns are disambiguated by taking the order of equations into account, just as in functional programming:% \end{isamarkuptext}% -\isacommand{consts}~sep1~::~{"}'a~*~'a~list~{\isasymRightarrow}~'a~list{"}\isanewline -\isacommand{recdef}~sep1~{"}measure~({\isasymlambda}(a,xs).~length~xs){"}\isanewline -~~{"}sep1(a,~x\#y\#zs)~=~x~\#~a~\#~sep1(a,y\#zs){"}\isanewline -~~{"}sep1(a,~xs)~~~~~=~xs{"}% +\isacommand{consts}\ sep1\ ::\ {"}'a\ *\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline +\isacommand{recdef}\ sep1\ {"}measure\ ({\isasymlambda}(a,xs).\ length\ xs){"}\isanewline +\ \ {"}sep1(a,\ x\#y\#zs)\ =\ x\ \#\ a\ \#\ sep1(a,y\#zs){"}\isanewline +\ \ {"}sep1(a,\ xs)\ \ \ \ \ =\ xs{"}% \begin{isamarkuptext}% \noindent This defines exactly the same function as \isa{sep} above, i.e.\ @@ -60,18 +60,18 @@ arguments as in the following definition: \end{warn}% \end{isamarkuptext}% -\isacommand{consts}~sep2~::~{"}'a~list~{\isasymRightarrow}~'a~{\isasymRightarrow}~'a~list{"}\isanewline -\isacommand{recdef}~sep2~{"}measure~length{"}\isanewline -~~{"}sep2~(x\#y\#zs)~=~({\isasymlambda}a.~x~\#~a~\#~sep2~zs~a){"}\isanewline -~~{"}sep2~xs~~~~~~~=~({\isasymlambda}a.~xs){"}% +\isacommand{consts}\ sep2\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ {\isasymRightarrow}\ 'a\ list{"}\isanewline +\isacommand{recdef}\ sep2\ {"}measure\ length{"}\isanewline +\ \ {"}sep2\ (x\#y\#zs)\ =\ ({\isasymlambda}a.\ x\ \#\ a\ \#\ sep2\ zs\ a){"}\isanewline +\ \ {"}sep2\ xs\ \ \ \ \ \ \ =\ ({\isasymlambda}a.\ xs){"}% \begin{isamarkuptext}% Because of its pattern-matching syntax, \isacommand{recdef} is also useful for the definition of non-recursive functions:% \end{isamarkuptext}% -\isacommand{consts}~swap12~::~{"}'a~list~{\isasymRightarrow}~'a~list{"}\isanewline -\isacommand{recdef}~swap12~{"}{\isabraceleft}{\isabraceright}{"}\isanewline -~~{"}swap12~(x\#y\#zs)~=~y\#x\#zs{"}\isanewline -~~{"}swap12~zs~~~~~~~=~zs{"}% +\isacommand{consts}\ swap12\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\isanewline +\isacommand{recdef}\ swap12\ {"}{\isabraceleft}{\isabraceright}{"}\isanewline +\ \ {"}swap12\ (x\#y\#zs)\ =\ y\#x\#zs{"}\isanewline +\ \ {"}swap12\ zs\ \ \ \ \ \ \ =\ zs{"}% \begin{isamarkuptext}% \noindent For non-recursive functions the termination measure degenerates to the empty diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Sun Aug 06 15:26:53 2000 +0200 @@ -8,17 +8,20 @@ terminate because of automatic splitting of \isa{if}. Let us look at an example:% \end{isamarkuptext}% -\isacommand{consts}~gcd~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{recdef}~gcd~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline -~~{"}gcd~(m,~n)~=~(if~n=0~then~m~else~gcd(n,~m~mod~n)){"}% +\isacommand{consts}\ gcd\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{recdef}\ gcd\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline +\ \ {"}gcd\ (m,\ n)\ =\ (if\ n=0\ then\ m\ else\ gcd(n,\ m\ mod\ n)){"}% \begin{isamarkuptext}% \noindent According to the measure function, the second argument should decrease with -each recursive call. The resulting termination condition% -\end{isamarkuptext}% -~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~m~mod~n~<~n{"}% -\begin{isamarkuptext}% -\noindent +each recursive call. The resulting termination condition +\begin{quote} + +\begin{isabelle}% +n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ m\ mod\ n\ <\ n +\end{isabelle}% + +\end{quote} 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 @@ -26,24 +29,34 @@ 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% -\end{isamarkuptext}% -~{"}gcd(m,n)~=~k{"}% -\begin{isamarkuptext}% -\noindent -in one step to% -\end{isamarkuptext}% -~{"}(if~n=0~then~m~else~gcd(n,~m~mod~n))~=~k{"}% -\begin{isamarkuptext}% -\noindent -where the condition cannot be reduced further, and splitting leads to% -\end{isamarkuptext}% -~{"}(n=0~{\isasymlongrightarrow}~m=k)~{\isasymand}~(n{\isasymnoteq}0~{\isasymlongrightarrow}~gcd(n,~m~mod~n)=k){"}% -\begin{isamarkuptext}% -\noindent -Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by -an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps. -Fortunately, this problem can be avoided in many different ways. +example, simplification reduces +\begin{quote} + +\begin{isabelle}% +gcd\ (m,\ n)\ =\ k +\end{isabelle}% + +\end{quote} +in one step to +\begin{quote} + +\begin{isabelle}% +(if\ n\ =\ 0\ then\ m\ else\ gcd\ (n,\ m\ mod\ n))\ =\ k +\end{isabelle}% + +\end{quote} +where the condition cannot be reduced further, and splitting leads to +\begin{quote} + +\begin{isabelle}% +(n\ =\ 0\ {\isasymlongrightarrow}\ m\ =\ k)\ {\isasymand}\ (n\ {\isasymnoteq}\ 0\ {\isasymlongrightarrow}\ gcd\ (n,\ m\ mod\ n)\ =\ k) +\end{isabelle}% + +\end{quote} +Since the recursive call \isa{gcd\ (n,\ m\ mod\ n)} is no longer protected by +an \isa{if}, it is unfolded again, which leads to an infinite chain of +simplification steps. Fortunately, this problem can be avoided in many +different ways. The most radical solution is to disable the offending \isa{split_if} as shown in the section on case splits in @@ -55,10 +68,10 @@ rather than \isa{if} on the right. In the case of \isa{gcd} the following alternative definition suggests itself:% \end{isamarkuptext}% -\isacommand{consts}~gcd1~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{recdef}~gcd1~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline -~~{"}gcd1~(m,~0)~=~m{"}\isanewline -~~{"}gcd1~(m,~n)~=~gcd1(n,~m~mod~n){"}% +\isacommand{consts}\ gcd1\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{recdef}\ gcd1\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline +\ \ {"}gcd1\ (m,\ 0)\ =\ m{"}\isanewline +\ \ {"}gcd1\ (m,\ n)\ =\ gcd1(n,\ m\ mod\ n){"}% \begin{isamarkuptext}% \noindent Note that the order of equations is important and hides the side condition @@ -68,9 +81,9 @@ A very simple alternative is to replace \isa{if} by \isa{case}, which is also available for \isa{bool} but is not split automatically:% \end{isamarkuptext}% -\isacommand{consts}~gcd2~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{recdef}~gcd2~{"}measure~({\isasymlambda}(m,n).n){"}\isanewline -~~{"}gcd2(m,n)~=~(case~n=0~of~True~{\isasymRightarrow}~m~|~False~{\isasymRightarrow}~gcd2(n,m~mod~n)){"}% +\isacommand{consts}\ gcd2\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{recdef}\ gcd2\ {"}measure\ ({\isasymlambda}(m,n).n){"}\isanewline +\ \ {"}gcd2(m,n)\ =\ (case\ n=0\ of\ True\ {\isasymRightarrow}\ m\ |\ False\ {\isasymRightarrow}\ gcd2(n,m\ mod\ n)){"}% \begin{isamarkuptext}% \noindent In fact, this is probably the neatest solution next to pattern matching. @@ -78,15 +91,15 @@ A final alternative is to replace the offending simplification rules by derived conditional ones. For \isa{gcd} it means we have to prove% \end{isamarkuptext}% -\isacommand{lemma}~[simp]:~{"}gcd~(m,~0)~=~m{"}\isanewline +\isacommand{lemma}\ [simp]:\ {"}gcd\ (m,\ 0)\ =\ m{"}\isanewline \isacommand{by}(simp)\isanewline -\isacommand{lemma}~[simp]:~{"}n~{\isasymnoteq}~0~{\isasymLongrightarrow}~gcd(m,~n)~=~gcd(n,~m~mod~n){"}\isanewline +\isacommand{lemma}\ [simp]:\ {"}n\ {\isasymnoteq}\ 0\ {\isasymLongrightarrow}\ gcd(m,\ n)\ =\ gcd(n,\ m\ mod\ n){"}\isanewline \isacommand{by}(simp)% \begin{isamarkuptext}% \noindent after which we can disable the original simplification rule:% \end{isamarkuptext}% -\isacommand{lemmas}~[simp~del]~=~gcd.simps\isanewline +\isacommand{lemmas}\ [simp\ del]\ =\ gcd.simps\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Sun Aug 06 15:26:53 2000 +0200 @@ -15,9 +15,9 @@ (there is one for each recursive call) automatically. For example, termination of the following artificial function% \end{isamarkuptext}% -\isacommand{consts}~f~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{recdef}~f~{"}measure({\isasymlambda}(x,y).~x-y){"}\isanewline -~~{"}f(x,y)~=~(if~x~{\isasymle}~y~then~x~else~f(x,y+1)){"}% +\isacommand{consts}\ f\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{recdef}\ f\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline +\ \ {"}f(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ f(x,y+1)){"}% \begin{isamarkuptext}% \noindent is not proved automatically (although maybe it should be). Isabelle prints a @@ -25,7 +25,7 @@ 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:% \end{isamarkuptext}% -\isacommand{lemma}~termi\_lem[simp]:~{"}{\isasymnot}~x~{\isasymle}~y~{\isasymLongrightarrow}~x~-~Suc~y~<~x~-~y{"}% +\isacommand{lemma}\ termi\_lem[simp]:\ {"}{\isasymnot}\ x\ {\isasymle}\ y\ {\isasymLongrightarrow}\ x\ -\ Suc\ y\ <\ x\ -\ y{"}% \begin{isamarkuptxt}% \noindent It was not proved automatically because of the special nature of \isa{-} @@ -38,16 +38,16 @@ we have turned our lemma into a simplification rule. Therefore our second attempt to define our function will automatically take it into account:% \end{isamarkuptext}% -\isacommand{consts}~g~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{recdef}~g~{"}measure({\isasymlambda}(x,y).~x-y){"}\isanewline -~~{"}g(x,y)~=~(if~x~{\isasymle}~y~then~x~else~g(x,y+1)){"}% +\isacommand{consts}\ g\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{recdef}\ g\ {"}measure({\isasymlambda}(x,y).\ x-y){"}\isanewline +\ \ {"}g(x,y)\ =\ (if\ x\ {\isasymle}\ y\ then\ x\ else\ g(x,y+1)){"}% \begin{isamarkuptext}% \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% \end{isamarkuptext}% -\isacommand{theorem}~wow:~{"}g(1,0)~=~g(1,1){"}\isanewline +\isacommand{theorem}\ wow:\ {"}g(1,0)\ =\ g(1,1){"}\isanewline \isacommand{by}(simp)% \begin{isamarkuptext}% \noindent @@ -57,7 +57,7 @@ simplification rule for the sake of the termination proof, we may want to disable it again:% \end{isamarkuptext}% -\isacommand{lemmas}~[simp~del]~=~termi\_lem% +\isacommand{lemmas}\ [simp\ del]\ =\ termi\_lem% \begin{isamarkuptext}% 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 @@ -76,11 +76,11 @@ allows arbitrary wellfounded relations. For example, termination of Ackermann's function requires the lexicographic product \isa{<*lex*>}:% \end{isamarkuptext}% -\isacommand{consts}~ack~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline -\isacommand{recdef}~ack~{"}measure(\%m.~m)~<*lex*>~measure(\%n.~n){"}\isanewline -~~{"}ack(0,n)~~~~~~~~~=~Suc~n{"}\isanewline -~~{"}ack(Suc~m,0)~~~~~=~ack(m,~1){"}\isanewline -~~{"}ack(Suc~m,Suc~n)~=~ack(m,ack(Suc~m,n)){"}% +\isacommand{consts}\ ack\ ::\ {"}nat*nat\ {\isasymRightarrow}\ nat{"}\isanewline +\isacommand{recdef}\ ack\ {"}measure(\%m.\ m)\ <*lex*>\ measure(\%n.\ n){"}\isanewline +\ \ {"}ack(0,n)\ \ \ \ \ \ \ \ \ =\ Suc\ n{"}\isanewline +\ \ {"}ack(Suc\ m,0)\ \ \ \ \ =\ ack(m,\ 1){"}\isanewline +\ \ {"}ack(Suc\ m,Suc\ n)\ =\ ack(m,ack(Suc\ m,n)){"}% \begin{isamarkuptext}% \noindent For details see the manual~\cite{isabelle-HOL} and the examples in the diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Recdef/examples.thy --- a/doc-src/TutorialI/Recdef/examples.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Recdef/examples.thy Sun Aug 06 15:26:53 2000 +0200 @@ -14,13 +14,13 @@ text{*\noindent The definition of \isa{fib} is accompanied by a \bfindex{measure function} -\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a +@{term"%n. n"} which 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}. +@{term"Suc(Suc x)"} is strictly greater than both \isa{x} and +@{term"Suc x"}. Slightly more interesting is the insertion of a fixed element between any two elements of a list: diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Recdef/simplification.thy --- a/doc-src/TutorialI/Recdef/simplification.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Recdef/simplification.thy Sun Aug 06 15:26:53 2000 +0200 @@ -18,11 +18,9 @@ text{*\noindent According to the measure function, the second argument should decrease with each recursive call. The resulting termination condition -*} - -(*<*)term(*>*) "n \\ 0 \\ m mod n < n"; - -text{*\noindent +\begin{quote} +@{term[display]"n ~= 0 ==> m mod n < n"} +\end{quote} 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 @@ -31,26 +29,21 @@ 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 +\begin{quote} +@{term[display]"gcd(m,n) = k"} +\end{quote} in one step to -*} - -(*<*)term(*>*) "(if n=0 then m else gcd(n, m mod n)) = k"; - -text{*\noindent +\begin{quote} +@{term[display]"(if n=0 then m else gcd(n, m mod n)) = k"} +\end{quote} where the condition cannot be reduced further, and splitting leads to -*} - -(*<*)term(*>*) "(n=0 \\ m=k) \\ (n\\0 \\ 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}, it is unfolded again, which leads to an infinite chain of simplification steps. -Fortunately, this problem can be avoided in many different ways. +\begin{quote} +@{term[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"} +\end{quote} +Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by +an \isa{if}, it is unfolded again, which leads to an infinite chain of +simplification steps. Fortunately, this problem can be avoided in many +different ways. The most radical solution is to disable the offending \isa{split_if} as shown in the section on case splits in diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Sun Aug 06 15:26:53 2000 +0200 @@ -15,19 +15,19 @@ 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 +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 +@{typ"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{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 +@{term"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 +(Cons False Nil)} becomes @{term"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$}. +the right, i.e.\ the term @{term"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 @@ -48,8 +48,8 @@ (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 +syntax \isa{app xs ys} the infix +@{term"xs @ ys"}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred form. Both functions are defined recursively: *} @@ -190,8 +190,8 @@ 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 +the only assumption is the induction hypothesis @{term"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. diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Aug 06 15:26:53 2000 +0200 @@ -1,5 +1,5 @@ \begin{isabelle}% -\isacommand{theory}~ToyList~=~PreList:% +\isacommand{theory}\ ToyList\ =\ PreList:% \begin{isamarkuptext}% \noindent HOL already has a predefined theory of lists called \isa{List} --- @@ -9,25 +9,25 @@ theory that contains pretty much everything but lists, thus avoiding ambiguities caused by defining lists twice.% \end{isamarkuptext}% -\isacommand{datatype}~'a~list~=~Nil~~~~~~~~~~~~~~~~~~~~~~~~~~({"}[]{"})\isanewline -~~~~~~~~~~~~~~~~~|~Cons~'a~{"}'a~list{"}~~~~~~~~~~~~(\isakeyword{infixr}~{"}\#{"}~65)% +\isacommand{datatype}\ 'a\ list\ =\ Nil\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ ({"}[]{"})\isanewline +\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |\ Cons\ 'a\ {"}'a\ list{"}\ \ \ \ \ \ \ \ \ \ \ \ (\isakeyword{infixr}\ {"}\#{"}\ 65)% \begin{isamarkuptext}% \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 +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{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 +\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 +(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$}. +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 @@ -38,25 +38,25 @@ \end{warn} Next, two functions \isa{app} and \isaindexbold{rev} are declared:% \end{isamarkuptext}% -\isacommand{consts}~app~::~{"}'a~list~{\isasymRightarrow}~'a~list~{\isasymRightarrow}~'a~list{"}~~~(\isakeyword{infixr}~{"}@{"}~65)\isanewline -~~~~~~~rev~::~{"}'a~list~{\isasymRightarrow}~'a~list{"}% +\isacommand{consts}\ app\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list\ {\isasymRightarrow}\ 'a\ list{"}\ \ \ (\isakeyword{infixr}\ {"}@{"}\ 65)\isanewline +\ \ \ \ \ \ \ rev\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a\ list{"}% \begin{isamarkuptext}% \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 +syntax \isa{app xs ys} the infix +\isa{xs\ @\ ys}\index{$HOL2list@\texttt{\at}|bold} becomes the preferred form. Both functions are defined recursively:% \end{isamarkuptext}% \isacommand{primrec}\isanewline -{"}[]~@~ys~~~~~~~=~ys{"}\isanewline -{"}(x~\#~xs)~@~ys~=~x~\#~(xs~@~ys){"}\isanewline +{"}[]\ @\ ys\ \ \ \ \ \ \ =\ ys{"}\isanewline +{"}(x\ \#\ xs)\ @\ ys\ =\ x\ \#\ (xs\ @\ ys){"}\isanewline \isanewline \isacommand{primrec}\isanewline -{"}rev~[]~~~~~~~~=~[]{"}\isanewline -{"}rev~(x~\#~xs)~~=~(rev~xs)~@~(x~\#~[]){"}% +{"}rev\ []\ \ \ \ \ \ \ \ =\ []{"}\isanewline +{"}rev\ (x\ \#\ xs)\ \ =\ (rev\ xs)\ @\ (x\ \#\ []){"}% \begin{isamarkuptext}% \noindent The equations for \isa{app} and \isa{rev} hardly need comments: @@ -94,7 +94,7 @@ To lessen this burden, quotation marks around a single identifier can be dropped, unless the identifier happens to be a keyword, as in% \end{isamarkuptext}% -\isacommand{consts}~{"}end{"}~::~{"}'a~list~{\isasymRightarrow}~'a{"}% +\isacommand{consts}\ {"}end{"}\ ::\ {"}'a\ list\ {\isasymRightarrow}\ 'a{"}% \begin{isamarkuptext}% \noindent When Isabelle prints a syntax error message, it refers to the HOL syntax as @@ -114,7 +114,7 @@ Our goal is to show that reversing a list twice produces the original list. The input line% \end{isamarkuptext}% -\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}% +\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}% \begin{isamarkuptxt}% \index{*theorem|bold}\index{*simp (attribute)|bold} \begin{itemize} @@ -160,7 +160,7 @@ defined functions are best established by induction. In this case there is not much choice except to induct on \isa{xs}:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac~xs)% +\isacommand{apply}(induct\_tac\ xs)% \begin{isamarkuptxt}% \noindent\index{*induct_tac}% This tells Isabelle to perform induction on variable \isa{xs}. The suffix @@ -183,8 +183,7 @@ 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 +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. @@ -213,7 +212,7 @@ proof}\indexbold{proof!abandon} (at the shell level type \isacommand{oops}\indexbold{*oops}) we start a new proof:% \end{isamarkuptext}% -\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}% +\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}% \begin{isamarkuptxt}% \noindent The keywords \isacommand{theorem}\index{*theorem} and \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate @@ -225,7 +224,7 @@ \isa{ys}. Because \isa{\at} is defined by recursion on the first argument, \isa{xs} is the correct one:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac~xs)% +\isacommand{apply}(induct\_tac\ xs)% \begin{isamarkuptxt}% \noindent This time not even the base case is solved automatically:% @@ -246,8 +245,8 @@ This time the canonical proof procedure% \end{isamarkuptext}% -\isacommand{lemma}~app\_Nil2~[simp]:~{"}xs~@~[]~=~xs{"}\isanewline -\isacommand{apply}(induct\_tac~xs)\isanewline +\isacommand{lemma}\ app\_Nil2\ [simp]:\ {"}xs\ @\ []\ =\ xs{"}\isanewline +\isacommand{apply}(induct\_tac\ xs)\isanewline \isacommand{apply}(auto)% \begin{isamarkuptxt}% \noindent @@ -272,8 +271,8 @@ Going back to the proof of the first lemma% \end{isamarkuptext}% -\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline -\isacommand{apply}(induct\_tac~xs)\isanewline +\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline +\isacommand{apply}(induct\_tac\ xs)\isanewline \isacommand{apply}(auto)% \begin{isamarkuptxt}% \noindent @@ -300,8 +299,8 @@ \begin{comment} \isacommand{oops}% \end{comment} -\isacommand{lemma}~app\_assoc~[simp]:~{"}(xs~@~ys)~@~zs~=~xs~@~(ys~@~zs){"}\isanewline -\isacommand{apply}(induct\_tac~xs)\isanewline +\isacommand{lemma}\ app\_assoc\ [simp]:\ {"}(xs\ @\ ys)\ @\ zs\ =\ xs\ @\ (ys\ @\ zs){"}\isanewline +\isacommand{apply}(induct\_tac\ xs)\isanewline \isacommand{by}(auto)% \begin{isamarkuptext}% \noindent @@ -309,15 +308,15 @@ Now we can go back and prove the first lemma% \end{isamarkuptext}% -\isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}\isanewline -\isacommand{apply}(induct\_tac~xs)\isanewline +\isacommand{lemma}\ rev\_app\ [simp]:\ {"}rev(xs\ @\ ys)\ =\ (rev\ ys)\ @\ (rev\ xs){"}\isanewline +\isacommand{apply}(induct\_tac\ xs)\isanewline \isacommand{by}(auto)% \begin{isamarkuptext}% \noindent and then solve our main theorem:% \end{isamarkuptext}% -\isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}\isanewline -\isacommand{apply}(induct\_tac~xs)\isanewline +\isacommand{theorem}\ rev\_rev\ [simp]:\ {"}rev(rev\ xs)\ =\ xs{"}\isanewline +\isacommand{apply}(induct\_tac\ xs)\isanewline \isacommand{by}(auto)% \begin{isamarkuptext}% \noindent diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/ToyList2/ToyList1 --- a/doc-src/TutorialI/ToyList2/ToyList1 Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/ToyList2/ToyList1 Sun Aug 06 15:26:53 2000 +0200 @@ -1,15 +1,15 @@ -theory ToyList = PreList:; +theory ToyList = PreList: datatype 'a list = Nil ("[]") - | Cons 'a "'a list" (infixr "#" 65); + | Cons 'a "'a list" (infixr "#" 65) consts app :: "'a list => 'a list => 'a list" (infixr "@" 65) - rev :: "'a list => 'a list"; + rev :: "'a list => 'a list" primrec "[] @ ys = ys" -"(x # xs) @ ys = x # (xs @ ys)"; +"(x # xs) @ ys = x # (xs @ ys)" primrec "rev [] = []" -"rev (x # xs) = (rev xs) @ (x # [])"; +"rev (x # xs) = (rev xs) @ (x # [])" diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/ToyList2/ToyList2 --- a/doc-src/TutorialI/ToyList2/ToyList2 Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/ToyList2/ToyList2 Sun Aug 06 15:26:53 2000 +0200 @@ -1,18 +1,18 @@ -lemma app_Nil2 [simp]: "xs @ [] = xs"; -apply(induct_tac xs); -apply(auto); -.; +lemma app_Nil2 [simp]: "xs @ [] = xs" +apply(induct_tac xs) +apply(auto) +. -lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)"; -apply(induct_tac xs); -by(auto); +lemma app_assoc [simp]: "(xs @ ys) @ zs = xs @ (ys @ zs)" +apply(induct_tac xs) +by(auto) -lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; -apply(induct_tac xs); -by(auto); +lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)" +apply(induct_tac xs) +by(auto) -theorem rev_rev [simp]: "rev(rev xs) = xs"; -apply(induct_tac xs); -by(auto); +theorem rev_rev [simp]: "rev(rev xs) = xs" +apply(induct_tac xs) +by(auto) -end; +end diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Sun Aug 06 15:26:53 2000 +0200 @@ -81,8 +81,8 @@ options: *}; -theorems [simp] = Let_def; -theorems [split] = option.split; +lemmas [simp] = Let_def; +lemmas [split] = option.split; text{*\noindent The reason becomes clear when looking (probably after a failed proof @@ -105,7 +105,6 @@ \isa{as} is instantiated. The start of the proof is completely conventional: *}; - apply(induct_tac as, auto); txt{*\noindent @@ -119,15 +118,13 @@ well now. It turns out that instead of induction, case distinction suffices: *}; - -apply(case_tac[!] bs); -by(auto); +by(case_tac[!] bs, 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]} in our case. Individual -subgoal numbers are also allowed. +All methods ending in \isa{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]} in our case. Individual subgoal numbers, +e.g. \isa{[2]} are also allowed. This proof may look surprisingly straightforward. However, note that this comes at a cost: the proof script is unreadable because the diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Sun Aug 06 15:26:53 2000 +0200 @@ -70,8 +70,8 @@ expand all \isa{let}s and to split all \isa{case}-constructs over options:% \end{isamarkuptext}% -\isacommand{theorems}\ [simp]\ =\ Let\_def\isanewline -\isacommand{theorems}\ [split]\ =\ option.split% +\isacommand{lemmas}\ [simp]\ =\ Let\_def\isanewline +\isacommand{lemmas}\ [split]\ =\ option.split% \begin{isamarkuptext}% \noindent The reason becomes clear when looking (probably after a failed proof @@ -106,14 +106,13 @@ well now. It turns out that instead of induction, case distinction suffices:% \end{isamarkuptxt}% -\isacommand{apply}(case\_tac[!]\ bs)\isanewline -\isacommand{by}(auto)% +\isacommand{by}(case\_tac[!]\ bs,\ auto)% \begin{isamarkuptext}% \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]} in our case. Individual -subgoal numbers are also allowed. +All methods ending in \isa{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]} in our case. Individual subgoal numbers, +e.g. \isa{[2]} are also allowed. This proof may look surprisingly straightforward. However, note that this comes at a cost: the proof script is unreadable because the diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/appendix.tex --- a/doc-src/TutorialI/appendix.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/appendix.tex Sun Aug 06 15:26:53 2000 +0200 @@ -118,179 +118,33 @@ \end{figure} -\begin{figure}[htbp] - -%FIXME too long to be useful!?? -\begin{center} -\begin{tabular}{|lll|} -\hline -\texttt{ML} & -\texttt{ML_command} & -\texttt{ML_setup} \\ -\texttt{also} & -\texttt{apply} & -\texttt{apply_end} \\ -\texttt{arities} & -\texttt{assume} & -\texttt{axclass} \\ -\texttt{axioms} & -\texttt{back} & -\texttt{by} \\ -\texttt{cannot_undo} & -\texttt{case} & -\texttt{cd} \\ -\texttt{chapter} & -\texttt{classes} & -\texttt{classrel} \\ -\texttt{clear_undos} & -\texttt{coinductive} & -\texttt{commit} \\ -\texttt{constdefs} & -\texttt{consts} & -\texttt{context} \\ -\texttt{datatype} & -\texttt{def} & -\texttt{defaultsort} \\ -\texttt{defer} & -\texttt{defer_recdef} & -\texttt{defs} \\ -\texttt{disable_pr} & -\texttt{enable_pr} & -\texttt{end} \\ -\texttt{exit} & -\texttt{finally} & -\texttt{fix} \\ -\texttt{from} & -\texttt{global} & -\texttt{have} \\ -\texttt{header} & -\texttt{help} & -\texttt{hence} \\ -\texttt{hide} & -\texttt{inductive} & -\texttt{inductive_cases} \\ -\texttt{init_toplevel} & -\texttt{instance} & -\texttt{judgment} \\ -\texttt{kill} & -\texttt{kill_thy} & -\texttt{lemma} \\ -\texttt{lemmas} & -\texttt{let} & -\texttt{local} \\ -\texttt{moreover} & -\texttt{next} & -\texttt{nonterminals} \\ -\texttt{note} & -\texttt{obtain} & -\texttt{oops} \\ -\texttt{oracle} & -\texttt{parse_ast_translation} & -\texttt{parse_translation} \\ -\texttt{pr} & -\texttt{prefer} & -\texttt{presume} \\ -\texttt{pretty_setmargin} & -\texttt{primrec} & -\texttt{print_ast_translation} \\ -\texttt{print_attributes} & -\texttt{print_binds} & -\texttt{print_cases} \\ -\texttt{print_claset} & -\texttt{print_context} & -\texttt{print_facts} \\ -\texttt{print_methods} & -\texttt{print_simpset} & -\texttt{print_syntax} \\ -\texttt{print_theorems} & -\texttt{print_theory} & -\texttt{print_translation} \\ -\texttt{proof} & -\texttt{prop} & -\texttt{pwd} \\ -\texttt{qed} & -\texttt{quit} & -\texttt{recdef} \\ -\texttt{record} & -\texttt{redo} & -\texttt{remove_thy} \\ -\texttt{rep_datatype} & -\texttt{sect} & -\texttt{section} \\ -\texttt{setup} & -\texttt{show} & -\texttt{sorry} \\ -\texttt{subsect} & -\texttt{subsection} & -\texttt{subsubsect} \\ -\texttt{subsubsection} & -\texttt{syntax} & -\texttt{term} \\ -\texttt{text} & -\texttt{text_raw} & -\texttt{then} \\ -\texttt{theorem} & -\texttt{theorems} & -\texttt{theory} \\ -\texttt{thm} & -\texttt{thms_containing} & -\texttt{thus} \\ -\texttt{token_translation} & -\texttt{touch_all_thys} & -\texttt{touch_child_thys} \\ -\texttt{touch_thy} & -\texttt{translations} & -\texttt{txt} \\ -\texttt{txt_raw} & -\texttt{typ} & -\texttt{typed_print_translation} \\ -\texttt{typedecl} & -\texttt{typedef} & -\texttt{types} \\ -\texttt{ultimately} & -\texttt{undo} & -\texttt{undos_proof} \\ -\texttt{update_thy} & -\texttt{update_thy_only} & -\texttt{use} \\ -\texttt{use_thy} & -\texttt{use_thy_only} & -\texttt{welcome} \\ -\texttt{with} & - & - \\ -\hline -\end{tabular} -\end{center} - -\begin{center} -\begin{tabular}{|lllll|} -\hline -\texttt{and} & -\texttt{binder} & -\texttt{con_defs} & -\texttt{concl} & -\texttt{congs} \\ -\texttt{distinct} & -\texttt{files} & -\texttt{in} & -\texttt{induction} & -\texttt{infixl} \\ -\texttt{infixr} & -\texttt{inject} & -\texttt{intrs} & -\texttt{is} & -\texttt{monos} \\ -\texttt{output} & -\texttt{where} & - & - & - \\ -\hline -\end{tabular} -\end{center} - - -\caption{Commands and minor keywords in HOL theories} -\label{fig:keywords} -\end{figure} +%\begin{figure}[htbp] +%\begin{center} +%\begin{tabular}{|lllll|} +%\hline +%\texttt{and} & +%\texttt{binder} & +%\texttt{con_defs} & +%\texttt{concl} & +%\texttt{congs} \\ +%\texttt{distinct} & +%\texttt{files} & +%\texttt{in} & +%\texttt{induction} & +%\texttt{infixl} \\ +%\texttt{infixr} & +%\texttt{inject} & +%\texttt{intrs} & +%\texttt{is} & +%\texttt{monos} \\ +%\texttt{output} & +%\texttt{where} & +% & +% & +% \\ +%\hline +%\end{tabular} +%\end{center} +%\caption{Minor keywords in HOL theories} +%\label{fig:keywords} +%\end{figure} diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/basics.tex --- a/doc-src/TutorialI/basics.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/basics.tex Sun Aug 06 15:26:53 2000 +0200 @@ -65,7 +65,11 @@ \begin{center}\small \url{http://isabelle.in.tum.de/library/} \end{center} -and is recommended browsing. +and is recommended browsing. Note that most of the theories in the library +are based on classical Isabelle without the Isar extension. This means that +they look slightly different than the theories in this tutorial, and that all +proofs are in separate ML files. + \begin{warn} HOL contains a theory \ttindexbold{Main}, the union of all the basic predefined theories like arithmetic, lists, sets, etc.\ (see the online @@ -275,13 +279,11 @@ mathematical symbols. For those that do not, remember that ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix. -Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces, -for example Proof General, require each command to be terminated by a -semicolon, whereas others, for example the shell level, do not. But even at -the shell level it is advisable to use semicolons to enforce that a command +Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} +Commands may but need not be terminated by semicolons. +At the shell level it is advisable to use semicolons to enforce that a command is executed immediately; otherwise Isabelle may wait for the next keyword -before it knows that the command is complete. Note that for readibility -reasons we often drop the final semicolon in the text. +before it knows that the command is complete. \section{Getting started} @@ -296,3 +298,4 @@ type each command into the file first and then enter it into Isabelle by copy-and-paste, thus ensuring that you have a complete record of your theory. As mentioned above, Proof General offers a much superior interface. +If you have installed Proof General, you can start it with \texttt{Isabelle}. diff -r 02c51ca9c531 -r d17c0b34d5c8 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Fri Aug 04 23:02:11 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Sun Aug 06 15:26:53 2000 +0200 @@ -5,12 +5,12 @@ constructs and proof procedures introduced are general purpose and recur in any specification or verification task. -The dedicated functional programmer should be warned: HOL offers only {\em - total functional programming} --- all functions in HOL must be total; lazy -data structures are not directly available. On the positive side, functions -in HOL need not be computable: HOL is a specification language that goes well -beyond what can be expressed as a program. However, for the time being we -concentrate on the computable. +The dedicated functional programmer should be warned: HOL offers only +\emph{total functional programming} --- all functions in HOL must be total; +lazy data structures are not directly available. On the positive side, +functions in HOL need not be computable: HOL is a specification language that +goes well beyond what can be expressed as a program. However, for the time +being we concentrate on the computable. \section{An introductory theory} \label{sec:intro-theory} @@ -119,10 +119,7 @@ named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle automatically loads all the required parent theories from their respective files (which may take a moment, unless the theories are already loaded and - the files have not been modified). The only time when you need to load a - theory by hand is when you simply want to check if it loads successfully - without wanting to make use of the theory itself. This you can do by typing - \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. + the files have not been modified). If you suddenly discover that you need to modify a parent theory of your current theory you must first abandon your current theory\indexbold{abandon @@ -131,6 +128,11 @@ been modified you go back to your original theory. When its first line \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:} is processed, the modified parent is reloaded automatically. + + The only time when you need to load a theory by hand is when you simply + want to check if it loads successfully without wanting to make use of the + theory itself. This you can do by typing + \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}. \end{description} Further commands are found in the Isabelle/Isar Reference Manual. @@ -372,23 +374,7 @@ \subsection{Products} - -HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ * - $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair -are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and -\isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right: -\isa{($a@1$,$a@2$,$a@3$)} stands for \isa{($a@1$,($a@2$,$a@3$))} and -\isa{$\tau@1$ * $\tau@2$ * $\tau@3$} for \isa{$\tau@1$ * ($\tau@2$ * - $\tau@3$)}. Therefore we have \isa{fst(snd($a@1$,$a@2$,$a@3$)) = $a@2$}. - -It is possible to use (nested) tuples as patterns in abstractions, for -example \isa{\isasymlambda(x,y,z).x+y+z} and -\isa{\isasymlambda((x,y),z).x+y+z}. -In addition to explicit $\lambda$-abstractions, tuple patterns can be used in -most variable binding constructs. Typical examples are - -\input{Misc/document/pairs.tex}% -Further important examples are quantifiers and sets (see~\S\ref{quant-pats}). +\input{Misc/document/pairs.tex} %FIXME move stuff below into section on proofs about products? \begin{warn} @@ -401,10 +387,13 @@ theorem proving with tuple patterns. \end{warn} -Finally note that products, like natural numbers, are datatypes, which means +Note that products, like natural numbers, are datatypes, which means in particular that \isa{induct_tac} and \isa{case_tac} are applicable to products (see \S\ref{proofs-about-products}). +Instead of tuples with many components (where ``many'' is not much above 2), +it is far preferable to use record types (see \S\ref{sec:records}). + \section{Definitions} \label{sec:Definitions} @@ -455,11 +444,11 @@ \label{sec:Simplification} \index{simplification|(} -So far we have proved our theorems by \isa{auto}, which ``simplifies'' all -subgoals. In fact, \isa{auto} can do much more than that, except that it -did not need to so far. However, when you go beyond toy examples, you need to -understand the ingredients of \isa{auto}. This section covers the method -that \isa{auto} always applies first, namely simplification. +So far we have proved our theorems by \isa{auto}, which ``simplifies'' +\emph{all} subgoals. In fact, \isa{auto} can do much more than that, except +that it did not need to so far. However, when you go beyond toy examples, you +need to understand the ingredients of \isa{auto}. This section covers the +method that \isa{auto} always applies first, namely simplification. Simplification is one of the central theorem proving tools in Isabelle and many other systems. The tool itself is called the \bfindex{simplifier}. The @@ -505,8 +494,8 @@ The simplification attribute of theorems can be turned on and off as follows: \begin{ttbox} -theorems [simp] = \(list of theorem names\); -theorems [simp del] = \(list of theorem names\); +lemmas [simp] = \(list of theorem names\); +lemmas [simp del] = \(list of theorem names\); \end{ttbox} As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) = xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification