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

author | nipkow |

Tue, 25 Apr 2000 08:09:10 +0200 | |

changeset 8771 | 026f37a86ea7 |

parent 8770 | bfab4d4b7516 |

child 8772 | ebb07113c4f7 |

*** empty log message ***

--- a/doc-src/TutorialI/CodeGen/CodeGen.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Tue Apr 25 08:09:10 2000 +0200 @@ -18,18 +18,18 @@ | Bex "'v binop" "('a,'v)expr" "('a,'v)expr"; text{*\noindent -The three constructors represent constants, variables and the combination of -two subexpressions with a binary operation. +The three constructors represent constants, variables and the application of +a binary operation to two subexpressions. The value of an expression w.r.t.\ an environment that maps variables to values is easily defined: *} -consts value :: "('a \\<Rightarrow> 'v) \\<Rightarrow> ('a,'v)expr \\<Rightarrow> 'v"; +consts value :: "('a,'v)expr \\<Rightarrow> ('a \\<Rightarrow> 'v) \\<Rightarrow> 'v"; primrec -"value env (Cex v) = v" -"value env (Vex a) = env a" -"value env (Bex f e1 e2) = f (value env e1) (value env e2)"; +"value (Cex v) env = v" +"value (Vex a) env = env a" +"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)"; text{* The stack machine has three instructions: load a constant value onto the @@ -43,20 +43,21 @@ | Apply "'v binop"; text{* -The execution of the stack machine is modelled by a function \isa{exec} -that takes a store (modelled as a function from addresses to values, just -like the environment for evaluating expressions), a stack (modelled as a -list) of values, and a list of instructions, and returns the stack at the end -of the execution---the store remains unchanged: +The execution of the stack machine is modelled by a function +\isa{exec} that takes a list of instructions, a store (modelled as a +function from addresses to values, just like the environment for +evaluating expressions), and a stack (modelled as a list) of values, +and returns the stack at the end of the execution---the store remains +unchanged: *} -consts exec :: "('a\\<Rightarrow>'v) \\<Rightarrow> 'v list \\<Rightarrow> ('a,'v)instr list \\<Rightarrow> 'v list"; +consts exec :: "('a,'v)instr list \\<Rightarrow> ('a\\<Rightarrow>'v) \\<Rightarrow> 'v list \\<Rightarrow> 'v list"; primrec -"exec s vs [] = vs" -"exec s vs (i#is) = (case i of - Const v \\<Rightarrow> exec s (v#vs) is - | Load a \\<Rightarrow> exec s ((s a)#vs) is - | Apply f \\<Rightarrow> exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)"; +"exec [] s vs = vs" +"exec (i#is) s vs = (case i of + Const v \\<Rightarrow> exec is s (v#vs) + | Load a \\<Rightarrow> exec is s ((s a)#vs) + | Apply f \\<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))"; text{*\noindent Recall that \isa{hd} and \isa{tl} @@ -81,13 +82,13 @@ 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: *} -theorem "exec s [] (comp e) = [value s e]"; +theorem "exec (comp e) s [] = [value e s]"; (*<*)oops;(*>*) text{*\noindent This theorem needs to be generalized to *} -theorem "\\<forall>vs. exec s vs (comp e) = (value s e) # vs"; +theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs"; txt{*\noindent which is proved by induction on \isa{e} followed by simplification, once @@ -96,7 +97,7 @@ *} (*<*)oops;(*>*) lemma exec_app[simp]: - "\\<forall>vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys"; + "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; txt{*\noindent This requires induction on \isa{xs} and ordinary simplification for the @@ -113,20 +114,20 @@ *} (*<*) lemmas [simp del] = exec_app; -lemma [simp]: "\\<forall>vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys"; +lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; (*>*) apply(induct_tac xs, auto split: instr.split).; text{*\noindent Although this is more compact, it is less clear for the reader of the proof. -We could now go back and prove \isa{exec s [] (comp e) = [value s e]} +We could now go back and prove \isa{exec (comp e) s [] = [value e s]} merely by simplification with the generalized version we just proved. However, this is unnecessary because the generalized version fully subsumes its instance. *} (*<*) -theorem "\\<forall>vs. exec s vs (comp e) = (value s e) # vs"; +theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs"; apply(induct_tac e, auto).; end (*>*)

--- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Tue Apr 25 08:09:10 2000 +0200 @@ -16,17 +16,17 @@ ~~~~~~~~~~~~~~~~~~~~~|~Bex~{"}'v~binop{"}~~{"}('a,'v)expr{"}~~{"}('a,'v)expr{"}% \begin{isamarkuptext}% \noindent -The three constructors represent constants, variables and the combination of -two subexpressions with a binary operation. +The three constructors represent constants, variables and the application of +a binary operation to two subexpressions. The value of an expression w.r.t.\ an environment that maps variables to values is easily defined:% \end{isamarkuptext}% -\isacommand{consts}~value~::~{"}('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~('a,'v)expr~{\isasymRightarrow}~'v{"}\isanewline +\isacommand{consts}~value~::~{"}('a,'v)expr~{\isasymRightarrow}~('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~'v{"}\isanewline \isacommand{primrec}\isanewline -{"}value~env~(Cex~v)~=~v{"}\isanewline -{"}value~env~(Vex~a)~=~env~a{"}\isanewline -{"}value~env~(Bex~f~e1~e2)~=~f~(value~env~e1)~(value~env~e2){"}% +{"}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 @@ -37,19 +37,20 @@ ~~~~~~~~~~~~~~~~~~~~~~~|~Load~'a\isanewline ~~~~~~~~~~~~~~~~~~~~~~~|~Apply~{"}'v~binop{"}% \begin{isamarkuptext}% -The execution of the stack machine is modelled by a function \isa{exec} -that takes a store (modelled as a function from addresses to values, just -like the environment for evaluating expressions), a stack (modelled as a -list) of values, and a list of instructions, and returns the stack at the end -of the execution---the store remains unchanged:% +The execution of the stack machine is modelled by a function +\isa{exec} that takes a list of instructions, a store (modelled as a +function from addresses to values, just like the environment for +evaluating expressions), and a stack (modelled as a list) of values, +and returns the stack at the end of the execution---the store remains +unchanged:% \end{isamarkuptext}% -\isacommand{consts}~exec~::~{"}('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~('a,'v)instr~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~s~vs~(i\#is)~=~(case~i~of\isanewline -~~~~Const~v~~{\isasymRightarrow}~exec~s~(v\#vs)~is\isanewline -~~|~Load~a~~~{\isasymRightarrow}~exec~s~((s~a)\#vs)~is\isanewline -~~|~Apply~f~~{\isasymRightarrow}~exec~s~(~(f~(hd~vs)~(hd(tl~vs)))\#(tl(tl~vs))~)~is){"}% +{"}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} @@ -72,12 +73,12 @@ 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~s~[]~(comp~e)~=~[value~s~e]{"}% +\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~s~vs~(comp~e)~=~(value~s~e)~\#~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 @@ -85,7 +86,7 @@ instruction sequences:% \end{isamarkuptxt}% \isacommand{lemma}~exec\_app[simp]:\isanewline -~~{"}{\isasymforall}vs.~exec~s~vs~(xs@ys)~=~exec~s~(exec~s~vs~xs)~ys{"}% +~~{"}{\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 @@ -105,7 +106,7 @@ \noindent Although this is more compact, it is less clear for the reader of the proof. -We could now go back and prove \isa{exec s [] (comp e) = [value s e]} +We could now go back and prove \isa{exec (comp e) s [] = [value e s]} merely by simplification with the generalized version we just proved. However, this is unnecessary because the generalized version fully subsumes its instance.%

--- a/doc-src/TutorialI/Datatype/ABexpr.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy Tue Apr 25 08:09:10 2000 +0200 @@ -33,28 +33,28 @@ The semantics is fixed via two evaluation functions *} -consts evala :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a aexp \\<Rightarrow> nat" - evalb :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a bexp \\<Rightarrow> bool"; +consts evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat" + evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool"; text{*\noindent -that take an environment (a mapping from variables \isa{'a} to values -\isa{nat}) and an expression and return its arithmetic/boolean +that take an expression and an environment (a mapping from variables \isa{'a} to values +\isa{nat}) and return its arithmetic/boolean value. Since the datatypes are mutually recursive, so are functions that operate on them. Hence they need to be defined in a single \isacommand{primrec} section: *} primrec - "evala env (IF b a1 a2) = - (if evalb env b then evala env a1 else evala env a2)" - "evala env (Sum a1 a2) = evala env a1 + evala env a2" - "evala env (Diff a1 a2) = evala env a1 - evala env a2" - "evala env (Var v) = env v" - "evala env (Num n) = n" + "evala (IF b a1 a2) env = + (if evalb b env then evala a1 env else evala a2 env)" + "evala (Sum a1 a2) env = evala a1 env + evala a2 env" + "evala (Diff a1 a2) env = evala a1 env - evala a2 env" + "evala (Var v) env = env v" + "evala (Num n) env = n" - "evalb env (Less a1 a2) = (evala env a1 < evala env a2)" - "evalb env (And b1 b2) = (evalb env b1 \\<and> evalb env b2)" - "evalb env (Neg b) = (\\<not> evalb env b)" + "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)" + "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)" + "evalb (Neg b) env = (\\<not> evalb b env)" text{*\noindent In the same fashion we also define two functions that perform substitution: @@ -93,8 +93,8 @@ theorems simultaneously: *} -lemma "evala env (substa s a) = evala (\\<lambda>x. evala env (s x)) a \\<and> - evalb env (substb s b) = evalb (\\<lambda>x. evala env (s x)) b"; +lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and> + evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)"; apply(induct_tac a and b); txt{*\noindent

