*** empty log message ***
authornipkow
Tue Apr 25 08:09:10 2000 +0200 (2000-04-25)
changeset 8771026f37a86ea7
parent 8770 bfab4d4b7516
child 8772 ebb07113c4f7
*** empty log message ***
doc-src/TutorialI/CodeGen/CodeGen.thy
doc-src/TutorialI/CodeGen/document/CodeGen.tex
doc-src/TutorialI/Datatype/ABexpr.thy
doc-src/TutorialI/Datatype/Fundata.thy
doc-src/TutorialI/Datatype/document/ABexpr.tex
doc-src/TutorialI/Datatype/document/Fundata.tex
doc-src/TutorialI/Ifexpr/Ifexpr.thy
doc-src/TutorialI/Ifexpr/document/Ifexpr.tex
doc-src/TutorialI/Misc/case_splits.thy
doc-src/TutorialI/Misc/cases.thy
doc-src/TutorialI/Misc/cond_rewr.thy
doc-src/TutorialI/Misc/document/case_splits.tex
doc-src/TutorialI/Misc/document/cases.tex
doc-src/TutorialI/Misc/document/cond_rewr.tex
doc-src/TutorialI/Misc/document/let_rewr.tex
doc-src/TutorialI/Misc/document/trace_simp.tex
doc-src/TutorialI/Misc/document/types.tex
doc-src/TutorialI/Misc/let_rewr.thy
doc-src/TutorialI/Misc/trace_simp.thy
doc-src/TutorialI/Misc/types.thy
doc-src/TutorialI/Recdef/Induction.thy
doc-src/TutorialI/Recdef/document/Induction.tex
doc-src/TutorialI/Recdef/document/examples.tex
doc-src/TutorialI/Recdef/document/simplification.tex
doc-src/TutorialI/Recdef/document/termination.tex
doc-src/TutorialI/Recdef/examples.thy
doc-src/TutorialI/Recdef/simplification.thy
doc-src/TutorialI/Recdef/termination.thy
doc-src/TutorialI/ToyList/ToyList.thy
doc-src/TutorialI/ToyList/document/ToyList.tex
doc-src/TutorialI/Trie/Option2.thy
doc-src/TutorialI/Trie/Trie.thy
doc-src/TutorialI/Trie/document/Option2.tex
doc-src/TutorialI/Trie/document/Trie.tex
doc-src/TutorialI/appendix.tex
doc-src/TutorialI/basics.tex
doc-src/TutorialI/fp.tex
doc-src/TutorialI/isabelle.sty
     1.1 --- a/doc-src/TutorialI/CodeGen/CodeGen.thy	Sun Apr 23 11:41:45 2000 +0200
     1.2 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy	Tue Apr 25 08:09:10 2000 +0200
     1.3 @@ -18,18 +18,18 @@
     1.4                       | Bex "'v binop"  "('a,'v)expr"  "('a,'v)expr";
     1.5  
     1.6  text{*\noindent
     1.7 -The three constructors represent constants, variables and the combination of
     1.8 -two subexpressions with a binary operation.
     1.9 +The three constructors represent constants, variables and the application of
    1.10 +a binary operation to two subexpressions.
    1.11  
    1.12  The value of an expression w.r.t.\ an environment that maps variables to
    1.13  values is easily defined:
    1.14  *}
    1.15  
    1.16 -consts value :: "('a \\<Rightarrow> 'v) \\<Rightarrow> ('a,'v)expr \\<Rightarrow> 'v";
    1.17 +consts value :: "('a,'v)expr \\<Rightarrow> ('a \\<Rightarrow> 'v) \\<Rightarrow> 'v";
    1.18  primrec
    1.19 -"value env (Cex v) = v"
    1.20 -"value env (Vex a) = env a"
    1.21 -"value env (Bex f e1 e2) = f (value env e1) (value env e2)";
    1.22 +"value (Cex v) env = v"
    1.23 +"value (Vex a) env = env a"
    1.24 +"value (Bex f e1 e2) env = f (value e1 env) (value e2 env)";
    1.25  
    1.26  text{*
    1.27  The stack machine has three instructions: load a constant value onto the
    1.28 @@ -43,20 +43,21 @@
    1.29                         | Apply "'v binop";
    1.30  
    1.31  text{*
    1.32 -The execution of the stack machine is modelled by a function \isa{exec}
    1.33 -that takes a store (modelled as a function from addresses to values, just
    1.34 -like the environment for evaluating expressions), a stack (modelled as a
    1.35 -list) of values, and a list of instructions, and returns the stack at the end
    1.36 -of the execution---the store remains unchanged:
    1.37 +The execution of the stack machine is modelled by a function
    1.38 +\isa{exec} that takes a list of instructions, a store (modelled as a
    1.39 +function from addresses to values, just like the environment for
    1.40 +evaluating expressions), and a stack (modelled as a list) of values,
    1.41 +and returns the stack at the end of the execution---the store remains
    1.42 +unchanged:
    1.43  *}
    1.44  
    1.45 -consts exec :: "('a\\<Rightarrow>'v) \\<Rightarrow> 'v list \\<Rightarrow> ('a,'v)instr list \\<Rightarrow> 'v list";
    1.46 +consts exec :: "('a,'v)instr list \\<Rightarrow> ('a\\<Rightarrow>'v) \\<Rightarrow> 'v list \\<Rightarrow> 'v list";
    1.47  primrec
    1.48 -"exec s vs [] = vs"
    1.49 -"exec s vs (i#is) = (case i of
    1.50 -    Const v  \\<Rightarrow> exec s (v#vs) is
    1.51 -  | Load a   \\<Rightarrow> exec s ((s a)#vs) is
    1.52 -  | Apply f  \\<Rightarrow> exec s ( (f (hd vs) (hd(tl vs)))#(tl(tl vs)) ) is)";
    1.53 +"exec [] s vs = vs"
    1.54 +"exec (i#is) s vs = (case i of
    1.55 +    Const v  \\<Rightarrow> exec is s (v#vs)
    1.56 +  | Load a   \\<Rightarrow> exec is s ((s a)#vs)
    1.57 +  | Apply f  \\<Rightarrow> exec is s ((f (hd vs) (hd(tl vs)))#(tl(tl vs))))";
    1.58  
    1.59  text{*\noindent
    1.60  Recall that \isa{hd} and \isa{tl}
    1.61 @@ -81,13 +82,13 @@
    1.62  Now we have to prove the correctness of the compiler, i.e.\ that the
    1.63  execution of a compiled expression results in the value of the expression:
    1.64  *}
    1.65 -theorem "exec s [] (comp e) = [value s e]";
    1.66 +theorem "exec (comp e) s [] = [value e s]";
    1.67  (*<*)oops;(*>*)
    1.68  text{*\noindent
    1.69  This theorem needs to be generalized to
    1.70  *}
    1.71  
    1.72 -theorem "\\<forall>vs. exec s vs (comp e) = (value s e) # vs";
    1.73 +theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
    1.74  
    1.75  txt{*\noindent
    1.76  which is proved by induction on \isa{e} followed by simplification, once
    1.77 @@ -96,7 +97,7 @@
    1.78  *}
    1.79  (*<*)oops;(*>*)
    1.80  lemma exec_app[simp]:
    1.81 -  "\\<forall>vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys"; 
    1.82 +  "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    1.83  
    1.84  txt{*\noindent
    1.85  This requires induction on \isa{xs} and ordinary simplification for the
    1.86 @@ -113,20 +114,20 @@
    1.87  *}
    1.88  (*<*)
    1.89  lemmas [simp del] = exec_app;
    1.90 -lemma [simp]: "\\<forall>vs. exec s vs (xs@ys) = exec s (exec s vs xs) ys"; 
    1.91 +lemma [simp]: "\\<forall>vs. exec (xs@ys) s vs = exec ys s (exec xs s vs)"; 
    1.92  (*>*)
    1.93  apply(induct_tac xs, auto split: instr.split).;
    1.94  
    1.95  text{*\noindent
    1.96  Although this is more compact, it is less clear for the reader of the proof.
    1.97  
    1.98 -We could now go back and prove \isa{exec s [] (comp e) = [value s e]}
    1.99 +We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
   1.100  merely by simplification with the generalized version we just proved.
   1.101  However, this is unnecessary because the generalized version fully subsumes
   1.102  its instance.
   1.103  *}
   1.104  (*<*)
   1.105 -theorem "\\<forall>vs. exec s vs (comp e) = (value s e) # vs";
   1.106 +theorem "\\<forall>vs. exec (comp e) s vs = (value e s) # vs";
   1.107  apply(induct_tac e, auto).;
   1.108  end
   1.109  (*>*)
     2.1 --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Sun Apr 23 11:41:45 2000 +0200
     2.2 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex	Tue Apr 25 08:09:10 2000 +0200
     2.3 @@ -16,17 +16,17 @@
     2.4  ~~~~~~~~~~~~~~~~~~~~~|~Bex~{"}'v~binop{"}~~{"}('a,'v)expr{"}~~{"}('a,'v)expr{"}%
     2.5  \begin{isamarkuptext}%
     2.6  \noindent
     2.7 -The three constructors represent constants, variables and the combination of
     2.8 -two subexpressions with a binary operation.
     2.9 +The three constructors represent constants, variables and the application of
    2.10 +a binary operation to two subexpressions.
    2.11  
    2.12  The value of an expression w.r.t.\ an environment that maps variables to
    2.13  values is easily defined:%
    2.14  \end{isamarkuptext}%
    2.15 -\isacommand{consts}~value~::~{"}('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~('a,'v)expr~{\isasymRightarrow}~'v{"}\isanewline
    2.16 +\isacommand{consts}~value~::~{"}('a,'v)expr~{\isasymRightarrow}~('a~{\isasymRightarrow}~'v)~{\isasymRightarrow}~'v{"}\isanewline
    2.17  \isacommand{primrec}\isanewline
    2.18 -{"}value~env~(Cex~v)~=~v{"}\isanewline
    2.19 -{"}value~env~(Vex~a)~=~env~a{"}\isanewline
    2.20 -{"}value~env~(Bex~f~e1~e2)~=~f~(value~env~e1)~(value~env~e2){"}%
    2.21 +{"}value~(Cex~v)~env~=~v{"}\isanewline
    2.22 +{"}value~(Vex~a)~env~=~env~a{"}\isanewline
    2.23 +{"}value~(Bex~f~e1~e2)~env~=~f~(value~e1~env)~(value~e2~env){"}%
    2.24  \begin{isamarkuptext}%
    2.25  The stack machine has three instructions: load a constant value onto the
    2.26  stack, load the contents of a certain address onto the stack, and apply a
    2.27 @@ -37,19 +37,20 @@
    2.28  ~~~~~~~~~~~~~~~~~~~~~~~|~Load~'a\isanewline
    2.29  ~~~~~~~~~~~~~~~~~~~~~~~|~Apply~{"}'v~binop{"}%
    2.30  \begin{isamarkuptext}%
    2.31 -The execution of the stack machine is modelled by a function \isa{exec}
    2.32 -that takes a store (modelled as a function from addresses to values, just
    2.33 -like the environment for evaluating expressions), a stack (modelled as a
    2.34 -list) of values, and a list of instructions, and returns the stack at the end
    2.35 -of the execution---the store remains unchanged:%
    2.36 +The execution of the stack machine is modelled by a function
    2.37 +\isa{exec} that takes a list of instructions, a store (modelled as a
    2.38 +function from addresses to values, just like the environment for
    2.39 +evaluating expressions), and a stack (modelled as a list) of values,
    2.40 +and returns the stack at the end of the execution---the store remains
    2.41 +unchanged:%
    2.42  \end{isamarkuptext}%
    2.43 -\isacommand{consts}~exec~::~{"}('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~('a,'v)instr~list~{\isasymRightarrow}~'v~list{"}\isanewline
    2.44 +\isacommand{consts}~exec~::~{"}('a,'v)instr~list~{\isasymRightarrow}~('a{\isasymRightarrow}'v)~{\isasymRightarrow}~'v~list~{\isasymRightarrow}~'v~list{"}\isanewline
    2.45  \isacommand{primrec}\isanewline
    2.46 -{"}exec~s~vs~[]~=~vs{"}\isanewline
    2.47 -{"}exec~s~vs~(i\#is)~=~(case~i~of\isanewline
    2.48 -~~~~Const~v~~{\isasymRightarrow}~exec~s~(v\#vs)~is\isanewline
    2.49 -~~|~Load~a~~~{\isasymRightarrow}~exec~s~((s~a)\#vs)~is\isanewline
    2.50 -~~|~Apply~f~~{\isasymRightarrow}~exec~s~(~(f~(hd~vs)~(hd(tl~vs)))\#(tl(tl~vs))~)~is){"}%
    2.51 +{"}exec~[]~s~vs~=~vs{"}\isanewline
    2.52 +{"}exec~(i\#is)~s~vs~=~(case~i~of\isanewline
    2.53 +~~~~Const~v~~{\isasymRightarrow}~exec~is~s~(v\#vs)\isanewline
    2.54 +~~|~Load~a~~~{\isasymRightarrow}~exec~is~s~((s~a)\#vs)\isanewline
    2.55 +~~|~Apply~f~~{\isasymRightarrow}~exec~is~s~((f~(hd~vs)~(hd(tl~vs)))\#(tl(tl~vs)))){"}%
    2.56  \begin{isamarkuptext}%
    2.57  \noindent
    2.58  Recall that \isa{hd} and \isa{tl}
    2.59 @@ -72,12 +73,12 @@
    2.60  Now we have to prove the correctness of the compiler, i.e.\ that the
    2.61  execution of a compiled expression results in the value of the expression:%
    2.62  \end{isamarkuptext}%
    2.63 -\isacommand{theorem}~{"}exec~s~[]~(comp~e)~=~[value~s~e]{"}%
    2.64 +\isacommand{theorem}~{"}exec~(comp~e)~s~[]~=~[value~e~s]{"}%
    2.65  \begin{isamarkuptext}%
    2.66  \noindent
    2.67  This theorem needs to be generalized to%
    2.68  \end{isamarkuptext}%
    2.69 -\isacommand{theorem}~{"}{\isasymforall}vs.~exec~s~vs~(comp~e)~=~(value~s~e)~\#~vs{"}%
    2.70 +\isacommand{theorem}~{"}{\isasymforall}vs.~exec~(comp~e)~s~vs~=~(value~e~s)~\#~vs{"}%
    2.71  \begin{isamarkuptxt}%
    2.72  \noindent
    2.73  which is proved by induction on \isa{e} followed by simplification, once
    2.74 @@ -85,7 +86,7 @@
    2.75  instruction sequences:%
    2.76  \end{isamarkuptxt}%
    2.77  \isacommand{lemma}~exec\_app[simp]:\isanewline
    2.78 -~~{"}{\isasymforall}vs.~exec~s~vs~(xs@ys)~=~exec~s~(exec~s~vs~xs)~ys{"}%
    2.79 +~~{"}{\isasymforall}vs.~exec~(xs@ys)~s~vs~=~exec~ys~s~(exec~xs~s~vs){"}%
    2.80  \begin{isamarkuptxt}%
    2.81  \noindent
    2.82  This requires induction on \isa{xs} and ordinary simplification for the
    2.83 @@ -105,7 +106,7 @@
    2.84  \noindent
    2.85  Although this is more compact, it is less clear for the reader of the proof.
    2.86  
    2.87 -We could now go back and prove \isa{exec s [] (comp e) = [value s e]}
    2.88 +We could now go back and prove \isa{exec (comp e) s [] = [value e s]}
    2.89  merely by simplification with the generalized version we just proved.
    2.90  However, this is unnecessary because the generalized version fully subsumes
    2.91  its instance.%
     3.1 --- a/doc-src/TutorialI/Datatype/ABexpr.thy	Sun Apr 23 11:41:45 2000 +0200
     3.2 +++ b/doc-src/TutorialI/Datatype/ABexpr.thy	Tue Apr 25 08:09:10 2000 +0200
     3.3 @@ -33,28 +33,28 @@
     3.4  The semantics is fixed via two evaluation functions
     3.5  *}
     3.6  
     3.7 -consts  evala :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a aexp \\<Rightarrow> nat"
     3.8 -        evalb :: "('a \\<Rightarrow> nat) \\<Rightarrow> 'a bexp \\<Rightarrow> bool";
     3.9 +consts  evala :: "'a aexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> nat"
    3.10 +        evalb :: "'a bexp \\<Rightarrow> ('a \\<Rightarrow> nat) \\<Rightarrow> bool";
    3.11  
    3.12  text{*\noindent
    3.13 -that take an environment (a mapping from variables \isa{'a} to values
    3.14 -\isa{nat}) and an expression and return its arithmetic/boolean
    3.15 +that take an expression and an environment (a mapping from variables \isa{'a} to values
    3.16 +\isa{nat}) and return its arithmetic/boolean
    3.17  value. Since the datatypes are mutually recursive, so are functions that
    3.18  operate on them. Hence they need to be defined in a single \isacommand{primrec}
    3.19  section:
    3.20  *}
    3.21  
    3.22  primrec
    3.23 -  "evala env (IF b a1 a2) =
    3.24 -     (if evalb env b then evala env a1 else evala env a2)"
    3.25 -  "evala env (Sum a1 a2) = evala env a1 + evala env a2"
    3.26 -  "evala env (Diff a1 a2) = evala env a1 - evala env a2"
    3.27 -  "evala env (Var v) = env v"
    3.28 -  "evala env (Num n) = n"
    3.29 +  "evala (IF b a1 a2) env =
    3.30 +     (if evalb b env then evala a1 env else evala a2 env)"
    3.31 +  "evala (Sum a1 a2) env = evala a1 env + evala a2 env"
    3.32 +  "evala (Diff a1 a2) env = evala a1 env - evala a2 env"
    3.33 +  "evala (Var v) env = env v"
    3.34 +  "evala (Num n) env = n"
    3.35  
    3.36 -  "evalb env (Less a1 a2) = (evala env a1 < evala env a2)"
    3.37 -  "evalb env (And b1 b2) = (evalb env b1 \\<and> evalb env b2)"
    3.38 -  "evalb env (Neg b) = (\\<not> evalb env b)"
    3.39 +  "evalb (Less a1 a2) env = (evala a1 env < evala a2 env)"
    3.40 +  "evalb (And b1 b2) env = (evalb b1 env \\<and> evalb b2 env)"
    3.41 +  "evalb (Neg b) env = (\\<not> evalb b env)"
    3.42  
    3.43  text{*\noindent
    3.44  In the same fashion we also define two functions that perform substitution:
    3.45 @@ -93,8 +93,8 @@
    3.46  theorems simultaneously:
    3.47  *}
    3.48  
    3.49 -lemma "evala env (substa s a) = evala (\\<lambda>x. evala env (s x)) a \\<and>
    3.50 -        evalb env (substb s b) = evalb (\\<lambda>x. evala env (s x)) b";
    3.51 +lemma "evala (substa s a) env = evala a (\\<lambda>x. evala (s x) env) \\<and>
    3.52 +        evalb (substb s b) env = evalb b (\\<lambda>x. evala (s x) env)";
    3.53  apply(induct_tac a and b);
    3.54  
    3.55  txt{*\noindent
     4.1 --- a/doc-src/TutorialI/Datatype/Fundata.thy	Sun Apr 23 11:41:45 2000 +0200
     4.2 +++ b/doc-src/TutorialI/Datatype/Fundata.thy	Tue Apr 25 08:09:10 2000 +0200
     4.3 @@ -14,7 +14,7 @@
     4.4  term "Branch 0 (\\<lambda>i. Branch i (\\<lambda>n. Tip))";
     4.5  
     4.6  text{*\noindent of type \isa{(nat,nat)bigtree} is the tree whose
     4.7 -root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
     4.8 +root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
     4.9  has merely \isa{Tip}s as further subtrees.
    4.10  
    4.11  Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:
    4.12 @@ -35,7 +35,7 @@
    4.13  
    4.14  The following lemma has a canonical proof  *}
    4.15  
    4.16 -lemma "map_bt g (map_bt f T) = map_bt (g o f) T";
    4.17 +lemma "map_bt (g o f) T = map_bt g (map_bt f T)";
    4.18  apply(induct_tac "T", auto).
    4.19  
    4.20  text{*\noindent
     5.1 --- a/doc-src/TutorialI/Datatype/document/ABexpr.tex	Sun Apr 23 11:41:45 2000 +0200
     5.2 +++ b/doc-src/TutorialI/Datatype/document/ABexpr.tex	Tue Apr 25 08:09:10 2000 +0200
     5.3 @@ -29,27 +29,27 @@
     5.4  expressions can be arithmetic comparisons, conjunctions and negations.
     5.5  The semantics is fixed via two evaluation functions%
     5.6  \end{isamarkuptext}%
     5.7 -\isacommand{consts}~~evala~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~aexp~{\isasymRightarrow}~nat{"}\isanewline
     5.8 -~~~~~~~~evalb~::~{"}('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~'a~bexp~{\isasymRightarrow}~bool{"}%
     5.9 +\isacommand{consts}~~evala~::~{"}'a~aexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~nat{"}\isanewline
    5.10 +~~~~~~~~evalb~::~{"}'a~bexp~{\isasymRightarrow}~('a~{\isasymRightarrow}~nat)~{\isasymRightarrow}~bool{"}%
    5.11  \begin{isamarkuptext}%
    5.12  \noindent
    5.13 -that take an environment (a mapping from variables \isa{'a} to values
    5.14 -\isa{nat}) and an expression and return its arithmetic/boolean
    5.15 +that take an expression and an environment (a mapping from variables \isa{'a} to values
    5.16 +\isa{nat}) and return its arithmetic/boolean
    5.17  value. Since the datatypes are mutually recursive, so are functions that
    5.18  operate on them. Hence they need to be defined in a single \isacommand{primrec}
    5.19  section:%
    5.20  \end{isamarkuptext}%
    5.21  \isacommand{primrec}\isanewline
    5.22 -~~{"}evala~env~(IF~b~a1~a2)~=\isanewline
    5.23 -~~~~~(if~evalb~env~b~then~evala~env~a1~else~evala~env~a2){"}\isanewline
    5.24 -~~{"}evala~env~(Sum~a1~a2)~=~evala~env~a1~+~evala~env~a2{"}\isanewline
    5.25 -~~{"}evala~env~(Diff~a1~a2)~=~evala~env~a1~-~evala~env~a2{"}\isanewline
    5.26 -~~{"}evala~env~(Var~v)~=~env~v{"}\isanewline
    5.27 -~~{"}evala~env~(Num~n)~=~n{"}\isanewline
    5.28 +~~{"}evala~(IF~b~a1~a2)~env~=\isanewline
    5.29 +~~~~~(if~evalb~b~env~then~evala~a1~env~else~evala~a2~env){"}\isanewline
    5.30 +~~{"}evala~(Sum~a1~a2)~env~=~evala~a1~env~+~evala~a2~env{"}\isanewline
    5.31 +~~{"}evala~(Diff~a1~a2)~env~=~evala~a1~env~-~evala~a2~env{"}\isanewline
    5.32 +~~{"}evala~(Var~v)~env~=~env~v{"}\isanewline
    5.33 +~~{"}evala~(Num~n)~env~=~n{"}\isanewline
    5.34  \isanewline
    5.35 -~~{"}evalb~env~(Less~a1~a2)~=~(evala~env~a1~<~evala~env~a2){"}\isanewline
    5.36 -~~{"}evalb~env~(And~b1~b2)~=~(evalb~env~b1~{\isasymand}~evalb~env~b2){"}\isanewline
    5.37 -~~{"}evalb~env~(Neg~b)~=~({\isasymnot}~evalb~env~b){"}%
    5.38 +~~{"}evalb~(Less~a1~a2)~env~=~(evala~a1~env~<~evala~a2~env){"}\isanewline
    5.39 +~~{"}evalb~(And~b1~b2)~env~=~(evalb~b1~env~{\isasymand}~evalb~b2~env){"}\isanewline
    5.40 +~~{"}evalb~(Neg~b)~env~=~({\isasymnot}~evalb~b~env){"}%
    5.41  \begin{isamarkuptext}%
    5.42  \noindent
    5.43  In the same fashion we also define two functions that perform substitution:%
    5.44 @@ -84,8 +84,8 @@
    5.45  theorem in the induction step. Therefore you need to state and prove both
    5.46  theorems simultaneously:%
    5.47  \end{isamarkuptext}%
    5.48 -\isacommand{lemma}~{"}evala~env~(substa~s~a)~=~evala~({\isasymlambda}x.~evala~env~(s~x))~a~{\isasymand}\isanewline
    5.49 -~~~~~~~~evalb~env~(substb~s~b)~=~evalb~({\isasymlambda}x.~evala~env~(s~x))~b{"}\isanewline
    5.50 +\isacommand{lemma}~{"}evala~(substa~s~a)~env~=~evala~a~({\isasymlambda}x.~evala~(s~x)~env)~{\isasymand}\isanewline
    5.51 +~~~~~~~~evalb~(substb~s~b)~env~=~evalb~b~({\isasymlambda}x.~evala~(s~x)~env){"}\isanewline
    5.52  \isacommand{apply}(induct\_tac~a~\isakeyword{and}~b)%
    5.53  \begin{isamarkuptxt}%
    5.54  \noindent
     6.1 --- a/doc-src/TutorialI/Datatype/document/Fundata.tex	Sun Apr 23 11:41:45 2000 +0200
     6.2 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex	Tue Apr 25 08:09:10 2000 +0200
     6.3 @@ -12,7 +12,7 @@
     6.4  \isacommand{term}~{"}Branch~0~({\isasymlambda}i.~Branch~i~({\isasymlambda}n.~Tip)){"}%
     6.5  \begin{isamarkuptext}%
     6.6  \noindent of type \isa{(nat,nat)bigtree} is the tree whose
     6.7 -root is labeled with 0 and whose $n$th subtree is labeled with $n$ and
     6.8 +root is labeled with 0 and whose $i$th subtree is labeled with $i$ and
     6.9  has merely \isa{Tip}s as further subtrees.
    6.10  
    6.11  Function \isa{map_bt} applies a function to all labels in a \isa{bigtree}:%
    6.12 @@ -32,7 +32,7 @@
    6.13  
    6.14  The following lemma has a canonical proof%
    6.15  \end{isamarkuptext}%
    6.16 -\isacommand{lemma}~{"}map\_bt~g~(map\_bt~f~T)~=~map\_bt~(g~o~f)~T{"}\isanewline
    6.17 +\isacommand{lemma}~{"}map\_bt~(g~o~f)~T~=~map\_bt~g~(map\_bt~f~T){"}\isanewline
    6.18  \isacommand{apply}(induct\_tac~{"}T{"},~auto)\isacommand{.}%
    6.19  \begin{isamarkuptext}%
    6.20  \noindent
     7.1 --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Sun Apr 23 11:41:45 2000 +0200
     7.2 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy	Tue Apr 25 08:09:10 2000 +0200
     7.3 @@ -61,7 +61,7 @@
     7.4  \subsubsection{Transformation into and of If-expressions}
     7.5  
     7.6  The type \isa{boolex} is close to the customary representation of logical
     7.7 -formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
     7.8 +formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
     7.9  translate from \isa{boolex} into \isa{ifex}:
    7.10  *}
    7.11  
    7.12 @@ -153,7 +153,8 @@
    7.13  normality of \isa{normif}:
    7.14  *}
    7.15  
    7.16 -lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";(*<*)
    7.17 +lemma [simp]: "\\<forall>t e. normal(normif b t e) = (normal t \\<and> normal e)";
    7.18 +(*<*)
    7.19  apply(induct_tac b);
    7.20  apply(auto).;
    7.21  
    7.22 @@ -161,4 +162,5 @@
    7.23  apply(induct_tac b);
    7.24  apply(auto).;
    7.25  
    7.26 -end(*>*)
    7.27 +end
    7.28 +(*>*)
     8.1 --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Sun Apr 23 11:41:45 2000 +0200
     8.2 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex	Tue Apr 25 08:09:10 2000 +0200
     8.3 @@ -54,7 +54,7 @@
     8.4  \subsubsection{Transformation into and of If-expressions}
     8.5  
     8.6  The type \isa{boolex} is close to the customary representation of logical
     8.7 -formulae, whereas \isa{ifex} is designed for efficiency. Thus we need to
     8.8 +formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
     8.9  translate from \isa{boolex} into \isa{ifex}:%
    8.10  \end{isamarkuptext}%
    8.11  \isacommand{consts}~bool2if~::~{"}boolex~{\isasymRightarrow}~ifex{"}\isanewline
     9.1 --- a/doc-src/TutorialI/Misc/case_splits.thy	Sun Apr 23 11:41:45 2000 +0200
     9.2 +++ b/doc-src/TutorialI/Misc/case_splits.thy	Tue Apr 25 08:09:10 2000 +0200
     9.3 @@ -48,15 +48,16 @@
     9.4  In contrast to \isa{if}-expressions, the simplifier does not split
     9.5  \isa{case}-expressions by default because this can lead to nontermination
     9.6  in case of recursive datatypes. Again, if the \isa{only:} modifier is
     9.7 -dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)}
     9.8 -alone will not do:
     9.9 +dropped, the above goal is solved,
    9.10  *}
    9.11  (*<*)
    9.12  lemma "(case xs of [] \\<Rightarrow> zs | y#ys \\<Rightarrow> y#(ys@zs)) = xs@zs";
    9.13  (*>*)
    9.14  apply(simp split: list.split).;
    9.15  
    9.16 -text{*
    9.17 +text{*\noindent%
    9.18 +which \isacommand{apply}\isa{(simp)} alone will not do.
    9.19 +
    9.20  In general, every datatype $t$ comes with a theorem
    9.21  \isa{$t$.split} which can be declared to be a \bfindex{split rule} either
    9.22  locally as above, or by giving it the \isa{split} attribute globally:
    10.1 --- a/doc-src/TutorialI/Misc/cases.thy	Sun Apr 23 11:41:45 2000 +0200
    10.2 +++ b/doc-src/TutorialI/Misc/cases.thy	Tue Apr 25 08:09:10 2000 +0200
    10.3 @@ -5,11 +5,13 @@
    10.4  lemma "(case xs of [] \\<Rightarrow> [] | y#ys \\<Rightarrow> xs) = xs";
    10.5  apply(case_tac xs);
    10.6  
    10.7 -txt{*
    10.8 +txt{*\noindent
    10.9 +results in the proof state
   10.10  \begin{isabellepar}%
   10.11  ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
   10.12  ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
   10.13  \end{isabellepar}%
   10.14 +which is solved automatically:
   10.15  *}
   10.16  
   10.17  apply(auto).;
    11.1 --- a/doc-src/TutorialI/Misc/cond_rewr.thy	Sun Apr 23 11:41:45 2000 +0200
    11.2 +++ b/doc-src/TutorialI/Misc/cond_rewr.thy	Tue Apr 25 08:09:10 2000 +0200
    11.3 @@ -23,7 +23,7 @@
    11.4  apply(simp).
    11.5  (*>*)
    11.6  text{*\noindent
    11.7 -is proved by simplification:
    11.8 +is proved by plain simplification:
    11.9  the conditional equation \isa{hd_Cons_tl} above
   11.10  can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs}
   11.11  because the corresponding precondition \isa{rev xs \isasymnoteq\ []}
    12.1 --- a/doc-src/TutorialI/Misc/document/case_splits.tex	Sun Apr 23 11:41:45 2000 +0200
    12.2 +++ b/doc-src/TutorialI/Misc/document/case_splits.tex	Tue Apr 25 08:09:10 2000 +0200
    12.3 @@ -41,11 +41,13 @@
    12.4  In contrast to \isa{if}-expressions, the simplifier does not split
    12.5  \isa{case}-expressions by default because this can lead to nontermination
    12.6  in case of recursive datatypes. Again, if the \isa{only:} modifier is
    12.7 -dropped, the above goal is solved, which \isacommand{apply}\isa{(simp)}
    12.8 -alone will not do:%
    12.9 +dropped, the above goal is solved,%
   12.10  \end{isamarkuptext}%
   12.11  \isacommand{apply}(simp~split:~list.split)\isacommand{.}%
   12.12  \begin{isamarkuptext}%
   12.13 +\noindent%
   12.14 +which \isacommand{apply}\isa{(simp)} alone will not do.
   12.15 +
   12.16  In general, every datatype $t$ comes with a theorem
   12.17  \isa{$t$.split} which can be declared to be a \bfindex{split rule} either
   12.18  locally as above, or by giving it the \isa{split} attribute globally:%
    13.1 --- a/doc-src/TutorialI/Misc/document/cases.tex	Sun Apr 23 11:41:45 2000 +0200
    13.2 +++ b/doc-src/TutorialI/Misc/document/cases.tex	Tue Apr 25 08:09:10 2000 +0200
    13.3 @@ -3,10 +3,13 @@
    13.4  \isacommand{lemma}~{"}(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs{"}\isanewline
    13.5  \isacommand{apply}(case\_tac~xs)%
    13.6  \begin{isamarkuptxt}%
    13.7 +\noindent
    13.8 +results in the proof state
    13.9  \begin{isabellepar}%
   13.10  ~1.~xs~=~[]~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y~\#~ys~{\isasymRightarrow}~xs)~=~xs\isanewline
   13.11  ~2.~{\isasymAnd}a~list.~xs=a\#list~{\isasymLongrightarrow}~(case~xs~of~[]~{\isasymRightarrow}~[]~|~y\#ys~{\isasymRightarrow}~xs)~=~xs%
   13.12 -\end{isabellepar}%%
   13.13 +\end{isabellepar}%
   13.14 +which is solved automatically:%
   13.15  \end{isamarkuptxt}%
   13.16  \isacommand{apply}(auto)\isacommand{.}\isanewline
   13.17  \end{isabelle}%
    14.1 --- a/doc-src/TutorialI/Misc/document/cond_rewr.tex	Sun Apr 23 11:41:45 2000 +0200
    14.2 +++ b/doc-src/TutorialI/Misc/document/cond_rewr.tex	Tue Apr 25 08:09:10 2000 +0200
    14.3 @@ -19,7 +19,7 @@
    14.4  \isacommand{lemma}~{"}xs~{\isasymnoteq}~[]~{\isasymLongrightarrow}~hd(rev~xs)~\#~tl(rev~xs)~=~rev~xs{"}%
    14.5  \begin{isamarkuptext}%
    14.6  \noindent
    14.7 -is proved by simplification:
    14.8 +is proved by plain simplification:
    14.9  the conditional equation \isa{hd_Cons_tl} above
   14.10  can simplify \isa{hd(rev~xs)~\#~tl(rev~xs)} to \isa{rev xs}
   14.11  because the corresponding precondition \isa{rev xs \isasymnoteq\ []}
    15.1 --- a/doc-src/TutorialI/Misc/document/let_rewr.tex	Sun Apr 23 11:41:45 2000 +0200
    15.2 +++ b/doc-src/TutorialI/Misc/document/let_rewr.tex	Tue Apr 25 08:09:10 2000 +0200
    15.3 @@ -3,6 +3,6 @@
    15.4  \isacommand{apply}(simp~add:~Let\_def)\isacommand{.}%
    15.5  \begin{isamarkuptext}%
    15.6  If, in a particular context, there is no danger of a combinatorial explosion
    15.7 -of nested \texttt{let}s one could even add \texttt{Let_def} permanently:%
    15.8 +of nested \isa{let}s one could even add \isa{Let_def} permanently:%
    15.9  \end{isamarkuptext}%
   15.10  \isacommand{theorems}~[simp]~=~Let\_def\end{isabelle}%
    16.1 --- a/doc-src/TutorialI/Misc/document/trace_simp.tex	Sun Apr 23 11:41:45 2000 +0200
    16.2 +++ b/doc-src/TutorialI/Misc/document/trace_simp.tex	Tue Apr 25 08:09:10 2000 +0200
    16.3 @@ -31,7 +31,7 @@
    16.4  [x] = [] == False
    16.5  \end{ttbox}
    16.6  
    16.7 -In more complicated cases, the trace can quite lenghty, especially since
    16.8 +In more complicated cases, the trace can be quite lenghty, especially since
    16.9  invocations of the simplifier are often nested (e.g.\ when solving conditions
   16.10  of rewrite rules). Thus it is advisable to reset it:%
   16.11  \end{isamarkuptxt}%
    17.1 --- a/doc-src/TutorialI/Misc/document/types.tex	Sun Apr 23 11:41:45 2000 +0200
    17.2 +++ b/doc-src/TutorialI/Misc/document/types.tex	Tue Apr 25 08:09:10 2000 +0200
    17.3 @@ -6,7 +6,7 @@
    17.4  \noindent\indexbold{*types}%
    17.5  Internally all synonyms are fully expanded.  As a consequence Isabelle's
    17.6  output never contains synonyms.  Their main purpose is to improve the
    17.7 -readability of theory definitions.  Synonyms can be used just like any other
    17.8 +readability of theories.  Synonyms can be used just like any other
    17.9  type:%
   17.10  \end{isamarkuptext}%
   17.11  \isacommand{consts}~nand~::~gate\isanewline
   17.12 @@ -24,7 +24,7 @@
   17.13  \begin{isamarkuptext}%
   17.14  \noindent%
   17.15  where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
   17.16 -\isa{exor_def} are arbitrary user-supplied names.
   17.17 +\isa{exor_def} are user-supplied names.
   17.18  The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
   17.19  that should only be used in constant definitions.
   17.20  Declarations and definitions can also be merged%
    18.1 --- a/doc-src/TutorialI/Misc/let_rewr.thy	Sun Apr 23 11:41:45 2000 +0200
    18.2 +++ b/doc-src/TutorialI/Misc/let_rewr.thy	Tue Apr 25 08:09:10 2000 +0200
    18.3 @@ -6,7 +6,7 @@
    18.4  
    18.5  text{*
    18.6  If, in a particular context, there is no danger of a combinatorial explosion
    18.7 -of nested \texttt{let}s one could even add \texttt{Let_def} permanently:
    18.8 +of nested \isa{let}s one could even add \isa{Let_def} permanently:
    18.9  *}
   18.10  theorems [simp] = Let_def;
   18.11  (*<*)
    19.1 --- a/doc-src/TutorialI/Misc/trace_simp.thy	Sun Apr 23 11:41:45 2000 +0200
    19.2 +++ b/doc-src/TutorialI/Misc/trace_simp.thy	Tue Apr 25 08:09:10 2000 +0200
    19.3 @@ -33,7 +33,7 @@
    19.4  [x] = [] == False
    19.5  \end{ttbox}
    19.6  
    19.7 -In more complicated cases, the trace can quite lenghty, especially since
    19.8 +In more complicated cases, the trace can be quite lenghty, especially since
    19.9  invocations of the simplifier are often nested (e.g.\ when solving conditions
   19.10  of rewrite rules). Thus it is advisable to reset it:
   19.11  *}
    20.1 --- a/doc-src/TutorialI/Misc/types.thy	Sun Apr 23 11:41:45 2000 +0200
    20.2 +++ b/doc-src/TutorialI/Misc/types.thy	Tue Apr 25 08:09:10 2000 +0200
    20.3 @@ -7,7 +7,7 @@
    20.4  text{*\noindent\indexbold{*types}%
    20.5  Internally all synonyms are fully expanded.  As a consequence Isabelle's
    20.6  output never contains synonyms.  Their main purpose is to improve the
    20.7 -readability of theory definitions.  Synonyms can be used just like any other
    20.8 +readability of theories.  Synonyms can be used just like any other
    20.9  type:
   20.10  *}
   20.11  
   20.12 @@ -28,7 +28,7 @@
   20.13  
   20.14  text{*\noindent%
   20.15  where \isacommand{defs}\indexbold{*defs} is a keyword and \isa{nand_def} and
   20.16 -\isa{exor_def} are arbitrary user-supplied names.
   20.17 +\isa{exor_def} are user-supplied names.
   20.18  The symbol \indexboldpos{\isasymequiv}{$IsaEq} is a special form of equality
   20.19  that should only be used in constant definitions.
   20.20  Declarations and definitions can also be merged
    21.1 --- a/doc-src/TutorialI/Recdef/Induction.thy	Sun Apr 23 11:41:45 2000 +0200
    21.2 +++ b/doc-src/TutorialI/Recdef/Induction.thy	Tue Apr 25 08:09:10 2000 +0200
    21.3 @@ -15,7 +15,7 @@
    21.4  \textbf{recursion induction}. Roughly speaking, it
    21.5  requires you to prove for each \isacommand{recdef} equation that the property
    21.6  you are trying to establish holds for the left-hand side provided it holds
    21.7 -for all recursive calls on the right-hand side. Here is a simple example:
    21.8 +for all recursive calls on the right-hand side. Here is a simple example
    21.9  *}
   21.10  
   21.11  lemma "map f (sep(x,xs)) = sep(f x, map f xs)";
    22.1 --- a/doc-src/TutorialI/Recdef/document/Induction.tex	Sun Apr 23 11:41:45 2000 +0200
    22.2 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex	Tue Apr 25 08:09:10 2000 +0200
    22.3 @@ -13,7 +13,7 @@
    22.4  \textbf{recursion induction}. Roughly speaking, it
    22.5  requires you to prove for each \isacommand{recdef} equation that the property
    22.6  you are trying to establish holds for the left-hand side provided it holds
    22.7 -for all recursive calls on the right-hand side. Here is a simple example:%
    22.8 +for all recursive calls on the right-hand side. Here is a simple example%
    22.9  \end{isamarkuptext}%
   22.10  \isacommand{lemma}~{"}map~f~(sep(x,xs))~=~sep(f~x,~map~f~xs){"}%
   22.11  \begin{isamarkuptxt}%
    23.1 --- a/doc-src/TutorialI/Recdef/document/examples.tex	Sun Apr 23 11:41:45 2000 +0200
    23.2 +++ b/doc-src/TutorialI/Recdef/document/examples.tex	Tue Apr 25 08:09:10 2000 +0200
    23.3 @@ -11,7 +11,7 @@
    23.4  \begin{isamarkuptext}%
    23.5  \noindent
    23.6  The definition of \isa{fib} is accompanied by a \bfindex{measure function}
    23.7 -\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
    23.8 +\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
    23.9  natural number. The requirement is that in each equation the measure of the
   23.10  argument on the left-hand side is strictly greater than the measure of the
   23.11  argument of each recursive call. In the case of \isa{fib} this is
   23.12 @@ -74,7 +74,7 @@
   23.13  ~~{"}swap12~zs~~~~~~~=~zs{"}%
   23.14  \begin{isamarkuptext}%
   23.15  \noindent
   23.16 -In the non-recursive case the termination measure degenerates to the empty
   23.17 +For non-recursive functions the termination measure degenerates to the empty
   23.18  set \isa{\{\}}.%
   23.19  \end{isamarkuptext}%
   23.20  \end{isabelle}%
    24.1 --- a/doc-src/TutorialI/Recdef/document/simplification.tex	Sun Apr 23 11:41:45 2000 +0200
    24.2 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex	Tue Apr 25 08:09:10 2000 +0200
    24.3 @@ -42,10 +42,10 @@
    24.4  \begin{isamarkuptext}%
    24.5  \noindent
    24.6  Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
    24.7 -an \isa{if}, this leads to an infinite chain of simplification steps.
    24.8 +an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
    24.9  Fortunately, this problem can be avoided in many different ways.
   24.10  
   24.11 -Of course the most radical solution is to disable the offending
   24.12 +The most radical solution is to disable the offending
   24.13  \isa{split_if} as shown in the section on case splits in
   24.14  \S\ref{sec:SimpFeatures}.
   24.15  However, we do not recommend this because it means you will often have to
    25.1 --- a/doc-src/TutorialI/Recdef/document/termination.tex	Sun Apr 23 11:41:45 2000 +0200
    25.2 +++ b/doc-src/TutorialI/Recdef/document/termination.tex	Tue Apr 25 08:09:10 2000 +0200
    25.3 @@ -4,8 +4,8 @@
    25.4  When a function is defined via \isacommand{recdef}, Isabelle tries to prove
    25.5  its termination with the help of the user-supplied measure.  All of the above
    25.6  examples are simple enough that Isabelle can prove automatically that the
    25.7 -measure of the argument goes down in each recursive call. In that case
    25.8 -$f$.\isa{simps} contains the defining equations (or variants derived from
    25.9 +measure of the argument goes down in each recursive call. As a result,
   25.10 +\isa{$f$.simps} will contain the defining equations (or variants derived from
   25.11  them) as theorems. For example, look (via \isacommand{thm}) at
   25.12  \isa{sep.simps} and \isa{sep1.simps} to see that they define the same
   25.13  function. What is more, those equations are automatically declared as
   25.14 @@ -34,8 +34,8 @@
   25.15  \isacommand{apply}(arith)\isacommand{.}%
   25.16  \begin{isamarkuptext}%
   25.17  \noindent
   25.18 -Because \isacommand{recdef}'s the termination prover involves simplification,
   25.19 -we have declared our lemma a simplification rule. Therefore our second
   25.20 +Because \isacommand{recdef}'s termination prover involves simplification,
   25.21 +we have turned our lemma into a simplification rule. Therefore our second
   25.22  attempt to define our function will automatically take it into account:%
   25.23  \end{isamarkuptext}%
   25.24  \isacommand{consts}~g~::~{"}nat*nat~{\isasymRightarrow}~nat{"}\isanewline
    26.1 --- a/doc-src/TutorialI/Recdef/examples.thy	Sun Apr 23 11:41:45 2000 +0200
    26.2 +++ b/doc-src/TutorialI/Recdef/examples.thy	Tue Apr 25 08:09:10 2000 +0200
    26.3 @@ -14,7 +14,7 @@
    26.4  
    26.5  text{*\noindent
    26.6  The definition of \isa{fib} is accompanied by a \bfindex{measure function}
    26.7 -\isa{\isasymlambda{}n.$\;$n} that maps the argument of \isa{fib} to a
    26.8 +\isa{\isasymlambda{}n.$\;$n} which maps the argument of \isa{fib} to a
    26.9  natural number. The requirement is that in each equation the measure of the
   26.10  argument on the left-hand side is strictly greater than the measure of the
   26.11  argument of each recursive call. In the case of \isa{fib} this is
   26.12 @@ -83,7 +83,7 @@
   26.13    "swap12 zs       = zs";
   26.14  
   26.15  text{*\noindent
   26.16 -In the non-recursive case the termination measure degenerates to the empty
   26.17 +For non-recursive functions the termination measure degenerates to the empty
   26.18  set \isa{\{\}}.
   26.19  *}
   26.20  
    27.1 --- a/doc-src/TutorialI/Recdef/simplification.thy	Sun Apr 23 11:41:45 2000 +0200
    27.2 +++ b/doc-src/TutorialI/Recdef/simplification.thy	Tue Apr 25 08:09:10 2000 +0200
    27.3 @@ -49,10 +49,10 @@
    27.4  
    27.5  text{*\noindent
    27.6  Since the recursive call \isa{gcd(n, m mod n)} is no longer protected by
    27.7 -an \isa{if}, this leads to an infinite chain of simplification steps.
    27.8 +an \isa{if}, it is unfolded again, which leads to an infinite chain of simplification steps.
    27.9  Fortunately, this problem can be avoided in many different ways.
   27.10  
   27.11 -Of course the most radical solution is to disable the offending
   27.12 +The most radical solution is to disable the offending
   27.13  \isa{split_if} as shown in the section on case splits in
   27.14  \S\ref{sec:SimpFeatures}.
   27.15  However, we do not recommend this because it means you will often have to
    28.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Sun Apr 23 11:41:45 2000 +0200
    28.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Tue Apr 25 08:09:10 2000 +0200
    28.3 @@ -6,8 +6,8 @@
    28.4  When a function is defined via \isacommand{recdef}, Isabelle tries to prove
    28.5  its termination with the help of the user-supplied measure.  All of the above
    28.6  examples are simple enough that Isabelle can prove automatically that the
    28.7 -measure of the argument goes down in each recursive call. In that case
    28.8 -$f$.\isa{simps} contains the defining equations (or variants derived from
    28.9 +measure of the argument goes down in each recursive call. As a result,
   28.10 +\isa{$f$.simps} will contain the defining equations (or variants derived from
   28.11  them) as theorems. For example, look (via \isacommand{thm}) at
   28.12  \isa{sep.simps} and \isa{sep1.simps} to see that they define the same
   28.13  function. What is more, those equations are automatically declared as
   28.14 @@ -39,8 +39,8 @@
   28.15  apply(arith).;
   28.16  
   28.17  text{*\noindent
   28.18 -Because \isacommand{recdef}'s the termination prover involves simplification,
   28.19 -we have declared our lemma a simplification rule. Therefore our second
   28.20 +Because \isacommand{recdef}'s termination prover involves simplification,
   28.21 +we have turned our lemma into a simplification rule. Therefore our second
   28.22  attempt to define our function will automatically take it into account:
   28.23  *}
   28.24  
    29.1 --- a/doc-src/TutorialI/ToyList/ToyList.thy	Sun Apr 23 11:41:45 2000 +0200
    29.2 +++ b/doc-src/TutorialI/ToyList/ToyList.thy	Tue Apr 25 08:09:10 2000 +0200
    29.3 @@ -1,10 +1,10 @@
    29.4  theory ToyList = PreList:
    29.5  
    29.6  text{*\noindent
    29.7 -HOL already has a predefined theory of lists called \texttt{List} ---
    29.8 -\texttt{ToyList} is merely a small fragment of it chosen as an example. In
    29.9 +HOL already has a predefined theory of lists called \isa{List} ---
   29.10 +\isa{ToyList} is merely a small fragment of it chosen as an example. In
   29.11  contrast to what is recommended in \S\ref{sec:Basic:Theories},
   29.12 -\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a
   29.13 +\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
   29.14  theory that contains pretty much everything but lists, thus avoiding
   29.15  ambiguities caused by defining lists twice.
   29.16  *}
   29.17 @@ -31,7 +31,7 @@
   29.18  
   29.19  \begin{warn}
   29.20    Syntax annotations are a powerful but completely optional feature. You
   29.21 -  could drop them from theory \texttt{ToyList} and go back to the identifiers
   29.22 +  could drop them from theory \isa{ToyList} and go back to the identifiers
   29.23    \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
   29.24    that their syntax is highly customized. We recommend that novices should
   29.25    not use syntax annotations in their own theories.
   29.26 @@ -67,7 +67,7 @@
   29.27  \isa{app} appends two lists and \isa{rev} reverses a list.  The keyword
   29.28  \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
   29.29  particularly primitive kind where each recursive call peels off a datatype
   29.30 -constructor from one of the arguments (see \S\ref{sec:datatype}).  Thus the
   29.31 +constructor from one of the arguments.  Thus the
   29.32  recursion always terminates, i.e.\ the function is \bfindex{total}.
   29.33  
   29.34  The termination requirement is absolutely essential in HOL, a logic of total
   29.35 @@ -103,7 +103,7 @@
   29.36  
   29.37  text{*\noindent
   29.38  When Isabelle prints a syntax error message, it refers to the HOL syntax as
   29.39 -the \bfindex{inner syntax}.
   29.40 +the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
   29.41  
   29.42  
   29.43  \section{An introductory proof}
   29.44 @@ -122,7 +122,7 @@
   29.45  
   29.46  theorem rev_rev [simp]: "rev(rev xs) = xs";
   29.47  
   29.48 -txt{*\noindent\index{*theorem|bold}\index{*simp (attribute)|bold}
   29.49 +txt{*\index{*theorem|bold}\index{*simp (attribute)|bold}
   29.50  \begin{itemize}
   29.51  \item
   29.52  establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
   29.53 @@ -220,8 +220,8 @@
   29.54  text{*
   29.55  \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
   29.56  
   29.57 -After abandoning the above proof attempt (at the shell level type
   29.58 -\isa{oops}) we start a new proof:
   29.59 +After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
   29.60 +\isacommand{oops}) we start a new proof:
   29.61  *}
   29.62  
   29.63  lemma rev_app [simp]: "rev(xs @ ys) = (rev ys) @ (rev xs)";
   29.64 @@ -232,7 +232,6 @@
   29.65  \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
   29.66  interchangeably.
   29.67  
   29.68 -%FIXME indent!
   29.69  There are two variables that we could induct on: \isa{xs} and
   29.70  \isa{ys}. Because \isa{\at} is defined by recursion on
   29.71  the first argument, \isa{xs} is the correct one:
   29.72 @@ -251,9 +250,9 @@
   29.73  ~1.~rev~ys~=~rev~ys~@~[]\isanewline
   29.74  ~2. \dots
   29.75  \end{isabellepar}%
   29.76 -We need to cancel this proof attempt and prove another simple lemma first.
   29.77 -In the future the step of cancelling an incomplete proof before embarking on
   29.78 -the proof of a lemma often remains implicit.
   29.79 +Again, we need to abandon this proof attempt and prove another simple lemma first.
   29.80 +In the future the step of abandoning an incomplete proof before embarking on
   29.81 +the proof of a lemma usually remains implicit.
   29.82  *}
   29.83  (*<*)
   29.84  oops
    30.1 --- a/doc-src/TutorialI/ToyList/document/ToyList.tex	Sun Apr 23 11:41:45 2000 +0200
    30.2 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex	Tue Apr 25 08:09:10 2000 +0200
    30.3 @@ -2,10 +2,10 @@
    30.4  \isacommand{theory}~ToyList~=~PreList:%
    30.5  \begin{isamarkuptext}%
    30.6  \noindent
    30.7 -HOL already has a predefined theory of lists called \texttt{List} ---
    30.8 -\texttt{ToyList} is merely a small fragment of it chosen as an example. In
    30.9 +HOL already has a predefined theory of lists called \isa{List} ---
   30.10 +\isa{ToyList} is merely a small fragment of it chosen as an example. In
   30.11  contrast to what is recommended in \S\ref{sec:Basic:Theories},
   30.12 -\texttt{ToyList} is not based on \texttt{Main} but on \texttt{PreList}, a
   30.13 +\isa{ToyList} is not based on \isa{Main} but on \isa{PreList}, a
   30.14  theory that contains pretty much everything but lists, thus avoiding
   30.15  ambiguities caused by defining lists twice.%
   30.16  \end{isamarkuptext}%
   30.17 @@ -31,7 +31,7 @@
   30.18  
   30.19  \begin{warn}
   30.20    Syntax annotations are a powerful but completely optional feature. You
   30.21 -  could drop them from theory \texttt{ToyList} and go back to the identifiers
   30.22 +  could drop them from theory \isa{ToyList} and go back to the identifiers
   30.23    \isa{Nil} and \isa{Cons}. However, lists are such a central datatype
   30.24    that their syntax is highly customized. We recommend that novices should
   30.25    not use syntax annotations in their own theories.
   30.26 @@ -63,7 +63,7 @@
   30.27  \isa{app} appends two lists and \isa{rev} reverses a list.  The keyword
   30.28  \isacommand{primrec}\index{*primrec} indicates that the recursion is of a
   30.29  particularly primitive kind where each recursive call peels off a datatype
   30.30 -constructor from one of the arguments (see \S\ref{sec:datatype}).  Thus the
   30.31 +constructor from one of the arguments.  Thus the
   30.32  recursion always terminates, i.e.\ the function is \bfindex{total}.
   30.33  
   30.34  The termination requirement is absolutely essential in HOL, a logic of total
   30.35 @@ -98,7 +98,7 @@
   30.36  \begin{isamarkuptext}%
   30.37  \noindent
   30.38  When Isabelle prints a syntax error message, it refers to the HOL syntax as
   30.39 -the \bfindex{inner syntax}.
   30.40 +the \bfindex{inner syntax} and the enclosing theory language as the \bfindex{outer syntax}.
   30.41  
   30.42  
   30.43  \section{An introductory proof}
   30.44 @@ -116,7 +116,7 @@
   30.45  \end{isamarkuptext}%
   30.46  \isacommand{theorem}~rev\_rev~[simp]:~{"}rev(rev~xs)~=~xs{"}%
   30.47  \begin{isamarkuptxt}%
   30.48 -\noindent\index{*theorem|bold}\index{*simp (attribute)|bold}
   30.49 +\index{*theorem|bold}\index{*simp (attribute)|bold}
   30.50  \begin{itemize}
   30.51  \item
   30.52  establishes a new theorem to be proved, namely \isa{rev(rev xs) = xs},
   30.53 @@ -209,8 +209,8 @@
   30.54  \begin{isamarkuptext}%
   30.55  \subsubsection*{First lemma: \texttt{rev(xs \at~ys) = (rev ys) \at~(rev xs)}}
   30.56  
   30.57 -After abandoning the above proof attempt (at the shell level type
   30.58 -\isa{oops}) we start a new proof:%
   30.59 +After abandoning the above proof attempt\indexbold{abandon proof} (at the shell level type
   30.60 +\isacommand{oops}) we start a new proof:%
   30.61  \end{isamarkuptext}%
   30.62  \isacommand{lemma}~rev\_app~[simp]:~{"}rev(xs~@~ys)~=~(rev~ys)~@~(rev~xs){"}%
   30.63  \begin{isamarkuptxt}%
   30.64 @@ -220,7 +220,6 @@
   30.65  \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much
   30.66  interchangeably.
   30.67  
   30.68 -%FIXME indent!
   30.69  There are two variables that we could induct on: \isa{xs} and
   30.70  \isa{ys}. Because \isa{\at} is defined by recursion on
   30.71  the first argument, \isa{xs} is the correct one:%
   30.72 @@ -236,9 +235,9 @@
   30.73  ~1.~rev~ys~=~rev~ys~@~[]\isanewline
   30.74  ~2. \dots
   30.75  \end{isabellepar}%
   30.76 -We need to cancel this proof attempt and prove another simple lemma first.
   30.77 -In the future the step of cancelling an incomplete proof before embarking on
   30.78 -the proof of a lemma often remains implicit.%
   30.79 +Again, we need to abandon this proof attempt and prove another simple lemma first.
   30.80 +In the future the step of abandoning an incomplete proof before embarking on
   30.81 +the proof of a lemma usually remains implicit.%
   30.82  \end{isamarkuptxt}%
   30.83  %
   30.84  \begin{isamarkuptext}%
    31.1 --- a/doc-src/TutorialI/Trie/Option2.thy	Sun Apr 23 11:41:45 2000 +0200
    31.2 +++ b/doc-src/TutorialI/Trie/Option2.thy	Tue Apr 25 08:09:10 2000 +0200
    31.3 @@ -2,8 +2,7 @@
    31.4  theory Option2 = Main:;
    31.5  (*>*)
    31.6  
    31.7 -datatype 'a option = None | Some 'a
    31.8 -
    31.9 +datatype 'a option = None | Some 'a;
   31.10  (*<*)
   31.11  end
   31.12  (*>*)
    32.1 --- a/doc-src/TutorialI/Trie/Trie.thy	Sun Apr 23 11:41:45 2000 +0200
    32.2 +++ b/doc-src/TutorialI/Trie/Trie.thy	Tue Apr 25 08:09:10 2000 +0200
    32.3 @@ -1,7 +1,6 @@
    32.4  (*<*)
    32.5  theory Trie = Main:;
    32.6  (*>*)
    32.7 -
    32.8  text{*
    32.9  To minimize running time, each node of a trie should contain an array that maps
   32.10  letters to subtries. We have chosen a (sometimes) more space efficient
   32.11 @@ -53,7 +52,7 @@
   32.12  *}
   32.13  
   32.14  lemma [simp]: "lookup (Trie None []) as = None";
   32.15 -apply(cases "as", auto).;
   32.16 +apply(case_tac as, auto).;
   32.17  
   32.18  text{*
   32.19  Things begin to get interesting with the definition of an update function
   32.20 @@ -107,7 +106,7 @@
   32.21  The start of the proof is completely conventional:
   32.22  *}
   32.23  
   32.24 -apply(induct_tac "as", auto);
   32.25 +apply(induct_tac as, auto);
   32.26  
   32.27  txt{*\noindent
   32.28  Unfortunately, this time we are left with three intimidating looking subgoals:
   32.29 @@ -127,8 +126,8 @@
   32.30  text{*\noindent
   32.31  Both \isaindex{case_tac} and \isaindex{induct_tac}
   32.32  take an optional first argument that specifies the range of subgoals they are
   32.33 -applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual
   32.34 -subgoal number are also allowed.
   32.35 +applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual
   32.36 +subgoal numbers are also allowed.
   32.37  
   32.38  This proof may look surprisingly straightforward. However, note that this
   32.39  comes at a cost: the proof script is unreadable because the
    33.1 --- a/doc-src/TutorialI/Trie/document/Option2.tex	Sun Apr 23 11:41:45 2000 +0200
    33.2 +++ b/doc-src/TutorialI/Trie/document/Option2.tex	Tue Apr 25 08:09:10 2000 +0200
    33.3 @@ -1,4 +1,3 @@
    33.4  \begin{isabelle}%
    33.5  \isanewline
    33.6 -\isacommand{datatype}~'a~option~=~None~|~Some~'a\isanewline
    33.7 -\end{isabelle}%
    33.8 +\isacommand{datatype}~'a~option~=~None~|~Some~'a\end{isabelle}%
    34.1 --- a/doc-src/TutorialI/Trie/document/Trie.tex	Sun Apr 23 11:41:45 2000 +0200
    34.2 +++ b/doc-src/TutorialI/Trie/document/Trie.tex	Tue Apr 25 08:09:10 2000 +0200
    34.3 @@ -44,7 +44,7 @@
    34.4  distinguishes the two cases whether the search string is empty or not:%
    34.5  \end{isamarkuptext}%
    34.6  \isacommand{lemma}~[simp]:~{"}lookup~(Trie~None~[])~as~=~None{"}\isanewline
    34.7 -\isacommand{apply}(cases~{"}as{"},~auto)\isacommand{.}%
    34.8 +\isacommand{apply}(case\_tac~as,~auto)\isacommand{.}%
    34.9  \begin{isamarkuptext}%
   34.10  Things begin to get interesting with the definition of an update function
   34.11  that adds a new (string,value) pair to a trie, overwriting the old value
   34.12 @@ -93,7 +93,7 @@
   34.13  \isa{as} is instantiated.
   34.14  The start of the proof is completely conventional:%
   34.15  \end{isamarkuptxt}%
   34.16 -\isacommand{apply}(induct\_tac~{"}as{"},~auto)%
   34.17 +\isacommand{apply}(induct\_tac~as,~auto)%
   34.18  \begin{isamarkuptxt}%
   34.19  \noindent
   34.20  Unfortunately, this time we are left with three intimidating looking subgoals:
   34.21 @@ -112,8 +112,8 @@
   34.22  \noindent
   34.23  Both \isaindex{case_tac} and \isaindex{induct_tac}
   34.24  take an optional first argument that specifies the range of subgoals they are
   34.25 -applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]}. Individual
   34.26 -subgoal number are also allowed.
   34.27 +applied to, where \isa{!} means all subgoals, i.e.\ \isa{[1-3]} in our case. Individual
   34.28 +subgoal numbers are also allowed.
   34.29  
   34.30  This proof may look surprisingly straightforward. However, note that this
   34.31  comes at a cost: the proof script is unreadable because the
    35.1 --- a/doc-src/TutorialI/appendix.tex	Sun Apr 23 11:41:45 2000 +0200
    35.2 +++ b/doc-src/TutorialI/appendix.tex	Tue Apr 25 08:09:10 2000 +0200
    35.3 @@ -80,7 +80,7 @@
    35.4  \end{center}
    35.5  \caption{Mathematical symbols and their ASCII-equivalents}
    35.6  \label{fig:ascii}
    35.7 -\end{figure}
    35.8 +\end{figure}\indexbold{ASCII symbols}
    35.9  
   35.10  \begin{figure}[htbp]
   35.11  \begin{center}
    36.1 --- a/doc-src/TutorialI/basics.tex	Sun Apr 23 11:41:45 2000 +0200
    36.2 +++ b/doc-src/TutorialI/basics.tex	Tue Apr 25 08:09:10 2000 +0200
    36.3 @@ -48,13 +48,13 @@
    36.4  where \texttt{B}$@1$, \dots, \texttt{B}$@n$ are the names of existing
    36.5  theories that \texttt{T} is based on and \texttt{\textit{declarations,
    36.6      definitions, and proofs}} represents the newly introduced concepts
    36.7 -(types, functions etc) and proofs about them. The \texttt{B}$@i$ are the
    36.8 +(types, functions etc.) and proofs about them. The \texttt{B}$@i$ are the
    36.9  direct \textbf{parent theories}\indexbold{parent theory} of \texttt{T}.
   36.10  Everything defined in the parent theories (and their parents \dots) is
   36.11  automatically visible. To avoid name clashes, identifiers can be
   36.12  \textbf{qualified} by theory names as in \texttt{T.f} and
   36.13  \texttt{B.f}.\indexbold{identifier!qualified} Each theory \texttt{T} must
   36.14 -reside in a \indexbold{theory file} named \texttt{T.thy}.
   36.15 +reside in a \bfindex{theory file} named \texttt{T.thy}.
   36.16  
   36.17  This tutorial is concerned with introducing you to the different linguistic
   36.18  constructs that can fill \textit{\texttt{declarations, definitions, and
   36.19 @@ -74,59 +74,33 @@
   36.20  \end{warn}
   36.21  
   36.22  
   36.23 -\section{Interaction and interfaces}
   36.24 -
   36.25 -Interaction with Isabelle can either occur at the shell level or through more
   36.26 -advanced interfaces. To keep the tutorial independent of the interface we
   36.27 -have phrased the description of the intraction in a neutral language. For
   36.28 -example, the phrase ``to cancel a proof'' means to type \texttt{oops} at the
   36.29 -shell level, which is explained the first time the phrase is used. Other
   36.30 -interfaces perform the same act by cursor movements and/or mouse clicks.
   36.31 -Although shell-based interaction is quite feasible for the kind of proof
   36.32 -scripts currently presented in this tutorial, the recommended interface for
   36.33 -Isabelle/Isar is the Emacs-based \bfindex{Proof
   36.34 -  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
   36.35 -
   36.36 -To improve readability some of the interfaces (including the shell level)
   36.37 -offer special fonts with mathematical symbols. Therefore the usual
   36.38 -mathematical symbols are used throughout the tutorial. Their
   36.39 -ASCII-equivalents are shown in figure~\ref{fig:ascii} in the appendix.
   36.40 -
   36.41 -Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
   36.42 -for example Proof General, require each command to be terminated by a
   36.43 -semicolon, whereas others, for example the shell level, do not. But even at
   36.44 -the shell level it is advisable to use semicolons to enforce that a command
   36.45 -is executed immediately; otherwise Isabelle may wait for the next keyword
   36.46 -before it knows that the command is complete. Note that for readibility
   36.47 -reasons we often drop the final semicolon in the text.
   36.48 -
   36.49 -
   36.50  \section{Types, terms and formulae}
   36.51  \label{sec:TypesTermsForms}
   36.52  \indexbold{type}
   36.53  
   36.54 -Embedded in the declarations of a theory are the types, terms and formulae of
   36.55 -HOL. HOL is a typed logic whose type system resembles that of functional
   36.56 -programming languages like ML or Haskell. Thus there are
   36.57 +Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed
   36.58 +logic whose type system resembles that of functional programming languages
   36.59 +like ML or Haskell. Thus there are
   36.60  \begin{description}
   36.61 -\item[base types,] in particular \ttindex{bool}, the type of truth values,
   36.62 -and \ttindex{nat}, the type of natural numbers.
   36.63 -\item[type constructors,] in particular \texttt{list}, the type of
   36.64 -lists, and \texttt{set}, the type of sets. Type constructors are written
   36.65 -postfix, e.g.\ \texttt{(nat)list} is the type of lists whose elements are
   36.66 +\item[base types,] in particular \isaindex{bool}, the type of truth values,
   36.67 +and \isaindex{nat}, the type of natural numbers.
   36.68 +\item[type constructors,] in particular \isaindex{list}, the type of
   36.69 +lists, and \isaindex{set}, the type of sets. Type constructors are written
   36.70 +postfix, e.g.\ \isa{(nat)list} is the type of lists whose elements are
   36.71  natural numbers. Parentheses around single arguments can be dropped (as in
   36.72 -\texttt{nat list}), multiple arguments are separated by commas (as in
   36.73 -\texttt{(bool,nat)foo}).
   36.74 +\isa{nat list}), multiple arguments are separated by commas (as in
   36.75 +\isa{(bool,nat)ty}).
   36.76  \item[function types,] denoted by \isasymFun\indexbold{$IsaFun@\isasymFun}.
   36.77 -  In HOL \isasymFun\ represents {\em total} functions only. As is customary,
   36.78 -  \texttt{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
   36.79 -  \texttt{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
   36.80 -  supports the notation \texttt{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
   36.81 -  which abbreviates \texttt{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
   36.82 +  In HOL \isasymFun\ represents \emph{total} functions only. As is customary,
   36.83 +  \isa{$\tau@1$ \isasymFun~$\tau@2$ \isasymFun~$\tau@3$} means
   36.84 +  \isa{$\tau@1$ \isasymFun~($\tau@2$ \isasymFun~$\tau@3$)}. Isabelle also
   36.85 +  supports the notation \isa{[$\tau@1,\dots,\tau@n$] \isasymFun~$\tau$}
   36.86 +  which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$
   36.87      \isasymFun~$\tau$}.
   36.88 -\item[type variables,] denoted by \texttt{'a}, \texttt{'b} etc, just like in
   36.89 -ML. They give rise to polymorphic types like \texttt{'a \isasymFun~'a}, the
   36.90 -type of the identity function.
   36.91 +\item[type variables,]\indexbold{type variable}\indexbold{variable!type}
   36.92 +  denoted by \isaindexbold{'a}, \isa{'b} etc., just like in ML. They give rise
   36.93 +  to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity
   36.94 +  function.
   36.95  \end{description}
   36.96  \begin{warn}
   36.97    Types are extremely important because they prevent us from writing
   36.98 @@ -145,77 +119,71 @@
   36.99  
  36.100  \noindent
  36.101  This can be reversed by \texttt{ML "reset show_types"}. Various other flags
  36.102 -can be set and reset in the same manner.\bfindex{flag!(re)setting}
  36.103 +can be set and reset in the same manner.\indexbold{flag!(re)setting}
  36.104  \end{warn}
  36.105  
  36.106  
  36.107  \textbf{Terms}\indexbold{term} are formed as in functional programming by
  36.108 -applying functions to arguments. If \texttt{f} is a function of type
  36.109 -\texttt{$\tau@1$ \isasymFun~$\tau@2$} and \texttt{t} is a term of type
  36.110 -$\tau@1$ then \texttt{f~t} is a term of type $\tau@2$. HOL also supports
  36.111 -infix functions like \texttt{+} and some basic constructs from functional
  36.112 +applying functions to arguments. If \isa{f} is a function of type
  36.113 +\isa{$\tau@1$ \isasymFun~$\tau@2$} and \isa{t} is a term of type
  36.114 +$\tau@1$ then \isa{f~t} is a term of type $\tau@2$. HOL also supports
  36.115 +infix functions like \isa{+} and some basic constructs from functional
  36.116  programming:
  36.117  \begin{description}
  36.118 -\item[\texttt{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
  36.119 +\item[\isa{if $b$ then $t@1$ else $t@2$}]\indexbold{*if}
  36.120  means what you think it means and requires that
  36.121 -$b$ is of type \texttt{bool} and $t@1$ and $t@2$ are of the same type.
  36.122 -\item[\texttt{let $x$ = $t$ in $u$}]\indexbold{*let}
  36.123 +$b$ is of type \isa{bool} and $t@1$ and $t@2$ are of the same type.
  36.124 +\item[\isa{let $x$ = $t$ in $u$}]\indexbold{*let}
  36.125  is equivalent to $u$ where all occurrences of $x$ have been replaced by
  36.126  $t$. For example,
  36.127 -\texttt{let x = 0 in x+x} means \texttt{0+0}. Multiple bindings are separated
  36.128 -by semicolons: \texttt{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
  36.129 -\item[\texttt{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
  36.130 +\isa{let x = 0 in x+x} is equivalent to \isa{0+0}. Multiple bindings are separated
  36.131 +by semicolons: \isa{let $x@1$ = $t@1$; \dots; $x@n$ = $t@n$ in $u$}.
  36.132 +\item[\isa{case $e$ of $c@1$ \isasymFun~$e@1$ |~\dots~| $c@n$ \isasymFun~$e@n$}]
  36.133  \indexbold{*case}
  36.134 -evaluates to $e@i$ if $e$ is of the form
  36.135 -$c@i$. See~\S\ref{sec:case-expressions} for details.
  36.136 +evaluates to $e@i$ if $e$ is of the form $c@i$.
  36.137  \end{description}
  36.138  
  36.139  Terms may also contain
  36.140  \isasymlambda-abstractions\indexbold{$Isalam@\isasymlambda}. For example,
  36.141 -\texttt{\isasymlambda{}x.~x+1} is the function that takes an argument
  36.142 -\texttt{x} and returns \texttt{x+1}. Instead of
  36.143 -\texttt{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.}~$t$ we can write
  36.144 -\texttt{\isasymlambda{}x~y~z.}~$t$.
  36.145 +\isa{\isasymlambda{}x.~x+1} is the function that takes an argument \isa{x} and
  36.146 +returns \isa{x+1}. Instead of
  36.147 +\isa{\isasymlambda{}x.\isasymlambda{}y.\isasymlambda{}z.~$t$} we can write
  36.148 +\isa{\isasymlambda{}x~y~z.~$t$}.
  36.149  
  36.150 -\textbf{Formulae}\indexbold{formula}
  36.151 -are terms of type \texttt{bool}. There are the basic
  36.152 -constants \ttindexbold{True} and \ttindexbold{False} and the usual logical
  36.153 -connectives (in decreasing order of priority):
  36.154 -\indexboldpos{\isasymnot}{$HOL0not},
  36.155 -\indexboldpos{\isasymand}{$HOL0and},
  36.156 -\indexboldpos{\isasymor}{$HOL0or}, and
  36.157 -\indexboldpos{\isasymimp}{$HOL0imp},
  36.158 +\textbf{Formulae}\indexbold{formula} are terms of type \isaindexbold{bool}.
  36.159 +There are the basic constants \isaindexbold{True} and \isaindexbold{False} and
  36.160 +the usual logical connectives (in decreasing order of priority):
  36.161 +\indexboldpos{\isasymnot}{$HOL0not}, \indexboldpos{\isasymand}{$HOL0and},
  36.162 +\indexboldpos{\isasymor}{$HOL0or}, and \indexboldpos{\isasymimp}{$HOL0imp},
  36.163  all of which (except the unary \isasymnot) associate to the right. In
  36.164 -particular \texttt{A \isasymimp~B \isasymimp~C} means
  36.165 -\texttt{A \isasymimp~(B \isasymimp~C)} and is thus
  36.166 -logically equivalent with \texttt{A \isasymand~B \isasymimp~C}
  36.167 -(which is \texttt{(A \isasymand~B) \isasymimp~C}).
  36.168 +particular \isa{A \isasymimp~B \isasymimp~C} means \isa{A \isasymimp~(B
  36.169 +  \isasymimp~C)} and is thus logically equivalent to \isa{A \isasymand~B
  36.170 +  \isasymimp~C} (which is \isa{(A \isasymand~B) \isasymimp~C}).
  36.171  
  36.172  Equality is available in the form of the infix function
  36.173 -\texttt{=}\indexbold{$HOL0eq@\texttt{=}} of type \texttt{'a \isasymFun~'a
  36.174 -  \isasymFun~bool}. Thus \texttt{$t@1$ = $t@2$} is a formula provided $t@1$
  36.175 +\isa{=}\indexbold{$HOL0eq@\texttt{=}} of type \isa{'a \isasymFun~'a
  36.176 +  \isasymFun~bool}. Thus \isa{$t@1$ = $t@2$} is a formula provided $t@1$
  36.177  and $t@2$ are terms of the same type. In case $t@1$ and $t@2$ are of type
  36.178 -\texttt{bool}, \texttt{=} acts as if-and-only-if. The formula
  36.179 -$t@1$~\isasymnoteq~$t@2$ is merely an abbreviation for
  36.180 -\texttt{\isasymnot($t@1$ = $t@2$)}.
  36.181 +\isa{bool}, \isa{=} acts as if-and-only-if. The formula
  36.182 +\isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for
  36.183 +\isa{\isasymnot($t@1$ = $t@2$)}.
  36.184  
  36.185  The syntax for quantifiers is
  36.186 -\texttt{\isasymforall{}x.}~$P$\indexbold{$HOL0All@\isasymforall} and
  36.187 -\texttt{\isasymexists{}x.}~$P$\indexbold{$HOL0Ex@\isasymexists}.  There is
  36.188 -even \texttt{\isasymuniqex{}x.}~$P$\index{$HOL0ExU@\isasymuniqex|bold}, which
  36.189 -means that there exists exactly one \texttt{x} that satisfies $P$.
  36.190 -Nested quantifications can be abbreviated:
  36.191 -\texttt{\isasymforall{}x~y~z.}~$P$ means
  36.192 -\texttt{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.}~$P$.
  36.193 +\isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and
  36.194 +\isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}.  There is
  36.195 +even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which
  36.196 +means that there exists exactly one \isa{x} that satisfies \isa{$P$}.  Nested
  36.197 +quantifications can be abbreviated: \isa{\isasymforall{}x~y~z.~$P$} means
  36.198 +\isa{\isasymforall{}x.\isasymforall{}y.\isasymforall{}z.~$P$}.
  36.199  
  36.200  Despite type inference, it is sometimes necessary to attach explicit
  36.201 -\bfindex{type constraints} to a term.  The syntax is \texttt{$t$::$\tau$} as
  36.202 -in \texttt{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isalamtc} binds weakly
  36.203 -and should therefore be enclosed in parentheses: \texttt{x < y::nat} is
  36.204 -ill-typed because it is interpreted as \texttt{(x < y)::nat}. The main reason
  36.205 -for type constraints are overloaded functions like \texttt{+}, \texttt{*} and
  36.206 -\texttt{<}. (See \S\ref{sec:TypeClasses} for a full discussion of
  36.207 -overloading.)
  36.208 +\textbf{type constraints}\indexbold{type constraint} to a term.  The syntax is
  36.209 +\isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that
  36.210 +\ttindexboldpos{::}{$Isalamtc} binds weakly and should therefore be enclosed
  36.211 +in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as
  36.212 +\isa{(x < y)::nat}. The main reason for type constraints are overloaded
  36.213 +functions like \isa{+}, \isa{*} and \isa{<}. (See \S\ref{sec:TypeClasses} for
  36.214 +a full discussion of overloading.)
  36.215  
  36.216  \begin{warn}
  36.217  In general, HOL's concrete syntax tries to follow the conventions of
  36.218 @@ -234,33 +202,35 @@
  36.219  
  36.220  \begin{itemize}
  36.221  \item
  36.222 -Remember that \texttt{f t u} means \texttt{(f t) u} and not \texttt{f(t u)}!
  36.223 +Remember that \isa{f t u} means \isa{(f t) u} and not \isa{f(t u)}!
  36.224  \item
  36.225 -Isabelle allows infix functions like \texttt{+}. The prefix form of function
  36.226 -application binds more strongly than anything else and hence \texttt{f~x + y}
  36.227 -means \texttt{(f~x)~+~y} and not \texttt{f(x+y)}.
  36.228 +Isabelle allows infix functions like \isa{+}. The prefix form of function
  36.229 +application binds more strongly than anything else and hence \isa{f~x + y}
  36.230 +means \isa{(f~x)~+~y} and not \isa{f(x+y)}.
  36.231  \item Remember that in HOL if-and-only-if is expressed using equality.  But
  36.232    equality has a high priority, as befitting a relation, while if-and-only-if
  36.233 -  typically has the lowest priority.  Thus, \texttt{\isasymnot~\isasymnot~P =
  36.234 -    P} means \texttt{\isasymnot\isasymnot(P = P)} and not
  36.235 -  \texttt{(\isasymnot\isasymnot P) = P}. When using \texttt{=} to mean
  36.236 -  logical equivalence, enclose both operands in parentheses, as in \texttt{(A
  36.237 +  typically has the lowest priority.  Thus, \isa{\isasymnot~\isasymnot~P =
  36.238 +    P} means \isa{\isasymnot\isasymnot(P = P)} and not
  36.239 +  \isa{(\isasymnot\isasymnot P) = P}. When using \isa{=} to mean
  36.240 +  logical equivalence, enclose both operands in parentheses, as in \isa{(A
  36.241      \isasymand~B) = (B \isasymand~A)}.
  36.242  \item
  36.243  Constructs with an opening but without a closing delimiter bind very weakly
  36.244  and should therefore be enclosed in parentheses if they appear in subterms, as
  36.245 -in \texttt{f = (\isasymlambda{}x.~x)}. This includes \ttindex{if},
  36.246 -\ttindex{let}, \ttindex{case}, \isasymlambda, and quantifiers.
  36.247 +in \isa{f = (\isasymlambda{}x.~x)}. This includes \isaindex{if},
  36.248 +\isaindex{let}, \isaindex{case}, \isa{\isasymlambda}, and quantifiers.
  36.249  \item
  36.250 -Never write \texttt{\isasymlambda{}x.x} or \texttt{\isasymforall{}x.x=x}
  36.251 -because \texttt{x.x} is always read as a single qualified identifier that
  36.252 -refers to an item \texttt{x} in theory \texttt{x}. Write
  36.253 -\texttt{\isasymlambda{}x.~x} and \texttt{\isasymforall{}x.~x=x} instead.
  36.254 -\item Identifiers\indexbold{identifier} may contain \texttt{_} and \texttt{'}.
  36.255 +Never write \isa{\isasymlambda{}x.x} or \isa{\isasymforall{}x.x=x}
  36.256 +because \isa{x.x} is always read as a single qualified identifier that
  36.257 +refers to an item \isa{x} in theory \isa{x}. Write
  36.258 +\isa{\isasymlambda{}x.~x} and \isa{\isasymforall{}x.~x=x} instead.
  36.259 +\item Identifiers\indexbold{identifier} may contain \isa{_} and \isa{'}.
  36.260  \end{itemize}
  36.261  
  36.262 -Remember that ASCII-equivalents of all mathematical symbols are
  36.263 -given in figure~\ref{fig:ascii} in the appendix.
  36.264 +For the sake of readability the usual mathematical symbols are used throughout
  36.265 +the tutorial. Their ASCII-equivalents are shown in figure~\ref{fig:ascii} in
  36.266 +the appendix.
  36.267 +
  36.268  
  36.269  \section{Variables}
  36.270  \label{sec:variables}
  36.271 @@ -270,9 +240,9 @@
  36.272  variables are automatically renamed to avoid clashes with free variables. In
  36.273  addition, Isabelle has a third kind of variable, called a \bfindex{schematic
  36.274    variable}\indexbold{variable!schematic} or \bfindex{unknown}, which starts
  36.275 -with a \texttt{?}.  Logically, an unknown is a free variable. But it may be
  36.276 +with a \isa{?}.  Logically, an unknown is a free variable. But it may be
  36.277  instantiated by another term during the proof process. For example, the
  36.278 -mathematical theorem $x = x$ is represented in Isabelle as \texttt{?x = ?x},
  36.279 +mathematical theorem $x = x$ is represented in Isabelle as \isa{?x = ?x},
  36.280  which means that Isabelle can instantiate it arbitrarily. This is in contrast
  36.281  to ordinary variables, which remain fixed. The programming language Prolog
  36.282  calls unknowns {\em logical\/} variables.
  36.283 @@ -283,11 +253,37 @@
  36.284  indicates that Isabelle will automatically instantiate those unknowns
  36.285  suitably when the theorem is used in some other proof.
  36.286  \begin{warn}
  36.287 -  If you use \texttt{?}\index{$HOL0Ex@\texttt{?}} as an existential
  36.288 -  quantifier, it needs to be followed by a space. Otherwise \texttt{?x} is
  36.289 +  If you use \isa{?}\index{$HOL0Ex@\texttt{?}} as an existential
  36.290 +  quantifier, it needs to be followed by a space. Otherwise \isa{?x} is
  36.291    interpreted as a schematic variable.
  36.292  \end{warn}
  36.293  
  36.294 +\section{Interaction and interfaces}
  36.295 +
  36.296 +Interaction with Isabelle can either occur at the shell level or through more
  36.297 +advanced interfaces. To keep the tutorial independent of the interface we
  36.298 +have phrased the description of the intraction in a neutral language. For
  36.299 +example, the phrase ``to abandon a proof'' means to type \isacommand{oops} at the
  36.300 +shell level, which is explained the first time the phrase is used. Other
  36.301 +interfaces perform the same act by cursor movements and/or mouse clicks.
  36.302 +Although shell-based interaction is quite feasible for the kind of proof
  36.303 +scripts currently presented in this tutorial, the recommended interface for
  36.304 +Isabelle/Isar is the Emacs-based \bfindex{Proof
  36.305 +  General}~\cite{Aspinall:TACAS:2000,proofgeneral}.
  36.306 +
  36.307 +Some interfaces (including the shell level) offer special fonts with
  36.308 +mathematical symbols. For those that do not, remember that ASCII-equivalents
  36.309 +are shown in figure~\ref{fig:ascii} in the appendix.
  36.310 +
  36.311 +Finally, a word about semicolons.\indexbold{$Isar@\texttt{;}} Some interfaces,
  36.312 +for example Proof General, require each command to be terminated by a
  36.313 +semicolon, whereas others, for example the shell level, do not. But even at
  36.314 +the shell level it is advisable to use semicolons to enforce that a command
  36.315 +is executed immediately; otherwise Isabelle may wait for the next keyword
  36.316 +before it knows that the command is complete. Note that for readibility
  36.317 +reasons we often drop the final semicolon in the text.
  36.318 +
  36.319 +
  36.320  \section{Getting started}
  36.321  
  36.322  Assuming you have installed Isabelle, you start it by typing \texttt{isabelle
  36.323 @@ -299,4 +295,4 @@
  36.324  create theory files.  While you are developing a theory, we recommend to
  36.325  type each command into the file first and then enter it into Isabelle by
  36.326  copy-and-paste, thus ensuring that you have a complete record of your theory.
  36.327 -As mentioned earlier, Proof General offers a much superior interface.
  36.328 +As mentioned above, Proof General offers a much superior interface.
    37.1 --- a/doc-src/TutorialI/fp.tex	Sun Apr 23 11:41:45 2000 +0200
    37.2 +++ b/doc-src/TutorialI/fp.tex	Tue Apr 25 08:09:10 2000 +0200
    37.3 @@ -116,14 +116,13 @@
    37.4    \isacommand{typ}\indexbold{*typ} \textit{string} reads and prints the given
    37.5    string as a type in the current context.
    37.6  \item[(Re)loading theories:] When you start your interaction you must open a
    37.7 -  named theory with the line
    37.8 -  \isacommand{theory}\texttt{~T~=}~\dots~\texttt{:}. Isabelle automatically
    37.9 -  loads all the required parent theories from their respective files (which
   37.10 -  may take a moment, unless the theories are already loaded and the files
   37.11 -  have not been modified). The only time when you need to load a theory by
   37.12 -  hand is when you simply want to check if it loads successfully without
   37.13 -  wanting to make use of the theory itself. This you can do by typing
   37.14 -  \isacommand{use\_thy}\indexbold{*use_thy}~\texttt{"T"}.
   37.15 +  named theory with the line \isa{\isacommand{theory}~T~=~\dots~:}. Isabelle
   37.16 +  automatically loads all the required parent theories from their respective
   37.17 +  files (which may take a moment, unless the theories are already loaded and
   37.18 +  the files have not been modified). The only time when you need to load a
   37.19 +  theory by hand is when you simply want to check if it loads successfully
   37.20 +  without wanting to make use of the theory itself. This you can do by typing
   37.21 +  \isa{\isacommand{use\_thy}\indexbold{*use_thy}~"T"}.
   37.22    
   37.23    If you suddenly discover that you need to modify a parent theory of your
   37.24    current theory you must first abandon your current theory (at the shell
   37.25 @@ -134,6 +133,9 @@
   37.26  \end{description}
   37.27  Further commands are found in the Isabelle/Isar Reference Manual.
   37.28  
   37.29 +We now examine Isabelle's functional programming constructs systematically,
   37.30 +starting with inductive datatypes.
   37.31 +
   37.32  
   37.33  \section{Datatypes}
   37.34  \label{sec:datatype}
   37.35 @@ -149,12 +151,12 @@
   37.36  
   37.37  Lists are one of the essential datatypes in computing. Readers of this
   37.38  tutorial and users of HOL need to be familiar with their basic operations.
   37.39 -Theory \texttt{ToyList} is only a small fragment of HOL's predefined theory
   37.40 -\texttt{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
   37.41 +Theory \isa{ToyList} is only a small fragment of HOL's predefined theory
   37.42 +\isa{List}\footnote{\url{http://isabelle.in.tum.de/library/HOL/List.html}}.
   37.43  The latter contains many further operations. For example, the functions
   37.44 -\isaindexbold{hd} (`head') and \isaindexbold{tl} (`tail') return the first
   37.45 +\isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first
   37.46  element and the remainder of a list. (However, pattern-matching is usually
   37.47 -preferable to \isa{hd} and \isa{tl}.)  Theory \texttt{List} also contains
   37.48 +preferable to \isa{hd} and \isa{tl}.)  Theory \isa{List} also contains
   37.49  more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates
   37.50  $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}.  In the rest of the tutorial we
   37.51  always use HOL's predefined lists.
   37.52 @@ -169,7 +171,7 @@
   37.53  C@1~\tau@{11}~\dots~\tau@{1k@1} ~\mid~ \dots ~\mid~
   37.54  C@m~\tau@{m1}~\dots~\tau@{mk@m}
   37.55  \]
   37.56 -where $\alpha@i$ are type variables (the parameters), $C@i$ are distinct
   37.57 +where $\alpha@i$ are distinct type variables (the parameters), $C@i$ are distinct
   37.58  constructor names and $\tau@{ij}$ are types; it is customary to capitalize
   37.59  the first letter in constructor names. There are a number of
   37.60  restrictions (such as that the type should not be empty) detailed
   37.61 @@ -192,7 +194,7 @@
   37.62  Isabelle immediately sees that $f$ terminates because one (fixed!) argument
   37.63  becomes smaller with every recursive call. There must be exactly one equation
   37.64  for each constructor.  Their order is immaterial.
   37.65 -A more general method for defining total recursive functions is explained in
   37.66 +A more general method for defining total recursive functions is introduced in
   37.67  \S\ref{sec:recdef}.
   37.68  
   37.69  \begin{exercise}
   37.70 @@ -276,6 +278,7 @@
   37.71  the constructs introduced above.
   37.72  
   37.73  \input{Ifexpr/document/Ifexpr.tex}
   37.74 +\medskip
   37.75  
   37.76  How does one come up with the required lemmas? Try to prove the main theorems
   37.77  without them and study carefully what \isa{auto} leaves unproved. This has
   37.78 @@ -368,7 +371,7 @@
   37.79  
   37.80  \subsection{Products}
   37.81  
   37.82 -HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \texttt{$\tau@1$ *
   37.83 +HOL also has pairs: \isa{($a@1$,$a@2$)} is of type \isa{$\tau@1$ *
   37.84    $\tau@2$} provided each $a@i$ is of type $\tau@i$. The components of a pair
   37.85  are extracted by \isa{fst} and \isa{snd}: \isa{fst($x$,$y$) = $x$} and
   37.86  \isa{snd($x$,$y$) = $y$}. Tuples are simulated by pairs nested to the right:
   37.87 @@ -411,7 +414,7 @@
   37.88  
   37.89  
   37.90  \subsection{Type synonyms}
   37.91 -\indexbold{type synonyms}
   37.92 +\indexbold{type synonym}
   37.93  
   37.94  Type synonyms are similar to those found in ML. Their syntax is fairly self
   37.95  explanatory:
   37.96 @@ -420,7 +423,6 @@
   37.97  
   37.98  Note that pattern-matching is not allowed, i.e.\ each definition must be of
   37.99  the form $f\,x@1\,\dots\,x@n~\isasymequiv~t$.
  37.100 -
  37.101  Section~\S\ref{sec:Simplification} explains how definitions are used
  37.102  in proofs.
  37.103  
  37.104 @@ -434,17 +436,17 @@
  37.105  \chapter{More Functional Programming}
  37.106  
  37.107  The purpose of this chapter is to deepen the reader's understanding of the
  37.108 -concepts encountered so far and to introduce an advanced forms of datatypes
  37.109 -and recursive functions. The first two sections give a structured
  37.110 -presentation of theorem proving by simplification
  37.111 -(\S\ref{sec:Simplification}) and discuss important heuristics for induction
  37.112 -(\S\ref{sec:InductionHeuristics}). They can be skipped by readers less
  37.113 -interested in proofs. They are followed by a case study, a compiler for
  37.114 -expressions (\S\ref{sec:ExprCompiler}). Advanced datatypes, including those
  37.115 -involving function spaces, are covered in \S\ref{sec:advanced-datatypes},
  37.116 -which closes with another case study, search trees (``tries'').  Finally we
  37.117 -introduce a very general form of recursive function definition which goes
  37.118 -well beyond what \isacommand{primrec} allows (\S\ref{sec:recdef}).
  37.119 +concepts encountered so far and to introduce advanced forms of datatypes and
  37.120 +recursive functions. The first two sections give a structured presentation of
  37.121 +theorem proving by simplification (\S\ref{sec:Simplification}) and discuss
  37.122 +important heuristics for induction (\S\ref{sec:InductionHeuristics}). They can
  37.123 +be skipped by readers less interested in proofs. They are followed by a case
  37.124 +study, a compiler for expressions (\S\ref{sec:ExprCompiler}). Advanced
  37.125 +datatypes, including those involving function spaces, are covered in
  37.126 +\S\ref{sec:advanced-datatypes}, which closes with another case study, search
  37.127 +trees (``tries'').  Finally we introduce \isacommand{recdef}, a very general
  37.128 +form of recursive function definition which goes well beyond what
  37.129 +\isacommand{primrec} allows (\S\ref{sec:recdef}).
  37.130  
  37.131  
  37.132  \section{Simplification}
  37.133 @@ -478,7 +480,7 @@
  37.134  (0#1#[]) @ []  \(\leadsto\)  0#((1#[]) @ [])  \(\leadsto\)  0#(1#([] @ []))  \(\leadsto\)  0#1#[]
  37.135  \end{ttbox}
  37.136  This is also known as \bfindex{term rewriting} and the equations are referred
  37.137 -to as \bfindex{rewrite rules}. This is more honest than ``simplification''
  37.138 +to as \bfindex{rewrite rules}. ``Rewriting'' is more honest than ``simplification''
  37.139  because the terms do not necessarily become simpler in the process.
  37.140  
  37.141  \subsubsection{Simplification rules}
  37.142 @@ -487,7 +489,7 @@
  37.143  To facilitate simplification, theorems can be declared to be simplification
  37.144  rules (with the help of the attribute \isa{[simp]}\index{*simp
  37.145    (attribute)}), in which case proofs by simplification make use of these
  37.146 -rules by default. In addition the constructs \isacommand{datatype} and
  37.147 +rules automatically. In addition the constructs \isacommand{datatype} and
  37.148  \isacommand{primrec} (and a few others) invisibly declare useful
  37.149  simplification rules. Explicit definitions are \emph{not} declared
  37.150  simplification rules automatically!
  37.151 @@ -502,14 +504,14 @@
  37.152  theorems [simp] = \(list of theorem names\);
  37.153  theorems [simp del] = \(list of theorem names\);
  37.154  \end{ttbox}
  37.155 -As a rule of thumb, rules that really simplify (like \isa{rev(rev xs) =
  37.156 +As a rule of thumb, equations that really simplify (like \isa{rev(rev xs) =
  37.157    xs} and \mbox{\isa{xs \at\ [] = xs}}) should be made simplification
  37.158  rules.  Those of a more specific nature (e.g.\ distributivity laws, which
  37.159  alter the structure of terms considerably) should only be used selectively,
  37.160  i.e.\ they should not be default simplification rules.  Conversely, it may
  37.161  also happen that a simplification rule needs to be disabled in certain
  37.162  proofs.  Frequent changes in the simplification status of a theorem may
  37.163 -indicates a badly designed theory.
  37.164 +indicate a badly designed theory.
  37.165  \begin{warn}
  37.166    Simplification may not terminate, for example if both $f(x) = g(x)$ and
  37.167    $g(x) = f(x)$ are simplification rules. It is the user's responsibility not
  37.168 @@ -568,7 +570,7 @@
  37.169  
  37.170  Proving a goal containing \isaindex{let}-expressions almost invariably
  37.171  requires the \isa{let}-con\-structs to be expanded at some point. Since
  37.172 -\isa{let}-\isa{in} is just syntactic sugar for a defined constant (called
  37.173 +\isa{let}-\isa{in} is just syntactic sugar for a predefined constant (called
  37.174  \isa{Let}), expanding \isa{let}-constructs means rewriting with
  37.175  \isa{Let_def}:
  37.176  
  37.177 @@ -600,7 +602,7 @@
  37.178  \index{arithmetic}
  37.179  
  37.180  The simplifier routinely solves a small class of linear arithmetic formulae
  37.181 -(over types \isa{nat} and \isa{int}): it only takes into account
  37.182 +(over type \isa{nat} and other numeric types): it only takes into account
  37.183  assumptions and conclusions that are (possibly negated) (in)equalities
  37.184  (\isa{=}, \isasymle, \isa{<}) and it only knows about addition. Thus
  37.185  
  37.186 @@ -673,7 +675,7 @@
  37.187  \end{quote}
  37.188  The heuristic is tricky to apply because it is not obvious that
  37.189  \isa{rev xs \at\ ys} is simpler than \isa{itrev xs ys}. But see what
  37.190 -happens if you try to prove the symmetric equation!
  37.191 +happens if you try to prove \isa{rev xs \at\ ys = itrev xs ys}!
  37.192  
  37.193  
  37.194  \section{Case study: compiling expressions}
  37.195 @@ -719,6 +721,7 @@
  37.196  right of a function arrow, but never on the left. Hence the above can of worms
  37.197  is ruled out but the following example of a potentially infinitely branching tree is
  37.198  accepted:
  37.199 +\smallskip
  37.200  
  37.201  \input{Datatype/document/Fundata.tex}
  37.202  \bigskip
  37.203 @@ -728,7 +731,7 @@
  37.204  \begin{ttbox}
  37.205  datatype lam = C (lam -> lam)
  37.206  \end{ttbox}
  37.207 -do indeed make sense (note the intentionally different arrow \isa{->}!).
  37.208 +do indeed make sense (note the intentionally different arrow \isa{->}).
  37.209  There is even a version of LCF on top of HOL, called
  37.210  HOLCF~\cite{MuellerNvOS99}.
  37.211  
  37.212 @@ -785,11 +788,11 @@
  37.213  Proper tries associate some value with each string. Since the
  37.214  information is stored only in the final node associated with the string, many
  37.215  nodes do not carry any value. This distinction is captured by the
  37.216 -following predefined datatype (from theory \texttt{Option}, which is a parent
  37.217 -of \texttt{Main}):
  37.218 +following predefined datatype (from theory \isa{Option}, which is a parent
  37.219 +of \isa{Main}):
  37.220 +\smallskip
  37.221  \input{Trie/document/Option2.tex}
  37.222 -\indexbold{*option}\indexbold{*None}\indexbold{*Some}
  37.223 -
  37.224 +\indexbold{*option}\indexbold{*None}\indexbold{*Some}%
  37.225  \input{Trie/document/Trie.tex}
  37.226  
  37.227  \begin{exercise}
    38.1 --- a/doc-src/TutorialI/isabelle.sty	Sun Apr 23 11:41:45 2000 +0200
    38.2 +++ b/doc-src/TutorialI/isabelle.sty	Tue Apr 25 08:09:10 2000 +0200
    38.3 @@ -19,6 +19,9 @@
    38.4  
    38.5  \newcommand{\isa}[1]{\emph{\isabelledefaultstyle\isabellestyle #1}}
    38.6  
    38.7 +\newenvironment{isabellequote}%
    38.8 +{\begin{quote}\begin{isabelle}\noindent}{\end{isabelle}\end{quote}}
    38.9 +
   38.10  \newcommand{\isanewline}{\mbox{}\\\mbox{}}
   38.11  
   38.12  \chardef\isabraceleft=`\{