author | nipkow |

Tue Apr 25 08:09:10 2000 +0200 (2000-04-25) | |

changeset 8771 | 026f37a86ea7 |

parent 8770 | bfab4d4b7516 |

child 8772 | ebb07113c4f7 |

*** empty log message ***

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=`\{