--- a/doc-src/TutorialI/Datatype/Fundata.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Tue Apr 25 08:09:10 2000 +0200 @@ -14,7 +14,7 @@ term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))"; text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose -root is labeled with 0 and whose $n$th subtree is labeled with $n$ and +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}: @@ -35,7 +35,7 @@ The following lemma has a canonical proof *} -lemma "map_bt g (map_bt f T) = map_bt (g o f) T"; +lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; apply(induct_tac "T", auto). text{*\noindent

--- a/doc-src/TutorialI/Datatype/document/ABexpr.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex Tue Apr 25 08:09:10 2000 +0200 @@ -29,27 +29,27 @@ expressions can be arithmetic comparisons, conjunctions and negations. The semantics is fixed via two evaluation functions% \end{isamarkuptext}% -\isacommand{consts}~~evala~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~nat{"}\isanewline -~~~~~~~~evalb~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~bexp~{\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 environment (a mapping from variables \isa{'a} to values -\isa{nat}) and an expression and return its arithmetic/boolean +that take an expression and an environment (a mapping from variables \isa{'a} to values +\isa{nat}) and return its arithmetic/boolean value. Since the datatypes are mutually recursive, so are functions that operate on them. Hence they need to be defined in a single \isacommand{primrec} section:% \end{isamarkuptext}% \isacommand{primrec}\isanewline -~~{"}evala~env~(IF~b~a1~a2)~=\isanewline -~~~~~(if~evalb~env~b~then~evala~env~a1~else~evala~env~a2){"}\isanewline -~~{"}evala~env~(Sum~a1~a2)~=~evala~env~a1~+~evala~env~a2{"}\isanewline -~~{"}evala~env~(Diff~a1~a2)~=~evala~env~a1~-~evala~env~a2{"}\isanewline -~~{"}evala~env~(Var~v)~=~env~v{"}\isanewline -~~{"}evala~env~(Num~n)~=~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~env~(Less~a1~a2)~=~(evala~env~a1~<~evala~env~a2){"}\isanewline -~~{"}evalb~env~(And~b1~b2)~=~(evalb~env~b1~{\isasymand}~evalb~env~b2){"}\isanewline -~~{"}evalb~env~(Neg~b)~=~({\isasymnot}~evalb~env~b){"}% +~~{"}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:% @@ -84,8 +84,8 @@ theorem in the induction step. Therefore you need to state and prove both theorems simultaneously:% \end{isamarkuptext}% -\isacommand{lemma}~{"}evala~env~(substa~s~a)~=~evala~({\isasymlambda}x.~evala~env~(s~x))~a~{\isasymand}\isanewline -~~~~~~~~evalb~env~(substb~s~b)~=~evalb~({\isasymlambda}x.~evala~env~(s~x))~b{"}\isanewline +\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

--- a/doc-src/TutorialI/Datatype/document/Fundata.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Tue Apr 25 08:09:10 2000 +0200 @@ -12,7 +12,7 @@ \isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}% \begin{isamarkuptext}% \noindent of type \isa{(nat,nat)bigtree} is the tree whose -root is labeled with 0 and whose $n$th subtree is labeled with $n$ and +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}:% @@ -32,7 +32,7 @@ The following lemma has a canonical proof% \end{isamarkuptext}% -\isacommand{lemma}~{"}map\_bt~g~(map\_bt~f~T)~=~map\_bt~(g~o~f)~T{"}\isanewline +\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

--- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Tue Apr 25 08:09:10 2000 +0200 @@ -61,7 +61,7 @@ \subsubsection{Transformation into and of If-expressions} The type \isa{boolex} is close to the customary representation of logical -formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to +formulae, whereas \isa{ifex} is designed for efficiency. It is easy to translate from \isa{boolex} into \isa{ifex}: *} @@ -153,7 +153,8 @@ normality of \isa{normif}: *} -lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*) +lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)"; +(*<*) apply(induct_tac b); apply(auto).; @@ -161,4 +162,5 @@ apply(induct_tac b); apply(auto).; -end(*>*) +end +(*>*)

--- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Tue Apr 25 08:09:10 2000 +0200 @@ -54,7 +54,7 @@ \subsubsection{Transformation into and of If-expressions} The type \isa{boolex} is close to the customary representation of logical -formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to +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

--- a/doc-src/TutorialI/Misc/case_splits.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/case_splits.thy Tue Apr 25 08:09:10 2000 +0200 @@ -48,15 +48,16 @@ In contrast to \isa{if}-expressions, the simplifier does not split \isa{case}-expressions by default because this can lead to nontermination in case of recursive datatypes. Again, if the \isa{only:} modifier is -dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)} -alone will not do: +dropped, the above goal is solved, *} (*<*) lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs"; (*>*) apply(simp split: list.split).; -text{* +text{*\noindent% +which \isacommand{apply}\isa{(simp)} alone will not do. + In general, every datatype $t$ comes with a theorem \isa{$t$.split} which can be declared to be a \bfindex{split rule} either locally as above, or by giving it the \isa{split} attribute globally:

--- a/doc-src/TutorialI/Misc/cases.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/cases.thy Tue Apr 25 08:09:10 2000 +0200 @@ -5,11 +5,13 @@ lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs"; apply(case_tac xs); -txt{* +txt{*\noindent +results in the proof state \begin{isabellepar}% ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs% \end{isabellepar}% +which is solved automatically: *} apply(auto).;

--- a/doc-src/TutorialI/Misc/cond_rewr.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/cond_rewr.thy Tue Apr 25 08:09:10 2000 +0200 @@ -23,7 +23,7 @@ apply(simp). (*>*) text{*\noindent -is proved by simplification: +is proved by plain simplification: the conditional equation \isa{hd_Cons_tl} above can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs} because the corresponding precondition \isa{rev xs \isasymnoteq\ []}

--- a/doc-src/TutorialI/Misc/document/case_splits.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex Tue Apr 25 08:09:10 2000 +0200 @@ -41,11 +41,13 @@ In contrast to \isa{if}-expressions, the simplifier does not split \isa{case}-expressions by default because this can lead to nontermination in case of recursive datatypes. Again, if the \isa{only:} modifier is -dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)} -alone will not do:% +dropped, the above goal is solved,% \end{isamarkuptext}% \isacommand{apply}(simp~split:~list.split)\isacommand{.}% \begin{isamarkuptext}% +\noindent% +which \isacommand{apply}\isa{(simp)} alone will not do. + In general, every datatype $t$ comes with a theorem \isa{$t$.split} which can be declared to be a \bfindex{split rule} either locally as above, or by giving it the \isa{split} attribute globally:%

--- a/doc-src/TutorialI/Misc/document/cases.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cases.tex Tue Apr 25 08:09:10 2000 +0200 @@ -3,10 +3,13 @@ \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 \begin{isabellepar}% ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs% -\end{isabellepar}%% +\end{isabellepar}% +which is solved automatically:% \end{isamarkuptxt}% \isacommand{apply}(auto)\isacommand{.}\isanewline \end{isabelle}%

--- a/doc-src/TutorialI/Misc/document/cond_rewr.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex Tue Apr 25 08:09:10 2000 +0200 @@ -19,7 +19,7 @@ \isacommand{lemma}~{"}xs~{\isasymnoteq}~[]~{\isasymLongrightarrow}~hd(rev~xs)~\#~tl(rev~xs)~=~rev~xs{"}% \begin{isamarkuptext}% \noindent -is proved by simplification: +is proved by plain simplification: the conditional equation \isa{hd_Cons_tl} above can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs} because the corresponding precondition \isa{rev xs \isasymnoteq\ []}

--- a/doc-src/TutorialI/Misc/document/let_rewr.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/let_rewr.tex Tue Apr 25 08:09:10 2000 +0200 @@ -3,6 +3,6 @@ \isacommand{apply}(simp~add:~Let\_def)\isacommand{.}% \begin{isamarkuptext}% If, in a particular context, there is no danger of a combinatorial explosion -of nested \texttt{let}s one could even add \texttt{Let_def} permanently:% +of nested \isa{let}s one could even add \isa{Let_def} permanently:% \end{isamarkuptext}% \isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%

--- a/doc-src/TutorialI/Misc/document/trace_simp.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/trace_simp.tex Tue Apr 25 08:09:10 2000 +0200 @@ -31,7 +31,7 @@ [x] = [] == False \end{ttbox} -In more complicated cases, the trace can quite lenghty, especially since +In more complicated cases, the trace can be quite lenghty, especially since invocations of the simplifier are often nested (e.g.\ when solving conditions of rewrite rules). Thus it is advisable to reset it:% \end{isamarkuptxt}%

--- a/doc-src/TutorialI/Misc/document/types.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/document/types.tex Tue Apr 25 08:09:10 2000 +0200 @@ -6,7 +6,7 @@ \noindent\indexbold{*types}% Internally all synonyms are fully expanded. As a consequence Isabelle's output never contains synonyms. Their main purpose is to improve the -readability of theory definitions. Synonyms can be used just like any other +readability of theories. Synonyms can be used just like any other type:% \end{isamarkuptext}% \isacommand{consts}~nand~::~gate\isanewline @@ -24,7 +24,7 @@ \begin{isamarkuptext}% \noindent% where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and -\isa{exor_def} are arbitrary user-supplied names. +\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. Declarations and definitions can also be merged%

--- a/doc-src/TutorialI/Misc/let_rewr.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/let_rewr.thy Tue Apr 25 08:09:10 2000 +0200 @@ -6,7 +6,7 @@ text{* If, in a particular context, there is no danger of a combinatorial explosion -of nested \texttt{let}s one could even add \texttt{Let_def} permanently: +of nested \isa{let}s one could even add \isa{Let_def} permanently: *} theorems [simp] = Let_def; (*<*)

--- a/doc-src/TutorialI/Misc/trace_simp.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/trace_simp.thy Tue Apr 25 08:09:10 2000 +0200 @@ -33,7 +33,7 @@ [x] = [] == False \end{ttbox} -In more complicated cases, the trace can quite lenghty, especially since +In more complicated cases, the trace can be quite lenghty, especially since invocations of the simplifier are often nested (e.g.\ when solving conditions of rewrite rules). Thus it is advisable to reset it: *}

--- a/doc-src/TutorialI/Misc/types.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Misc/types.thy Tue Apr 25 08:09:10 2000 +0200 @@ -7,7 +7,7 @@ text{*\noindent\indexbold{*types}% Internally all synonyms are fully expanded. As a consequence Isabelle's output never contains synonyms. Their main purpose is to improve the -readability of theory definitions. Synonyms can be used just like any other +readability of theories. Synonyms can be used just like any other type: *} @@ -28,7 +28,7 @@ text{*\noindent% where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and -\isa{exor_def} are arbitrary user-supplied names. +\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. Declarations and definitions can also be merged

--- a/doc-src/TutorialI/Recdef/Induction.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/Induction.thy Tue Apr 25 08:09:10 2000 +0200 @@ -15,7 +15,7 @@ \textbf{recursion induction}. Roughly speaking, it requires you to prove for each \isacommand{recdef} equation that the property you are trying to establish holds for the left-hand side provided it holds -for all recursive calls on the right-hand side. Here is a simple example: +for all recursive calls on the right-hand side. Here is a simple example *} lemma "map f (sep(x,xs)) = sep(f x, map f xs)";

