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