--- a/doc-src/TutorialI/Recdef/document/Induction.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Tue Apr 25 08:09:10 2000 +0200 @@ -13,7 +13,7 @@ \textbf{recursion induction}. Roughly speaking, it requires you to prove for each \isacommand{recdef} equation that the property you are trying to establish holds for the left-hand side provided it holds -for all recursive calls on the right-hand side. Here is a simple example:% +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){"}% \begin{isamarkuptxt}%

--- a/doc-src/TutorialI/Recdef/document/examples.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/examples.tex Tue Apr 25 08:09:10 2000 +0200 @@ -11,7 +11,7 @@ \begin{isamarkuptext}% \noindent The definition of \isa{fib} is accompanied by a \bfindex{measure function} -\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a +\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 @@ -74,7 +74,7 @@ ~~{"}swap12~zs~~~~~~~=~zs{"}% \begin{isamarkuptext}% \noindent -In the non-recursive case the termination measure degenerates to the empty +For non-recursive functions the termination measure degenerates to the empty set \isa{\{\}}.% \end{isamarkuptext}% \end{isabelle}%

--- a/doc-src/TutorialI/Recdef/document/simplification.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Tue Apr 25 08:09:10 2000 +0200 @@ -42,10 +42,10 @@ \begin{isamarkuptext}% \noindent Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by -an \isa{if}, this leads to an infinite chain of simplification steps. +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. -Of course the most radical solution is to disable the offending +The most radical solution is to disable the offending \isa{split_if} as shown in the section on case splits in \S\ref{sec:SimpFeatures}. However, we do not recommend this because it means you will often have to

--- a/doc-src/TutorialI/Recdef/document/termination.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Tue Apr 25 08:09:10 2000 +0200 @@ -4,8 +4,8 @@ When a function is defined via \isacommand{recdef}, Isabelle tries to prove its termination with the help of the user-supplied measure. All of the above examples are simple enough that Isabelle can prove automatically that the -measure of the argument goes down in each recursive call. In that case -$f$.\isa{simps} contains the defining equations (or variants derived from +measure of the argument goes down in each recursive call. As a result, +\isa{$f$.simps} will contain the defining equations (or variants derived from them) as theorems. For example, look (via \isacommand{thm}) at \isa{sep.simps} and \isa{sep1.simps} to see that they define the same function. What is more, those equations are automatically declared as @@ -34,8 +34,8 @@ \isacommand{apply}(arith)\isacommand{.}% \begin{isamarkuptext}% \noindent -Because \isacommand{recdef}'s the termination prover involves simplification, -we have declared our lemma a simplification rule. Therefore our second +Because \isacommand{recdef}'s termination prover involves simplification, +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

--- a/doc-src/TutorialI/Recdef/examples.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/examples.thy Tue Apr 25 08:09:10 2000 +0200 @@ -14,7 +14,7 @@ text{*\noindent The definition of \isa{fib} is accompanied by a \bfindex{measure function} -\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a +\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 @@ -83,7 +83,7 @@ "swap12 zs = zs"; text{*\noindent -In the non-recursive case the termination measure degenerates to the empty +For non-recursive functions the termination measure degenerates to the empty set \isa{\{\}}. *}

--- a/doc-src/TutorialI/Recdef/simplification.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/simplification.thy Tue Apr 25 08:09:10 2000 +0200 @@ -49,10 +49,10 @@ text{*\noindent Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by -an \isa{if}, this leads to an infinite chain of simplification steps. +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. -Of course the most radical solution is to disable the offending +The most radical solution is to disable the offending \isa{split_if} as shown in the section on case splits in \S\ref{sec:SimpFeatures}. However, we do not recommend this because it means you will often have to

--- a/doc-src/TutorialI/Recdef/termination.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Recdef/termination.thy Tue Apr 25 08:09:10 2000 +0200 @@ -6,8 +6,8 @@ When a function is defined via \isacommand{recdef}, Isabelle tries to prove its termination with the help of the user-supplied measure. All of the above examples are simple enough that Isabelle can prove automatically that the -measure of the argument goes down in each recursive call. In that case -$f$.\isa{simps} contains the defining equations (or variants derived from +measure of the argument goes down in each recursive call. As a result, +\isa{$f$.simps} will contain the defining equations (or variants derived from them) as theorems. For example, look (via \isacommand{thm}) at \isa{sep.simps} and \isa{sep1.simps} to see that they define the same function. What is more, those equations are automatically declared as @@ -39,8 +39,8 @@ apply(arith).; text{*\noindent -Because \isacommand{recdef}'s the termination prover involves simplification, -we have declared our lemma a simplification rule. Therefore our second +Because \isacommand{recdef}'s termination prover involves simplification, +we have turned our lemma into a simplification rule. Therefore our second attempt to define our function will automatically take it into account: *}

--- a/doc-src/TutorialI/ToyList/ToyList.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Tue Apr 25 08:09:10 2000 +0200 @@ -1,10 +1,10 @@ theory ToyList = PreList: text{*\noindent -HOL already has a predefined theory of lists called \texttt{List} --- -\texttt{ToyList} is merely a small fragment of it chosen as an example. In +HOL already has a predefined theory of lists called \isa{List} --- +\isa{ToyList} is merely a small fragment of it chosen as an example. In contrast to what is recommended in \S\ref{sec:Basic:Theories}, -\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a +\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a theory that contains pretty much everything but lists, thus avoiding ambiguities caused by defining lists twice. *} @@ -31,7 +31,7 @@ \begin{warn} Syntax annotations are a powerful but completely optional feature. You - could drop them from theory \texttt{ToyList} and go back to the identifiers + could drop them from theory \isa{ToyList} and go back to the identifiers \isa{Nil} and \isa{Cons}. However, lists are such a central datatype that their syntax is highly customized. We recommend that novices should not use syntax annotations in their own theories. @@ -67,7 +67,7 @@ \isa{app} appends two lists and \isa{rev} reverses a list. The keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is of a particularly primitive kind where each recursive call peels off a datatype -constructor from one of the arguments (see \S\ref{sec:datatype}). Thus the +constructor from one of the arguments. Thus the recursion always terminates, i.e.\ the function is \bfindex{total}. The termination requirement is absolutely essential in HOL, a logic of total @@ -103,7 +103,7 @@ text{*\noindent When Isabelle prints a syntax error message, it refers to the HOL syntax as -the \bfindex{inner syntax}. +the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}. \section{An introductory proof} @@ -122,7 +122,7 @@ theorem rev_rev [simp]: "rev(rev xs) = xs"; -txt{*\noindent\index{*theorem|bold}\index{*simp (attribute)|bold} +txt{*\index{*theorem|bold}\index{*simp (attribute)|bold} \begin{itemize} \item establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs}, @@ -220,8 +220,8 @@ text{* \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}} -After abandoning the above proof attempt (at the shell level type -\isa{oops}) we start a new proof: +After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type +\isacommand{oops}) we start a new proof: *} lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)"; @@ -232,7 +232,6 @@ \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much interchangeably. -%FIXME indent! There are two variables that we could induct on: \isa{xs} and \isa{ys}. Because \isa{\at} is defined by recursion on the first argument, \isa{xs} is the correct one: @@ -251,9 +250,9 @@ ~1.~rev~ys~=~rev~ys~@~[]\isanewline ~2. \dots \end{isabellepar}% -We need to cancel this proof attempt and prove another simple lemma first. -In the future the step of cancelling an incomplete proof before embarking on -the proof of a lemma often remains implicit. +Again, we need to abandon this proof attempt and prove another simple lemma first. +In the future the step of abandoning an incomplete proof before embarking on +the proof of a lemma usually remains implicit. *} (*<*) oops

--- a/doc-src/TutorialI/ToyList/document/ToyList.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Tue Apr 25 08:09:10 2000 +0200 @@ -2,10 +2,10 @@ \isacommand{theory}~ToyList~=~PreList:% \begin{isamarkuptext}% \noindent -HOL already has a predefined theory of lists called \texttt{List} --- -\texttt{ToyList} is merely a small fragment of it chosen as an example. In +HOL already has a predefined theory of lists called \isa{List} --- +\isa{ToyList} is merely a small fragment of it chosen as an example. In contrast to what is recommended in \S\ref{sec:Basic:Theories}, -\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a +\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a theory that contains pretty much everything but lists, thus avoiding ambiguities caused by defining lists twice.% \end{isamarkuptext}% @@ -31,7 +31,7 @@ \begin{warn} Syntax annotations are a powerful but completely optional feature. You - could drop them from theory \texttt{ToyList} and go back to the identifiers + could drop them from theory \isa{ToyList} and go back to the identifiers \isa{Nil} and \isa{Cons}. However, lists are such a central datatype that their syntax is highly customized. We recommend that novices should not use syntax annotations in their own theories. @@ -63,7 +63,7 @@ \isa{app} appends two lists and \isa{rev} reverses a list. The keyword \isacommand{primrec}\index{*primrec} indicates that the recursion is of a particularly primitive kind where each recursive call peels off a datatype -constructor from one of the arguments (see \S\ref{sec:datatype}). Thus the +constructor from one of the arguments. Thus the recursion always terminates, i.e.\ the function is \bfindex{total}. The termination requirement is absolutely essential in HOL, a logic of total @@ -98,7 +98,7 @@ \begin{isamarkuptext}% \noindent When Isabelle prints a syntax error message, it refers to the HOL syntax as -the \bfindex{inner syntax}. +the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}. \section{An introductory proof} @@ -116,7 +116,7 @@ \end{isamarkuptext}% \isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}% \begin{isamarkuptxt}% -\noindent\index{*theorem|bold}\index{*simp (attribute)|bold} +\index{*theorem|bold}\index{*simp (attribute)|bold} \begin{itemize} \item establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs}, @@ -209,8 +209,8 @@ \begin{isamarkuptext}% \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}} -After abandoning the above proof attempt (at the shell level type -\isa{oops}) we start a new proof:% +After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type +\isacommand{oops}) we start a new proof:% \end{isamarkuptext}% \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}% \begin{isamarkuptxt}% @@ -220,7 +220,6 @@ \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much interchangeably. -%FIXME indent! There are two variables that we could induct on: \isa{xs} and \isa{ys}. Because \isa{\at} is defined by recursion on the first argument, \isa{xs} is the correct one:% @@ -236,9 +235,9 @@ ~1.~rev~ys~=~rev~ys~@~[]\isanewline ~2. \dots \end{isabellepar}% -We need to cancel this proof attempt and prove another simple lemma first. -In the future the step of cancelling an incomplete proof before embarking on -the proof of a lemma often remains implicit.% +Again, we need to abandon this proof attempt and prove another simple lemma first. +In the future the step of abandoning an incomplete proof before embarking on +the proof of a lemma usually remains implicit.% \end{isamarkuptxt}% % \begin{isamarkuptext}%

--- a/doc-src/TutorialI/Trie/Option2.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Trie/Option2.thy Tue Apr 25 08:09:10 2000 +0200 @@ -2,8 +2,7 @@ theory Option2 = Main:; (*>*) -datatype 'a option = None | Some 'a - +datatype 'a option = None | Some 'a; (*<*) end (*>*)

--- a/doc-src/TutorialI/Trie/Trie.thy Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Trie/Trie.thy Tue Apr 25 08:09:10 2000 +0200 @@ -1,7 +1,6 @@ (*<*) theory Trie = Main:; (*>*) - text{* To minimize running time, each node of a trie should contain an array that maps letters to subtries. We have chosen a (sometimes) more space efficient @@ -53,7 +52,7 @@ *} lemma [simp]: "lookup (Trie None []) as = None"; -apply(cases "as", auto).; +apply(case_tac as, auto).; text{* Things begin to get interesting with the definition of an update function @@ -107,7 +106,7 @@ The start of the proof is completely conventional: *} -apply(induct_tac "as", auto); +apply(induct_tac as, auto); txt{*\noindent Unfortunately, this time we are left with three intimidating looking subgoals: @@ -127,8 +126,8 @@ text{*\noindent Both \isaindex{case_tac} and \isaindex{induct_tac} take an optional first argument that specifies the range of subgoals they are -applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual -subgoal number are also allowed. +applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual +subgoal numbers are also allowed. This proof may look surprisingly straightforward. However, note that this comes at a cost: the proof script is unreadable because the

--- a/doc-src/TutorialI/Trie/document/Option2.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Trie/document/Option2.tex Tue Apr 25 08:09:10 2000 +0200 @@ -1,4 +1,3 @@ \begin{isabelle}% \isanewline -\isacommand{datatype}~'a~option~=~None~|~Some~'a\isanewline -\end{isabelle}% +\isacommand{datatype}~'a~option~=~None~|~Some~'a\end{isabelle}%

--- a/doc-src/TutorialI/Trie/document/Trie.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Tue Apr 25 08:09:10 2000 +0200 @@ -44,7 +44,7 @@ distinguishes the two cases whether the search string is empty or not:% \end{isamarkuptext}% \isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline -\isacommand{apply}(cases~{"}as{"},~auto)\isacommand{.}% +\isacommand{apply}(case\_tac~as,~auto)\isacommand{.}% \begin{isamarkuptext}% Things begin to get interesting with the definition of an update function that adds a new (string,value) pair to a trie, overwriting the old value @@ -93,7 +93,7 @@ \isa{as} is instantiated. The start of the proof is completely conventional:% \end{isamarkuptxt}% -\isacommand{apply}(induct\_tac~{"}as{"},~auto)% +\isacommand{apply}(induct\_tac~as,~auto)% \begin{isamarkuptxt}% \noindent Unfortunately, this time we are left with three intimidating looking subgoals: @@ -112,8 +112,8 @@ \noindent Both \isaindex{case_tac} and \isaindex{induct_tac} take an optional first argument that specifies the range of subgoals they are -applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual -subgoal number are also allowed. +applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual +subgoal numbers are also allowed. This proof may look surprisingly straightforward. However, note that this comes at a cost: the proof script is unreadable because the

--- a/doc-src/TutorialI/appendix.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/appendix.tex Tue Apr 25 08:09:10 2000 +0200 @@ -80,7 +80,7 @@ \end{center} \caption{Mathematical symbols and their ASCII-equivalents} \label{fig:ascii} -\end{figure} +\end{figure}\indexbold{ASCII symbols} \begin{figure}[htbp] \begin{center}

--- a/doc-src/TutorialI/basics.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/basics.tex Tue Apr 25 08:09:10 2000 +0200 @@ -48,13 +48,13 @@ where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing theories that \texttt{T} is based on and \texttt{\textit{declarations, definitions, and proofs}} represents the newly introduced concepts -(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the +(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}. Everything defined in the parent theories (and their parents \dots) is automatically visible. To avoid name clashes, identifiers can be \textbf{qualified} by theory names as in \texttt{T.f} and \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must -reside in a \indexbold{theory file} named \texttt{T.thy}. +reside in a \bfindex{theory file} named \texttt{T.thy}. This tutorial is concerned with introducing you to the different linguistic constructs that can fill \textit{\texttt{declarations, definitions, and @@ -74,59 +74,33 @@ \end{warn} -\section{Interaction and interfaces} - -Interaction with Isabelle can either occur at the shell level or through more -advanced interfaces. To keep the tutorial independent of the interface we -have phrased the description of the intraction in a neutral language. For -example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the -shell level, which is explained the first time the phrase is used. Other -interfaces perform the same act by cursor movements and/or mouse clicks. -Although shell-based interaction is quite feasible for the kind of proof -scripts currently presented in this tutorial, the recommended interface for -Isabelle/Isar is the Emacs-based \bfindex{Proof - General}~\cite{Aspinall:TACAS:2000,proofgeneral}. - -To improve readability some of the interfaces (including the shell level) -offer special fonts with mathematical symbols. Therefore the usual -mathematical symbols are used throughout the tutorial. Their -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 -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. - - \section{Types, terms and formulae} \label{sec:TypesTermsForms} \indexbold{type} -Embedded in the declarations of a theory are the types, terms and formulae of -HOL. HOL is a typed logic whose type system resembles that of functional -programming languages like ML or Haskell. Thus there are +Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed +logic whose type system resembles that of functional programming languages +like ML or Haskell. Thus there are \begin{description} -\item[base types,] in particular \ttindex{bool}, the type of truth values, -and \ttindex{nat}, the type of natural numbers. -\item[type constructors,] in particular \texttt{list}, the type of -lists, and \texttt{set}, the type of sets. Type constructors are written -postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are +\item[base types,] in particular \isaindex{bool}, the type of truth values, +and \isaindex{nat}, the type of natural numbers. +\item[type constructors,] in particular \isaindex{list}, the type of +lists, and \isaindex{set}, the type of sets. Type constructors are written +postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are natural numbers. Parentheses around single arguments can be dropped (as in -\texttt{nat list}), multiple arguments are separated by commas (as in -\texttt{(bool,nat)foo}). +\isa{nat list}), multiple arguments are separated by commas (as in +\isa{(bool,nat)ty}). \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}. - In HOL \isasymFun\ represents {\em total} functions only. As is customary, - \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means - \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also - supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} - which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ + In HOL \isasymFun\ represents \emph{total} functions only. As is customary, + \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means + \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also + supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$} + which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ \isasymFun~$\tau$}. -\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in -ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the -type of the identity function. +\item[type variables,]\indexbold{type variable}\indexbold{variable!type} + denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise + to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity + function. \end{description} \begin{warn} Types are extremely important because they prevent us from writing @@ -145,77 +119,71 @@ \noindent This can be reversed by \texttt{ML "reset show_types"}. Various other flags -can be set and reset in the same manner.\bfindex{flag!(re)setting} +can be set and reset in the same manner.\indexbold{flag!(re)setting} \end{warn} \textbf{Terms}\indexbold{term} are formed as in functional programming by -applying functions to arguments. If \texttt{f} is a function of type -\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type -$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports -infix functions like \texttt{+} and some basic constructs from functional +applying functions to arguments. If \isa{f} is a function of type +\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type +$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports +infix functions like \isa{+} and some basic constructs from functional programming: \begin{description} -\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if} +\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if} means what you think it means and requires that -$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type. -\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let} +$b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type. +\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let} is equivalent to $u$ where all occurrences of $x$ have been replaced by $t$. For example, -\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated -by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. -\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] +\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated +by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}. +\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}] \indexbold{*case} -evaluates to $e@i$ if $e$ is of the form -$c@i$. See~\S\ref{sec:case-expressions} for details. +evaluates to $e@i$ if $e$ is of the form $c@i$. \end{description} Terms may also contain \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example, -\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument -\texttt{x} and returns \texttt{x+1}. Instead of -\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write -\texttt{\isasymlambda{}x~y~z.}~$t$. +\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and +returns \isa{x+1}. Instead of +\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write +\isa{\isasymlambda{}x~y~z.~$t$}. -\textbf{Formulae}\indexbold{formula} -are terms of type \texttt{bool}. There are the basic -constants \ttindexbold{True} and \ttindexbold{False} and the usual logical -connectives (in decreasing order of priority): -\indexboldpos{\isasymnot}{$HOL0not}, -\indexboldpos{\isasymand}{$HOL0and}, -\indexboldpos{\isasymor}{$HOL0or}, and -\indexboldpos{\isasymimp}{$HOL0imp}, +\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}. +There are the basic constants \isaindexbold{True} and \isaindexbold{False} and +the usual logical connectives (in decreasing order of priority): +\indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and}, +\indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp}, all of which (except the unary \isasymnot) associate to the right. In -particular \texttt{A \isasymimp~B \isasymimp~C} means -\texttt{A \isasymimp~(B \isasymimp~C)} and is thus -logically equivalent with \texttt{A \isasymand~B \isasymimp~C} -(which is \texttt{(A \isasymand~B) \isasymimp~C}). +particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B + \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B + \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}). Equality is available in the form of the infix function -\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a - \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$ +\isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a + \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$ and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type -\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula -$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for -\texttt{\isasymnot($t@1$ = $t@2$)}. +\isa{bool}, \isa{=} acts as if-and-only-if. The formula +\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for +\isa{\isasymnot($t@1$ = $t@2$)}. The syntax for quantifiers is -\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and -\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}. There is -even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which -means that there exists exactly one \texttt{x} that satisfies $P$. -Nested quantifications can be abbreviated: -\texttt{\isasymforall{}x~y~z.}~$P$ means -\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$. +\isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and +\isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}. There is +even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which +means that there exists exactly one \isa{x} that satisfies \isa{$P$}. Nested +quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means +\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}. Despite type inference, it is sometimes necessary to attach explicit -\bfindex{type constraints} to a term. The syntax is \texttt{$t$::$\tau$} as -in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly -and should therefore be enclosed in parentheses: \texttt{x < y::nat} is -ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason -for type constraints are overloaded functions like \texttt{+}, \texttt{*} and -\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of -overloading.) +\textbf{type constraints}\indexbold{type constraint} to a term. The syntax is +\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that +\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed +in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as +\isa{(x < y)::nat}. The main reason for type constraints are overloaded +functions like \isa{+}, \isa{*} and \isa{<}. (See \S\ref{sec:TypeClasses} for +a full discussion of overloading.) \begin{warn} In general, HOL's concrete syntax tries to follow the conventions of @@ -234,33 +202,35 @@ \begin{itemize} \item -Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}! +Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}! \item -Isabelle allows infix functions like \texttt{+}. The prefix form of function -application binds more strongly than anything else and hence \texttt{f~x + y} -means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}. +Isabelle allows infix functions like \isa{+}. The prefix form of function +application binds more strongly than anything else and hence \isa{f~x + y} +means \isa{(f~x)~+~y} and not \isa{f(x+y)}. \item Remember that in HOL if-and-only-if is expressed using equality. But equality has a high priority, as befitting a relation, while if-and-only-if - typically has the lowest priority. Thus, \texttt{\isasymnot~\isasymnot~P = - P} means \texttt{\isasymnot\isasymnot(P = P)} and not - \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean - logical equivalence, enclose both operands in parentheses, as in \texttt{(A + typically has the lowest priority. Thus, \isa{\isasymnot~\isasymnot~P = + P} means \isa{\isasymnot\isasymnot(P = P)} and not + \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean + logical equivalence, enclose both operands in parentheses, as in \isa{(A \isasymand~B) = (B \isasymand~A)}. \item Constructs with an opening but without a closing delimiter bind very weakly and should therefore be enclosed in parentheses if they appear in subterms, as -in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if}, -\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers. +in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if}, +\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers. \item -Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x} -because \texttt{x.x} is always read as a single qualified identifier that -refers to an item \texttt{x} in theory \texttt{x}. Write -\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead. -\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}. +Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x} +because \isa{x.x} is always read as a single qualified identifier that +refers to an item \isa{x} in theory \isa{x}. Write +\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead. +\item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}. \end{itemize} -Remember that ASCII-equivalents of all mathematical symbols are -given in figure~\ref{fig:ascii} in the appendix. +For the sake of readability the usual mathematical symbols are used throughout +the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in +the appendix. + \section{Variables} \label{sec:variables} @@ -270,9 +240,9 @@ variables are automatically renamed to avoid clashes with free variables. In addition, Isabelle has a third kind of variable, called a \bfindex{schematic variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts -with a \texttt{?}. Logically, an unknown is a free variable. But it may be +with a \isa{?}. Logically, an unknown is a free variable. But it may be instantiated by another term during the proof process. For example, the -mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x}, +mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x}, which means that Isabelle can instantiate it arbitrarily. This is in contrast to ordinary variables, which remain fixed. The programming language Prolog calls unknowns {\em logical\/} variables. @@ -283,11 +253,37 @@ indicates that Isabelle will automatically instantiate those unknowns suitably when the theorem is used in some other proof. \begin{warn} - If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential - quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is + If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential + quantifier, it needs to be followed by a space. Otherwise \isa{?x} is interpreted as a schematic variable. \end{warn} +\section{Interaction and interfaces} + +Interaction with Isabelle can either occur at the shell level or through more +advanced interfaces. To keep the tutorial independent of the interface we +have phrased the description of the intraction in a neutral language. For +example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the +shell level, which is explained the first time the phrase is used. Other +interfaces perform the same act by cursor movements and/or mouse clicks. +Although shell-based interaction is quite feasible for the kind of proof +scripts currently presented in this tutorial, the recommended interface for +Isabelle/Isar is the Emacs-based \bfindex{Proof + General}~\cite{Aspinall:TACAS:2000,proofgeneral}. + +Some interfaces (including the shell level) offer special fonts with +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 +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. + + \section{Getting started} Assuming you have installed Isabelle, you start it by typing \texttt{isabelle @@ -299,4 +295,4 @@ create theory files. While you are developing a theory, we recommend to 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 earlier, Proof General offers a much superior interface. +As mentioned above, Proof General offers a much superior interface.

--- a/doc-src/TutorialI/fp.tex Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/fp.tex Tue Apr 25 08:09:10 2000 +0200 @@ -116,14 +116,13 @@ \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given string as a type in the current context. \item[(Re)loading theories:] When you start your interaction you must open a - named theory with the line - \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:}. 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 - \isacommand{use\_thy}\indexbold{*use_thy}~\texttt{"T"}. + 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"}. If you suddenly discover that you need to modify a parent theory of your current theory you must first abandon your current theory (at the shell @@ -134,6 +133,9 @@ \end{description} Further commands are found in the Isabelle/Isar Reference Manual. +We now examine Isabelle's functional programming constructs systematically, +starting with inductive datatypes. + \section{Datatypes} \label{sec:datatype} @@ -149,12 +151,12 @@ Lists are one of the essential datatypes in computing. Readers of this tutorial and users of HOL need to be familiar with their basic operations. -Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory -\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}. +Theory \isa{ToyList} is only a small fragment of HOL's predefined theory +\isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}. The latter contains many further operations. For example, the functions -\isaindexbold{hd} (`head') and \isaindexbold{tl} (`tail') return the first +\isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first element and the remainder of a list. (However, pattern-matching is usually -preferable to \isa{hd} and \isa{tl}.) Theory \texttt{List} also contains +preferable to \isa{hd} and \isa{tl}.) Theory \isa{List} also contains more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we always use HOL's predefined lists. @@ -169,7 +171,7 @@ C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~ C@m~\tau@{m1}~\dots~\tau@{mk@m} \] -where $\alpha@i$ are type variables (the parameters), $C@i$ are distinct +where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct constructor names and $\tau@{ij}$ are types; it is customary to capitalize the first letter in constructor names. There are a number of restrictions (such as that the type should not be empty) detailed @@ -192,7 +194,7 @@ Isabelle immediately sees that $f$ terminates because one (fixed!) argument becomes smaller with every recursive call. There must be exactly one equation for each constructor. Their order is immaterial. -A more general method for defining total recursive functions is explained in +A more general method for defining total recursive functions is introduced in \S\ref{sec:recdef}. \begin{exercise} @@ -276,6 +278,7 @@ the constructs introduced above. \input{Ifexpr/document/Ifexpr.tex} +\medskip How does one come up with the required lemmas? Try to prove the main theorems without them and study carefully what \isa{auto} leaves unproved. This has @@ -368,7 +371,7 @@ \subsection{Products} -HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \texttt{$\tau@1$ * +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: @@ -411,7 +414,7 @@ \subsection{Type synonyms} -\indexbold{type synonyms} +\indexbold{type synonym} Type synonyms are similar to those found in ML. Their syntax is fairly self explanatory: @@ -420,7 +423,6 @@ Note that pattern-matching is not allowed, i.e.\ each definition must be of the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$. - Section~\S\ref{sec:Simplification} explains how definitions are used in proofs. @@ -434,17 +436,17 @@ \chapter{More Functional Programming} The purpose of this chapter is to deepen the reader's understanding of the -concepts encountered so far and to introduce an advanced forms of datatypes -and recursive functions. The first two sections give a structured -presentation of theorem proving by simplification -(\S\ref{sec:Simplification}) and discuss important heuristics for induction -(\S\ref{sec:InductionHeuristics}). They can be skipped by readers less -interested in proofs. They are followed by a case study, a compiler for -expressions (\S\ref{sec:ExprCompiler}). Advanced datatypes, including those -involving function spaces, are covered in \S\ref{sec:advanced-datatypes}, -which closes with another case study, search trees (``tries''). Finally we -introduce a very general form of recursive function definition which goes -well beyond what \isacommand{primrec} allows (\S\ref{sec:recdef}). +concepts encountered so far and to introduce advanced forms of datatypes and +recursive functions. The first two sections give a structured presentation of +theorem proving by simplification (\S\ref{sec:Simplification}) and discuss +important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can +be skipped by readers less interested in proofs. They are followed by a case +study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced +datatypes, including those involving function spaces, are covered in +\S\ref{sec:advanced-datatypes}, which closes with another case study, search +trees (``tries''). Finally we introduce \isacommand{recdef}, a very general +form of recursive function definition which goes well beyond what +\isacommand{primrec} allows (\S\ref{sec:recdef}). \section{Simplification} @@ -478,7 +480,7 @@ (0#1#[]) @ [] \(\leadsto\) 0#((1#[]) @ []) \(\leadsto\) 0#(1#([] @ [])) \(\leadsto\) 0#1#[] \end{ttbox} This is also known as \bfindex{term rewriting} and the equations are referred -to as \bfindex{rewrite rules}. This is more honest than ``simplification'' +to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification'' because the terms do not necessarily become simpler in the process. \subsubsection{Simplification rules} @@ -487,7 +489,7 @@ To facilitate simplification, theorems can be declared to be simplification rules (with the help of the attribute \isa{[simp]}\index{*simp (attribute)}), in which case proofs by simplification make use of these -rules by default. In addition the constructs \isacommand{datatype} and +rules automatically. In addition the constructs \isacommand{datatype} and \isacommand{primrec} (and a few others) invisibly declare useful simplification rules. Explicit definitions are \emph{not} declared simplification rules automatically! @@ -502,14 +504,14 @@ theorems [simp] = \(list of theorem names\); theorems [simp del] = \(list of theorem names\); \end{ttbox} -As a rule of thumb, rules that really simplify (like \isa{rev(rev xs) = +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 rules. Those of a more specific nature (e.g.\ distributivity laws, which alter the structure of terms considerably) should only be used selectively, i.e.\ they should not be default simplification rules. Conversely, it may also happen that a simplification rule needs to be disabled in certain proofs. Frequent changes in the simplification status of a theorem may -indicates a badly designed theory. +indicate a badly designed theory. \begin{warn} Simplification may not terminate, for example if both $f(x) = g(x)$ and $g(x) = f(x)$ are simplification rules. It is the user's responsibility not @@ -568,7 +570,7 @@ Proving a goal containing \isaindex{let}-expressions almost invariably requires the \isa{let}-con\-structs to be expanded at some point. Since -\isa{let}-\isa{in} is just syntactic sugar for a defined constant (called +\isa{let}-\isa{in} is just syntactic sugar for a predefined constant (called \isa{Let}), expanding \isa{let}-constructs means rewriting with \isa{Let_def}: @@ -600,7 +602,7 @@ \index{arithmetic} The simplifier routinely solves a small class of linear arithmetic formulae -(over types \isa{nat} and \isa{int}): it only takes into account +(over type \isa{nat} and other numeric types): it only takes into account assumptions and conclusions that are (possibly negated) (in)equalities (\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus @@ -673,7 +675,7 @@ \end{quote} The heuristic is tricky to apply because it is not obvious that \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what -happens if you try to prove the symmetric equation! +happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}! \section{Case study: compiling expressions} @@ -719,6 +721,7 @@ right of a function arrow, but never on the left. Hence the above can of worms is ruled out but the following example of a potentially infinitely branching tree is accepted: +\smallskip \input{Datatype/document/Fundata.tex} \bigskip @@ -728,7 +731,7 @@ \begin{ttbox} datatype lam = C (lam -> lam) \end{ttbox} -do indeed make sense (note the intentionally different arrow \isa{->}!). +do indeed make sense (note the intentionally different arrow \isa{->}). There is even a version of LCF on top of HOL, called HOLCF~\cite{MuellerNvOS99}. @@ -785,11 +788,11 @@ Proper tries associate some value with each string. Since the information is stored only in the final node associated with the string, many nodes do not carry any value. This distinction is captured by the -following predefined datatype (from theory \texttt{Option}, which is a parent -of \texttt{Main}): +following predefined datatype (from theory \isa{Option}, which is a parent +of \isa{Main}): +\smallskip \input{Trie/document/Option2.tex} -\indexbold{*option}\indexbold{*None}\indexbold{*Some} - +\indexbold{*option}\indexbold{*None}\indexbold{*Some}% \input{Trie/document/Trie.tex} \begin{exercise}

--- a/doc-src/TutorialI/isabelle.sty Sun Apr 23 11:41:45 2000 +0200 +++ b/doc-src/TutorialI/isabelle.sty Tue Apr 25 08:09:10 2000 +0200 @@ -19,6 +19,9 @@ \newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}} +\newenvironment{isabellequote}% +{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}} + \newcommand{\isanewline}{\mbox{}\\\mbox{}} \chardef\isabraceleft=`\{