# HG changeset patch # User paulson # Date 978715977 -3600 # Node ID 9e888d60d3e5413b9d400eaa5952fa15a9d0f8d4 # Parent 65d18005d8020796c968e20427758deae900bebe minor edits to Chapters 1-3 diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Advanced/WFrec.thy --- a/doc-src/TutorialI/Advanced/WFrec.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Advanced/WFrec.thy Fri Jan 05 18:32:57 2001 +0100 @@ -79,7 +79,7 @@ by simp; text{*\noindent -and should have appended the following hint to our above definition: +and should have appended the following hint to our definition above: \indexbold{*recdef_wf} *} (*<*) diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Advanced/document/WFrec.tex --- a/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Advanced/document/WFrec.tex Fri Jan 05 18:32:57 2001 +0100 @@ -76,7 +76,7 @@ \isacommand{by}\ simp% \begin{isamarkuptext}% \noindent -and should have appended the following hint to our above definition: +and should have appended the following hint to our definition above: \indexbold{*recdef_wf}% \end{isamarkuptext}% {\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}wf{\isacharcolon}\ wf{\isacharunderscore}id{\isacharparenright}\end{isabellebody}% diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Advanced/document/simp.tex --- a/doc-src/TutorialI/Advanced/document/simp.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Advanced/document/simp.tex Fri Jan 05 18:32:57 2001 +0100 @@ -93,7 +93,7 @@ once they apply, they can be used forever. The simplifier is aware of this danger and treats permutative rules by means of a special strategy, called \bfindex{ordered rewriting}: a permutative rewrite -rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed +rule is only applied if the term becomes ``smaller'' (with respect to a fixed lexicographic ordering on terms). For example, commutativity rewrites \isa{b\ {\isacharplus}\ a} to \isa{a\ {\isacharplus}\ b}, but then stops because \isa{a\ {\isacharplus}\ b} is strictly smaller than \isa{b\ {\isacharplus}\ a}. Permutative rewrite rules can be turned into diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Advanced/simp.thy --- a/doc-src/TutorialI/Advanced/simp.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Advanced/simp.thy Fri Jan 05 18:32:57 2001 +0100 @@ -78,7 +78,7 @@ once they apply, they can be used forever. The simplifier is aware of this danger and treats permutative rules by means of a special strategy, called \bfindex{ordered rewriting}: a permutative rewrite -rule is only applied if the term becomes ``smaller'' (w.r.t.\ some fixed +rule is only applied if the term becomes ``smaller'' (with respect to a fixed lexicographic ordering on terms). For example, commutativity rewrites @{term"b+a"} to @{term"a+b"}, but then stops because @{term"a+b"} is strictly smaller than @{term"b+a"}. Permutative rewrite rules can be turned into diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/Base.thy --- a/doc-src/TutorialI/CTL/Base.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CTL/Base.thy Fri Jan 05 18:32:57 2001 +0100 @@ -4,9 +4,9 @@ text{*\label{sec:VMC} Model checking is a very popular technique for the verification of finite -state systems (implementations) w.r.t.\ temporal logic formulae +state systems (implementations) with respect to temporal logic formulae (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic -and this section shall explore them a little in HOL. This is done in two steps: first +and this section will explore them a little in HOL\@. This is done in two steps: first we consider a simple modal logic called propositional dynamic logic (PDL) which we then extend to the temporal logic CTL used in many real model checkers. In each case we give both a traditional semantics (@{text \}) and a diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/CTL.thy --- a/doc-src/TutorialI/CTL/CTL.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CTL/CTL.thy Fri Jan 05 18:32:57 2001 +0100 @@ -346,7 +346,7 @@ text{* -The above language is not quite CTL. The latter also includes an +The above language is not quite CTL\@. The latter also includes an until-operator @{term"EU f g"} with semantics ``there exist a path where @{term f} is true until @{term g} becomes true''. With the help of an auxiliary function diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/CTLind.thy --- a/doc-src/TutorialI/CTL/CTLind.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CTL/CTLind.thy Fri Jan 05 18:32:57 2001 +0100 @@ -7,7 +7,7 @@ some of the induction principles and heuristics discussed above and we want to show how inductive definitions can simplify proofs. In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a -model checker for CTL. In particular the proof of the +model checker for CTL\@. In particular the proof of the @{thm[source]infinity_lemma} on the way to @{thm[source]AF_lemma2} is not as simple as one might intuitively expect, due to the @{text SOME} operator involved. Below we give a simpler proof of @{thm[source]AF_lemma2} diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/document/Base.tex --- a/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/Base.tex Fri Jan 05 18:32:57 2001 +0100 @@ -8,9 +8,9 @@ \begin{isamarkuptext}% \label{sec:VMC} Model checking is a very popular technique for the verification of finite -state systems (implementations) w.r.t.\ temporal logic formulae +state systems (implementations) with respect to temporal logic formulae (specifications) \cite{ClarkeGP-book,Huth-Ryan-book}. Its foundations are completely set theoretic -and this section shall explore them a little in HOL. This is done in two steps: first +and this section will explore them a little in HOL\@. This is done in two steps: first we consider a simple modal logic called propositional dynamic logic (PDL) which we then extend to the temporal logic CTL used in many real model checkers. In each case we give both a traditional semantics (\isa{{\isasymTurnstile}}) and a diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/document/CTL.tex --- a/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTL.tex Fri Jan 05 18:32:57 2001 +0100 @@ -281,7 +281,7 @@ \isacommand{apply}{\isacharparenleft}auto\ simp\ add{\isacharcolon}\ EF{\isacharunderscore}lemma\ equalityI{\isacharbrackleft}OF\ AF{\isacharunderscore}lemma{\isadigit{1}}\ AF{\isacharunderscore}lemma{\isadigit{2}}{\isacharbrackright}{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptext}% -The above language is not quite CTL. The latter also includes an +The above language is not quite CTL\@. The latter also includes an until-operator \isa{EU\ f\ g} with semantics ``there exist a path where \isa{f} is true until \isa{g} becomes true''. With the help of an auxiliary function% diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CTL/document/CTLind.tex --- a/doc-src/TutorialI/CTL/document/CTLind.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CTL/document/CTLind.tex Fri Jan 05 18:32:57 2001 +0100 @@ -11,7 +11,7 @@ some of the induction principles and heuristics discussed above and we want to show how inductive definitions can simplify proofs. In \S\ref{sec:CTL} we gave a fairly involved proof of the correctness of a -model checker for CTL. In particular the proof of the +model checker for CTL\@. In particular the proof of the \isa{infinity{\isacharunderscore}lemma} on the way to \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} is not as simple as one might intuitively expect, due to the \isa{SOME} operator involved. Below we give a simpler proof of \isa{AF{\isacharunderscore}lemma{\isadigit{2}}} diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CodeGen/CodeGen.thy --- a/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CodeGen/CodeGen.thy Fri Jan 05 18:32:57 2001 +0100 @@ -6,7 +6,7 @@ text{*\label{sec:ExprCompiler} The task is to develop a compiler from a generic type of expressions (built -up from variables, constants and binary operations) to a stack machine. This +from variables, constants and binary operations) to a stack machine. This generic type of expressions is a generalization of the boolean expressions in \S\ref{sec:boolex}. This time we do not commit ourselves to a particular type of variables or values but make them type parameters. Neither is there @@ -23,7 +23,7 @@ The three constructors represent constants, variables and the application of a binary operation to two subexpressions. -The value of an expression w.r.t.\ an environment that maps variables to +The value of an expression with respect to an environment that maps variables to values is easily defined: *} @@ -35,7 +35,7 @@ text{* The stack machine has three instructions: load a constant value onto the -stack, load the contents of a certain address onto the stack, and apply a +stack, load the contents of an address onto the stack, and apply a binary operation to the two topmost elements of the stack, replacing them by the result. As for @{text"expr"}, addresses and values are type parameters: *} @@ -66,12 +66,12 @@ return the first element and the remainder of a list. Because all functions are total, @{term"hd"} is defined even for the empty list, although we do not know what the result is. Thus our model of the -machine always terminates properly, although the above definition does not +machine always terminates properly, although the definition above does not tell us much about the result in situations where @{term"Apply"} was executed with fewer than two elements on the stack. The compiler is a function from expressions to a list of instructions. Its -definition is pretty much obvious: +definition is obvious: *} consts comp :: "('a,'v)expr \ ('a,'v)instr list"; diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/CodeGen/document/CodeGen.tex --- a/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/CodeGen/document/CodeGen.tex Fri Jan 05 18:32:57 2001 +0100 @@ -8,7 +8,7 @@ \begin{isamarkuptext}% \label{sec:ExprCompiler} The task is to develop a compiler from a generic type of expressions (built -up from variables, constants and binary operations) to a stack machine. This +from variables, constants and binary operations) to a stack machine. This generic type of expressions is a generalization of the boolean expressions in \S\ref{sec:boolex}. This time we do not commit ourselves to a particular type of variables or values but make them type parameters. Neither is there @@ -24,7 +24,7 @@ The three constructors represent constants, variables and the application of a binary operation to two subexpressions. -The value of an expression w.r.t.\ an environment that maps variables to +The value of an expression with respect to an environment that maps variables to values is easily defined:% \end{isamarkuptext}% \isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}v{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}v{\isachardoublequote}\isanewline @@ -34,7 +34,7 @@ {\isachardoublequote}value\ {\isacharparenleft}Bex\ f\ e{\isadigit{1}}\ e{\isadigit{2}}{\isacharparenright}\ env\ {\isacharequal}\ f\ {\isacharparenleft}value\ e{\isadigit{1}}\ env{\isacharparenright}\ {\isacharparenleft}value\ e{\isadigit{2}}\ env{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% The stack machine has three instructions: load a constant value onto the -stack, load the contents of a certain address onto the stack, and apply a +stack, load the contents of an address onto the stack, and apply a binary operation to the two topmost elements of the stack, replacing them by the result. As for \isa{expr}, addresses and values are type parameters:% \end{isamarkuptext}% @@ -62,12 +62,12 @@ return the first element and the remainder of a list. Because all functions are total, \isa{hd} is defined even for the empty list, although we do not know what the result is. Thus our model of the -machine always terminates properly, although the above definition does not +machine always terminates properly, although the definition above does not tell us much about the result in situations where \isa{Apply} was executed with fewer than two elements on the stack. The compiler is a function from expressions to a list of instructions. Its -definition is pretty much obvious:% +definition is obvious:% \end{isamarkuptext}% \isacommand{consts}\ comp\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}expr\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}v{\isacharparenright}instr\ list{\isachardoublequote}\isanewline \isacommand{primrec}\isanewline diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Datatype/Fundata.thy --- a/doc-src/TutorialI/Datatype/Fundata.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Datatype/Fundata.thy Fri Jan 05 18:32:57 2001 +0100 @@ -32,7 +32,7 @@ Isabelle because the termination proof is not as obvious since @{term"map_bt"} is only partially applied. -The following lemma has a canonical proof *} +The following lemma has a canonical proof: *} lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; apply(induct_tac T, simp_all) @@ -40,8 +40,9 @@ (*<*)lemma "map_bt (g o f) T = map_bt g (map_bt f T)"; apply(induct_tac T, rename_tac[2] F)(*>*) txt{*\noindent -but it is worth taking a look at the proof state after the induction step -to understand what the presence of the function type entails: +It is worth taking a look at the proof state after the induction step +to understand what the presence of the function type entails. +Notice the quantified induction hypothesis: @{subgoals[display,indent=0]} *} (*<*) diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Datatype/Nested.thy --- a/doc-src/TutorialI/Datatype/Nested.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Datatype/Nested.thy Fri Jan 05 18:32:57 2001 +0100 @@ -89,13 +89,13 @@ term. Prove that @{prop"trev(trev t) = t"}. \end{exercise} -The experienced functional programmer may feel that our above definition of -@{term subst} is unnecessarily complicated in that @{term substs} is -completely unnecessary. The @{term App}-case can be defined directly as +The experienced functional programmer may feel that our definition of +@{term subst} is too complicated in that @{term substs} is +unnecessary. The @{term App}-case can be defined directly as @{term[display]"subst s (App f ts) = App f (map (subst s) ts)"} where @{term"map"} is the standard list function such that @{text"map f [x1,...,xn] = [f x1,...,f xn]"}. This is true, but Isabelle -insists on the above fixed format. Fortunately, we can easily \emph{prove} +insists on the conjunctive format. Fortunately, we can easily \emph{prove} that the suggested equation holds: *} @@ -116,8 +116,8 @@ about @{term map}. Unfortunately inductive proofs about type @{text term} are still awkward because they expect a conjunction. One could derive a new induction principle as well (see -\S\ref{sec:derive-ind}), but turns out to be simpler to define -functions by \isacommand{recdef} instead of \isacommand{primrec}. +\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec} +and to define functions with \isacommand{recdef} instead. The details are explained in \S\ref{sec:nested-recdef} below. Of course, you may also combine mutual and nested recursion. For example, diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Datatype/document/Fundata.tex --- a/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Datatype/document/Fundata.tex Fri Jan 05 18:32:57 2001 +0100 @@ -33,15 +33,16 @@ Isabelle because the termination proof is not as obvious since \isa{map{\isacharunderscore}bt} is only partially applied. -The following lemma has a canonical proof% +The following lemma has a canonical proof:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}map{\isacharunderscore}bt\ {\isacharparenleft}g\ o\ f{\isacharparenright}\ T\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ T{\isacharparenright}{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ T{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline \isacommand{done}% \begin{isamarkuptxt}% \noindent -but it is worth taking a look at the proof state after the induction step -to understand what the presence of the function type entails: +It is worth taking a look at the proof state after the induction step +to understand what the presence of the function type entails. +Notice the quantified induction hypothesis: \begin{isabelle}% \ {\isadigit{1}}{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ Tip\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ Tip{\isacharparenright}\isanewline \ {\isadigit{2}}{\isachardot}\ {\isasymAnd}a\ F{\isachardot}\ {\isasymforall}x{\isachardot}\ map{\isacharunderscore}bt\ {\isacharparenleft}g\ {\isasymcirc}\ f{\isacharparenright}\ {\isacharparenleft}F\ x{\isacharparenright}\ {\isacharequal}\ map{\isacharunderscore}bt\ g\ {\isacharparenleft}map{\isacharunderscore}bt\ f\ {\isacharparenleft}F\ x{\isacharparenright}{\isacharparenright}\ {\isasymLongrightarrow}\isanewline diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Datatype/document/Nested.tex --- a/doc-src/TutorialI/Datatype/document/Nested.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Datatype/document/Nested.tex Fri Jan 05 18:32:57 2001 +0100 @@ -87,15 +87,15 @@ term. Prove that \isa{trev\ {\isacharparenleft}trev\ t{\isacharparenright}\ {\isacharequal}\ t}. \end{exercise} -The experienced functional programmer may feel that our above definition of -\isa{subst} is unnecessarily complicated in that \isa{substs} is -completely unnecessary. The \isa{App}-case can be defined directly as +The experienced functional programmer may feel that our definition of +\isa{subst} is too complicated in that \isa{substs} is +unnecessary. The \isa{App}-case can be defined directly as \begin{isabelle}% \ \ \ \ \ subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}% \end{isabelle} where \isa{map} is the standard list function such that \isa{map\ f\ {\isacharbrackleft}x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}xn{\isacharbrackright}\ {\isacharequal}\ {\isacharbrackleft}f\ x{\isadigit{1}}{\isacharcomma}{\isachardot}{\isachardot}{\isachardot}{\isacharcomma}f\ xn{\isacharbrackright}}. This is true, but Isabelle -insists on the above fixed format. Fortunately, we can easily \emph{prove} +insists on the conjunctive format. Fortunately, we can easily \emph{prove} that the suggested equation holds:% \end{isamarkuptext}% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}subst\ s\ {\isacharparenleft}App\ f\ ts{\isacharparenright}\ {\isacharequal}\ App\ f\ {\isacharparenleft}map\ {\isacharparenleft}subst\ s{\isacharparenright}\ ts{\isacharparenright}{\isachardoublequote}\isanewline @@ -114,8 +114,8 @@ about \isa{map}. Unfortunately inductive proofs about type \isa{term} are still awkward because they expect a conjunction. One could derive a new induction principle as well (see -\S\ref{sec:derive-ind}), but turns out to be simpler to define -functions by \isacommand{recdef} instead of \isacommand{primrec}. +\S\ref{sec:derive-ind}), but simpler is to stop using \isacommand{primrec} +and to define functions with \isacommand{recdef} instead. The details are explained in \S\ref{sec:nested-recdef} below. Of course, you may also combine mutual and nested recursion. For example, diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Ifexpr/Ifexpr.thy --- a/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Ifexpr/Ifexpr.thy Fri Jan 05 18:32:57 2001 +0100 @@ -36,12 +36,12 @@ values: *} -consts value :: "boolex \\ (nat \\ bool) \\ bool"; +consts value :: "boolex \ (nat \ bool) \ bool"; primrec "value (Const b) env = b" "value (Var x) env = env x" -"value (Neg b) env = (\\ value b env)" -"value (And b c) env = (value b env \\ value c env)"; +"value (Neg b) env = (\ value b env)" +"value (And b c) env = (value b env \ value c env)"; text{*\noindent \subsubsection{If-expressions} @@ -58,7 +58,7 @@ The evaluation if If-expressions proceeds as for @{typ"boolex"}: *} -consts valif :: "ifex \\ (nat \\ bool) \\ bool"; +consts valif :: "ifex \ (nat \ bool) \ bool"; primrec "valif (CIF b) env = b" "valif (VIF x) env = env x" @@ -73,7 +73,7 @@ translate from @{typ"boolex"} into @{typ"ifex"}: *} -consts bool2if :: "boolex \\ ifex"; +consts bool2if :: "boolex \ ifex"; primrec "bool2if (Const b) = CIF b" "bool2if (Var x) = VIF x" @@ -107,13 +107,13 @@ primitive recursive functions perform this task: *} -consts normif :: "ifex \\ ifex \\ ifex \\ ifex"; +consts normif :: "ifex \ ifex \ ifex \ ifex"; primrec "normif (CIF b) t e = IF (CIF b) t e" "normif (VIF x) t e = IF (VIF x) t e" "normif (IF b t e) u f = normif b (normif t u f) (normif e u f)"; -consts norm :: "ifex \\ ifex"; +consts norm :: "ifex \ ifex"; primrec "norm (CIF b) = CIF b" "norm (VIF x) = VIF x" @@ -133,7 +133,7 @@ *} lemma [simp]: - "\\t e. valif (normif b t e) env = valif (IF b t e) env"; + "\t e. valif (normif b t e) env = valif (IF b t e) env"; (*<*) apply(induct_tac b); by(auto); @@ -150,19 +150,19 @@ the above sense? We define a function that tests If-expressions for normality *} -consts normal :: "ifex \\ bool"; +consts normal :: "ifex \ bool"; primrec "normal(CIF b) = True" "normal(VIF x) = True" -"normal(IF b t e) = (normal t \\ normal e \\ - (case b of CIF b \\ True | VIF x \\ True | IF x y z \\ False))"; +"normal(IF b t e) = (normal t \ normal e \ + (case b of CIF b \ True | VIF x \ True | IF x y z \ False))"; text{*\noindent and prove @{term"normal(norm b)"}. Of course, this requires a lemma about normality of @{term"normif"}: *} -lemma[simp]: "\\t e. normal(normif b t e) = (normal t \\ normal e)"; +lemma[simp]: "\t e. normal(normif b t e) = (normal t \ normal e)"; (*<*) apply(induct_tac b); by(auto); @@ -173,9 +173,9 @@ (*>*) text{*\medskip -How does one come up with the required lemmas? Try to prove the main theorems -without them and study carefully what @{text auto} leaves unproved. This has -to provide the clue. The necessity of universal quantification +How do we come up with the required lemmas? Try to prove the main theorems +without them and study carefully what @{text auto} leaves unproved. This +can provide the clue. The necessity of universal quantification (@{text"\t e"}) in the two lemmas is explained in \S\ref{sec:InductionHeuristics} diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Ifexpr/document/Ifexpr.tex --- a/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Ifexpr/document/Ifexpr.tex Fri Jan 05 18:32:57 2001 +0100 @@ -148,9 +148,9 @@ \isacommand{lemma}{\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \medskip -How does one come up with the required lemmas? Try to prove the main theorems -without them and study carefully what \isa{auto} leaves unproved. This has -to provide the clue. The necessity of universal quantification +How do we come up with the required lemmas? Try to prove the main theorems +without them and study carefully what \isa{auto} leaves unproved. This +can provide the clue. The necessity of universal quantification (\isa{{\isasymforall}t\ e}) in the two lemmas is explained in \S\ref{sec:InductionHeuristics} diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/Itrev.thy --- a/doc-src/TutorialI/Misc/Itrev.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/Itrev.thy Fri Jan 05 18:32:57 2001 +0100 @@ -64,7 +64,7 @@ @{subgoals[display,indent=0,margin=65]} Just as predicted above, the overall goal, and hence the induction hypothesis, is too weak to solve the induction step because of the fixed -@{term"[]"}. The corresponding heuristic: +argument, @{term"[]"}. This suggests a heuristic: \begin{quote} \emph{Generalize goals for induction by replacing constants by variables.} \end{quote} @@ -109,11 +109,13 @@ provability of the goal. Because it is not always required, and may even complicate matters in some cases, this heuristic is often not applied blindly. +The variables that require generalization are typically those that +change in recursive calls. In general, if you have tried the above heuristics and still find your induction does not go through, and no obvious lemma suggests itself, you may need to generalize your proposition even further. This requires insight into -the problem at hand and is beyond simple rules of thumb. In a nutshell: you +the problem at hand and is beyond simple rules of thumb. You will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} to learn about some advanced techniques for inductive proofs. diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/Tree.thy --- a/doc-src/TutorialI/Misc/Tree.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/Tree.thy Fri Jan 05 18:32:57 2001 +0100 @@ -8,14 +8,14 @@ datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*) -consts mirror :: "'a tree \\ 'a tree"; +consts mirror :: "'a tree \ 'a tree"; primrec "mirror Tip = Tip" "mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*) text{*\noindent and a function @{term"mirror"} that mirrors a binary tree -by swapping subtrees (recursively). Prove +by swapping subtrees recursively. Prove *} lemma mirror_mirror: "mirror(mirror t) = t"; diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/document/Itrev.tex --- a/doc-src/TutorialI/Misc/document/Itrev.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/Itrev.tex Fri Jan 05 18:32:57 2001 +0100 @@ -67,7 +67,7 @@ \end{isabelle} Just as predicted above, the overall goal, and hence the induction hypothesis, is too weak to solve the induction step because of the fixed -\isa{{\isacharbrackleft}{\isacharbrackright}}. The corresponding heuristic: +argument, \isa{{\isacharbrackleft}{\isacharbrackright}}. This suggests a heuristic: \begin{quote} \emph{Generalize goals for induction by replacing constants by variables.} \end{quote} @@ -111,11 +111,13 @@ provability of the goal. Because it is not always required, and may even complicate matters in some cases, this heuristic is often not applied blindly. +The variables that require generalization are typically those that +change in recursive calls. In general, if you have tried the above heuristics and still find your induction does not go through, and no obvious lemma suggests itself, you may need to generalize your proposition even further. This requires insight into -the problem at hand and is beyond simple rules of thumb. In a nutshell: you +the problem at hand and is beyond simple rules of thumb. You will need to be creative. Additionally, you can read \S\ref{sec:advanced-ind} to learn about some advanced techniques for inductive proofs. diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/document/Tree.tex --- a/doc-src/TutorialI/Misc/document/Tree.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/Tree.tex Fri Jan 05 18:32:57 2001 +0100 @@ -10,7 +10,7 @@ \begin{isamarkuptext}% \noindent and a function \isa{mirror} that mirrors a binary tree -by swapping subtrees (recursively). Prove% +by swapping subtrees recursively. Prove% \end{isamarkuptext}% \isacommand{lemma}\ mirror{\isacharunderscore}mirror{\isacharcolon}\ {\isachardoublequote}mirror{\isacharparenleft}mirror\ t{\isacharparenright}\ {\isacharequal}\ t{\isachardoublequote}% \begin{isamarkuptext}% diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/document/pairs.tex --- a/doc-src/TutorialI/Misc/document/pairs.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/pairs.tex Fri Jan 05 18:32:57 2001 +0100 @@ -24,9 +24,10 @@ Products, like type \isa{nat}, are datatypes, which means in particular that \isa{induct{\isacharunderscore}tac} and \isa{case{\isacharunderscore}tac} are applicable to terms of product type. +Both replace the term by tuple of variables. \item -Instead of tuples with many components (where ``many'' is not much above 2), -it is preferable to use records. +Tuples with more than two or three components become unwieldy; +records are preferable. \end{itemize} For more information on pairs and records see Chapter~\ref{ch:more-types}.% \end{isamarkuptext}% diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/document/simp.tex --- a/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/document/simp.tex Fri Jan 05 18:32:57 2001 +0100 @@ -8,7 +8,7 @@ \begin{isamarkuptext}% \indexbold{simplification rule} To facilitate simplification, theorems can be declared to be simplification -rules (with the help of the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp +rules (by the attribute \isa{{\isacharbrackleft}simp{\isacharbrackright}}\index{*simp (attribute)}), in which case proofs by simplification make use of these rules automatically. In addition the constructs \isacommand{datatype} and \isacommand{primrec} (and a few others) invisibly declare useful @@ -33,7 +33,7 @@ proofs. Frequent changes in the simplification status of a theorem may indicate a badly designed theory. \begin{warn} - Simplification may not terminate, for example if both $f(x) = g(x)$ and + Simplification may run forever, for example if both $f(x) = g(x)$ and $g(x) = f(x)$ are simplification rules. It is the user's responsibility not to include simplification rules that can lead to nontermination, either on their own or in combination with other simplification rules. @@ -49,7 +49,7 @@ \begin{quote} \isa{simp} \textit{list of modifiers} \end{quote} -where the list of \emph{modifiers} helps to fine tune the behaviour and may +where the list of \emph{modifiers} fine tunes the behaviour and may be empty. Most if not all of the proofs seen so far could have been performed with \isa{simp} instead of \isa{auto}, except that \isa{simp} attacks only the first subgoal and may thus need to be repeated---use @@ -120,10 +120,9 @@ means that the assumptions are simplified but are not used in the simplification of each other or the conclusion. \end{description} -Neither \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} nor \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} allow to simplify -the above problematic subgoal. - -Note that only one of the above options is allowed, and it must precede all +Both \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}simp{\isacharparenright}} and \isa{{\isacharparenleft}no{\isacharunderscore}asm{\isacharunderscore}use{\isacharparenright}} run forever on +the problematic subgoal above. +Note that only one of the options is allowed, and it must precede all other arguments.% \end{isamarkuptext}% % @@ -183,7 +182,7 @@ \index{simplification!of let-expressions} Proving a goal containing \isaindex{let}-expressions almost invariably requires the \isa{let}-con\-structs to be expanded at some point. Since -\isa{let}-\isa{in} is just syntactic sugar for a predefined constant +\isa{let}\ldots\isa{=}\ldots\isa{in}{\ldots} is just syntactic sugar for a predefined constant (called \isa{Let}), expanding \isa{let}-constructs means rewriting with \isa{Let{\isacharunderscore}def}:% \end{isamarkuptext}% @@ -211,13 +210,13 @@ Note the use of ``\ttindexboldpos{,}{$Isar}'' to string together a sequence of methods. Assuming that the simplification rule \isa{{\isacharparenleft}rev\ xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}xs\ {\isacharequal}\ {\isacharbrackleft}{\isacharbrackright}{\isacharparenright}} -is present as well,% +is present as well, +the lemma below is proved by plain simplification:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ rev\ xs{\isachardoublequote}% \begin{isamarkuptext}% \noindent -is proved by plain simplification: -the conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above +The conditional equation \isa{hd{\isacharunderscore}Cons{\isacharunderscore}tl} above can simplify \isa{hd\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharhash}\ tl\ {\isacharparenleft}rev\ xs{\isacharparenright}} to \isa{rev\ xs} because the corresponding precondition \isa{rev\ xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}} simplifies to \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}}, which is exactly the local @@ -327,8 +326,8 @@ \index{arithmetic} The simplifier routinely solves a small class of linear arithmetic formulae (over type \isa{nat} and other numeric types): it only takes into account -assumptions and conclusions that are (possibly negated) (in)equalities -(\isa{{\isacharequal}}, \isasymle, \isa{{\isacharless}}) and it only knows about addition. Thus% +assumptions and conclusions that are relations +($=$, $\le$, $<$, possibly negated) and it only knows about addition. Thus% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}{\isasymlbrakk}\ {\isasymnot}\ m\ {\isacharless}\ n{\isacharsemicolon}\ m\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n{\isachardoublequote}% \begin{isamarkuptext}% diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/pairs.thy --- a/doc-src/TutorialI/Misc/pairs.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/pairs.thy Fri Jan 05 18:32:57 2001 +0100 @@ -22,9 +22,10 @@ Products, like type @{typ nat}, are datatypes, which means in particular that @{text induct_tac} and @{text case_tac} are applicable to terms of product type. +Both replace the term by tuple of variables. \item -Instead of tuples with many components (where ``many'' is not much above 2), -it is preferable to use records. +Tuples with more than two or three components become unwieldy; +records are preferable. \end{itemize} For more information on pairs and records see Chapter~\ref{ch:more-types}. *} diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Misc/simp.thy --- a/doc-src/TutorialI/Misc/simp.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Misc/simp.thy Fri Jan 05 18:32:57 2001 +0100 @@ -6,7 +6,7 @@ text{*\indexbold{simplification rule} To facilitate simplification, theorems can be declared to be simplification -rules (with the help of the attribute @{text"[simp]"}\index{*simp +rules (by the attribute @{text"[simp]"}\index{*simp (attribute)}), in which case proofs by simplification make use of these rules automatically. In addition the constructs \isacommand{datatype} and \isacommand{primrec} (and a few others) invisibly declare useful @@ -32,7 +32,7 @@ proofs. Frequent changes in the simplification status of a theorem may indicate a badly designed theory. \begin{warn} - Simplification may not terminate, for example if both $f(x) = g(x)$ and + Simplification may run forever, for example if both $f(x) = g(x)$ and $g(x) = f(x)$ are simplification rules. It is the user's responsibility not to include simplification rules that can lead to nontermination, either on their own or in combination with other simplification rules. @@ -46,7 +46,7 @@ \begin{quote} @{text simp} \textit{list of modifiers} \end{quote} -where the list of \emph{modifiers} helps to fine tune the behaviour and may +where the list of \emph{modifiers} fine tunes the behaviour and may be empty. Most if not all of the proofs seen so far could have been performed with @{text simp} instead of \isa{auto}, except that @{text simp} attacks only the first subgoal and may thus need to be repeated---use @@ -117,10 +117,9 @@ means that the assumptions are simplified but are not used in the simplification of each other or the conclusion. \end{description} -Neither @{text"(no_asm_simp)"} nor @{text"(no_asm_use)"} allow to simplify -the above problematic subgoal. - -Note that only one of the above options is allowed, and it must precede all +Both @{text"(no_asm_simp)"} and @{text"(no_asm_use)"} run forever on +the problematic subgoal above. +Note that only one of the options is allowed, and it must precede all other arguments. *} @@ -177,7 +176,7 @@ text{*\index{simplification!of let-expressions} Proving a goal containing \isaindex{let}-expressions almost invariably requires the @{text"let"}-con\-structs to be expanded at some point. Since -@{text"let"}-@{text"in"} is just syntactic sugar for a predefined constant +@{text"let"}\ldots\isa{=}\ldots@{text"in"}{\ldots} is just syntactic sugar for a predefined constant (called @{term"Let"}), expanding @{text"let"}-constructs means rewriting with @{thm[source]Let_def}: *} @@ -209,6 +208,7 @@ sequence of methods. Assuming that the simplification rule @{term"(rev xs = []) = (xs = [])"} is present as well, +the lemma below is proved by plain simplification: *} lemma "xs \ [] \ hd(rev xs) # tl(rev xs) = rev xs"; @@ -216,8 +216,7 @@ by(simp); (*>*) text{*\noindent -is proved by plain simplification: -the conditional equation @{thm[source]hd_Cons_tl} above +The conditional equation @{thm[source]hd_Cons_tl} above can simplify @{term"hd(rev xs) # tl(rev xs)"} to @{term"rev xs"} because the corresponding precondition @{term"rev xs ~= []"} simplifies to @{term"xs ~= []"}, which is exactly the local @@ -333,8 +332,8 @@ text{*\index{arithmetic} The simplifier routinely solves a small class of linear arithmetic formulae (over type \isa{nat} and other numeric types): it only takes into account -assumptions and conclusions that are (possibly negated) (in)equalities -(@{text"="}, \isasymle, @{text"<"}) and it only knows about addition. Thus +assumptions and conclusions that are relations +($=$, $\le$, $<$, possibly negated) and it only knows about addition. Thus *} lemma "\ \ m < n; m < n+1 \ \ m = n" diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/Induction.thy --- a/doc-src/TutorialI/Recdef/Induction.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Recdef/Induction.thy Fri Jan 05 18:32:57 2001 +0100 @@ -16,14 +16,15 @@ requires you to prove for each \isacommand{recdef} equation that the property you are trying to establish holds for the left-hand side provided it holds for all recursive calls on the right-hand side. Here is a simple example +involving the predefined @{term"map"} functional on lists: *} lemma "map f (sep(x,xs)) = sep(f x, map f xs)"; txt{*\noindent -involving the predefined @{term"map"} functional on lists: @{term"map f xs"} +Note that @{term"map f xs"} is the result of applying @{term"f"} to all elements of @{term"xs"}. We prove -this lemma by recursion induction w.r.t. @{term"sep"}: +this lemma by recursion induction over @{term"sep"}: *} apply(induct_tac x xs rule: sep.induct); @@ -46,7 +47,7 @@ In general, the format of invoking recursion induction is \begin{quote} -\isacommand{apply}@{text"(induct_tac ("}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} +\isacommand{apply}@{text"(induct_tac "}$x@1 \dots x@n$ @{text"rule:"} $f$@{text".induct)"} \end{quote}\index{*induct_tac}% where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the name of a function that takes an $n$-tuple. Usually the subgoal will diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/document/Induction.tex --- a/doc-src/TutorialI/Recdef/document/Induction.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Recdef/document/Induction.tex Fri Jan 05 18:32:57 2001 +0100 @@ -15,14 +15,15 @@ \textbf{recursion induction}. Roughly speaking, it requires you to prove for each \isacommand{recdef} equation that the property you are trying to establish holds for the left-hand side provided it holds -for all recursive calls on the right-hand side. Here is a simple example% +for all recursive calls on the right-hand side. Here is a simple example +involving the predefined \isa{map} functional on lists:% \end{isamarkuptext}% \isacommand{lemma}\ {\isachardoublequote}map\ f\ {\isacharparenleft}sep{\isacharparenleft}x{\isacharcomma}xs{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ sep{\isacharparenleft}f\ x{\isacharcomma}\ map\ f\ xs{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptxt}% \noindent -involving the predefined \isa{map} functional on lists: \isa{map\ f\ xs} +Note that \isa{map\ f\ xs} is the result of applying \isa{f} to all elements of \isa{xs}. We prove -this lemma by recursion induction w.r.t. \isa{sep}:% +this lemma by recursion induction over \isa{sep}:% \end{isamarkuptxt}% \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ x\ xs\ rule{\isacharcolon}\ sep{\isachardot}induct{\isacharparenright}% \begin{isamarkuptxt}% @@ -48,7 +49,7 @@ In general, the format of invoking recursion induction is \begin{quote} -\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ {\isacharparenleft}}$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} +\isacommand{apply}\isa{{\isacharparenleft}induct{\isacharunderscore}tac\ }$x@1 \dots x@n$ \isa{rule{\isacharcolon}} $f$\isa{{\isachardot}induct{\isacharparenright}} \end{quote}\index{*induct_tac}% where $x@1~\dots~x@n$ is a list of free variables in the subgoal and $f$ the name of a function that takes an $n$-tuple. Usually the subgoal will diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/document/simplification.tex --- a/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Recdef/document/simplification.tex Fri Jan 05 18:32:57 2001 +0100 @@ -75,7 +75,8 @@ In fact, this is probably the neatest solution next to pattern matching. A final alternative is to replace the offending simplification rules by -derived conditional ones. For \isa{gcd} it means we have to prove% +derived conditional ones. For \isa{gcd} it means we have to prove +these lemmas:% \end{isamarkuptext}% \isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}gcd\ {\isacharparenleft}m{\isacharcomma}\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ m{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}simp{\isacharparenright}\isanewline @@ -85,7 +86,7 @@ \isacommand{done}% \begin{isamarkuptext}% \noindent -after which we can disable the original simplification rule:% +Now we can disable the original simplification rule:% \end{isamarkuptext}% \isacommand{declare}\ gcd{\isachardot}simps\ {\isacharbrackleft}simp\ del{\isacharbrackright}\isanewline \end{isabellebody}% diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/document/termination.tex --- a/doc-src/TutorialI/Recdef/document/termination.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Recdef/document/termination.tex Fri Jan 05 18:32:57 2001 +0100 @@ -13,8 +13,8 @@ the same function. What is more, those equations are automatically declared as simplification rules. -In general, Isabelle may not be able to prove all termination conditions -(there is one for each recursive call) automatically. For example, +Isabelle may fail to prove some termination conditions +(there is one for each recursive call). For example, termination of the following artificial function% \end{isamarkuptext}% \isacommand{consts}\ f\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat{\isasymtimes}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline @@ -22,8 +22,8 @@ \ \ {\isachardoublequote}f{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ x\ {\isasymle}\ y\ then\ x\ else\ f{\isacharparenleft}x{\isacharcomma}y{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent -is not proved automatically (although maybe it should be). Isabelle prints a -kind of error message showing you what it was unable to prove. You will then +is not proved automatically. Isabelle prints a +message showing you what it was unable to prove. You will then have to prove it as a separate lemma before you attempt the definition of your function once more. In our case the required lemma is the obvious one:% \end{isamarkuptext}% diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/simplification.thy --- a/doc-src/TutorialI/Recdef/simplification.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Recdef/simplification.thy Fri Jan 05 18:32:57 2001 +0100 @@ -72,6 +72,7 @@ A final alternative is to replace the offending simplification rules by derived conditional ones. For @{term gcd} it means we have to prove +these lemmas: *} lemma [simp]: "gcd (m, 0) = m"; @@ -82,7 +83,7 @@ done text{*\noindent -after which we can disable the original simplification rule: +Now we can disable the original simplification rule: *} declare gcd.simps [simp del] diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Recdef/termination.thy --- a/doc-src/TutorialI/Recdef/termination.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Recdef/termination.thy Fri Jan 05 18:32:57 2001 +0100 @@ -13,8 +13,8 @@ the same function. What is more, those equations are automatically declared as simplification rules. -In general, Isabelle may not be able to prove all termination conditions -(there is one for each recursive call) automatically. For example, +Isabelle may fail to prove some termination conditions +(there is one for each recursive call). For example, termination of the following artificial function *} @@ -23,8 +23,8 @@ "f(x,y) = (if x \ y then x else f(x,y+1))"; text{*\noindent -is not proved automatically (although maybe it should be). Isabelle prints a -kind of error message showing you what it was unable to prove. You will then +is not proved automatically. Isabelle prints a +message showing you what it was unable to prove. You will then have to prove it as a separate lemma before you attempt the definition of your function once more. In our case the required lemma is the obvious one: *} diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Rules/Primes.thy --- a/doc-src/TutorialI/Rules/Primes.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Rules/Primes.thy Fri Jan 05 18:32:57 2001 +0100 @@ -84,7 +84,7 @@ done; theorem gcd_greatest_iff [iff]: - "k dvd gcd(m,n) = (k dvd m \ k dvd n)" + "(k dvd gcd(m,n)) = (k dvd m \ k dvd n)" apply (blast intro!: gcd_greatest intro: dvd_trans); done; diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/ToyList/ToyList.thy --- a/doc-src/TutorialI/ToyList/ToyList.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/ToyList/ToyList.thy Fri Jan 05 18:32:57 2001 +0100 @@ -30,12 +30,11 @@ and not as @{text"(x # y) # z"}. \begin{warn} - Syntax annotations are a powerful but completely optional feature. You + Syntax annotations are a powerful but optional feature. You could drop them from theory @{text"ToyList"} and go back to the identifiers - @{term[source]Nil} and @{term[source]Cons}. However, lists are such a - central datatype - that their syntax is highly customized. We recommend that novices should - not use syntax annotations in their own theories. + @{term[source]Nil} and @{term[source]Cons}. + We recommend that novices avoid using + syntax annotations in their own theories. \end{warn} Next, two functions @{text"app"} and \isaindexbold{rev} are declared: *} @@ -79,8 +78,8 @@ % However, this is a subtle issue that we cannot discuss here further. \begin{warn} - As we have indicated, the desire for total functions is not a gratuitously - imposed restriction but an essential characteristic of HOL. It is only + As we have indicated, the requirement for total functions is not a gratuitous + restriction but an essential characteristic of HOL\@. It is only because of totality that reasoning in HOL is comparatively easy. More generally, the philosophy in HOL is not to allow arbitrary axioms (such as function definitions whose totality has not been proved) because they @@ -116,7 +115,7 @@ illustrate not just the basic proof commands but also the typical proof process. -\subsubsection*{Main goal: @{text"rev(rev xs) = xs"}} +\subsubsection*{Main goal: @{text"rev(rev xs) = xs"}.} Our goal is to show that reversing a list twice produces the original list. The input line @@ -125,6 +124,8 @@ theorem rev_rev [simp]: "rev(rev xs) = xs"; txt{*\index{*theorem|bold}\index{*simp (attribute)|bold} +\noindent +does several things. It \begin{itemize} \item establishes a new theorem to be proved, namely @{prop"rev(rev xs) = xs"}, @@ -231,7 +232,7 @@ txt{*\noindent The keywords \isacommand{theorem}\index{*theorem} and \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate -the importance we attach to a proposition. In general, we use the words +the importance we attach to a proposition. We use the words \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much interchangeably. @@ -334,7 +335,7 @@ done text{*\noindent -and then solve our main theorem: +and then prove our main theorem: *} theorem rev_rev [simp]: "rev(rev xs) = xs"; diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/ToyList/document/ToyList.tex --- a/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/ToyList/document/ToyList.tex Fri Jan 05 18:32:57 2001 +0100 @@ -32,12 +32,11 @@ and not as \isa{{\isacharparenleft}x\ {\isacharhash}\ y{\isacharparenright}\ {\isacharhash}\ z}. \begin{warn} - Syntax annotations are a powerful but completely optional feature. You + Syntax annotations are a powerful but optional feature. You could drop them from theory \isa{ToyList} and go back to the identifiers - \isa{Nil} and \isa{Cons}. However, lists are such a - central datatype - that their syntax is highly customized. We recommend that novices should - not use syntax annotations in their own theories. + \isa{Nil} and \isa{Cons}. + We recommend that novices avoid using + syntax annotations in their own theories. \end{warn} Next, two functions \isa{app} and \isaindexbold{rev} are declared:% \end{isamarkuptext}% @@ -77,8 +76,8 @@ % However, this is a subtle issue that we cannot discuss here further. \begin{warn} - As we have indicated, the desire for total functions is not a gratuitously - imposed restriction but an essential characteristic of HOL. It is only + As we have indicated, the requirement for total functions is not a gratuitous + restriction but an essential characteristic of HOL\@. It is only because of totality that reasoning in HOL is comparatively easy. More generally, the philosophy in HOL is not to allow arbitrary axioms (such as function definitions whose totality has not been proved) because they @@ -113,7 +112,7 @@ illustrate not just the basic proof commands but also the typical proof process. -\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}} +\subsubsection*{Main goal: \isa{rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}.} Our goal is to show that reversing a list twice produces the original list. The input line% @@ -121,6 +120,8 @@ \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}% \begin{isamarkuptxt}% \index{*theorem|bold}\index{*simp (attribute)|bold} +\noindent +does several things. It \begin{itemize} \item establishes a new theorem to be proved, namely \isa{rev\ {\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs}, @@ -221,7 +222,7 @@ \begin{isamarkuptxt}% \noindent The keywords \isacommand{theorem}\index{*theorem} and \isacommand{lemma}\indexbold{*lemma} are interchangable and merely indicate -the importance we attach to a proposition. In general, we use the words +the importance we attach to a proposition. We use the words \emph{theorem}\index{theorem} and \emph{lemma}\index{lemma} pretty much interchangeably. @@ -320,7 +321,7 @@ \isacommand{done}% \begin{isamarkuptext}% \noindent -and then solve our main theorem:% +and then prove our main theorem:% \end{isamarkuptext}% \isacommand{theorem}\ rev{\isacharunderscore}rev\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}rev{\isacharparenleft}rev\ xs{\isacharparenright}\ {\isacharequal}\ xs{\isachardoublequote}\isanewline \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ xs{\isacharparenright}\isanewline diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Trie/Trie.thy --- a/doc-src/TutorialI/Trie/Trie.thy Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Trie/Trie.thy Fri Jan 05 18:32:57 2001 +0100 @@ -3,7 +3,7 @@ (*>*) text{* To minimize running time, each node of a trie should contain an array that maps -letters to subtries. We have chosen a (sometimes) more space efficient +letters to subtries. We have chosen a representation where the subtries are held in an association list, i.e.\ a list of (letter,trie) pairs. Abstracting over the alphabet @{typ"'a"} and the values @{typ"'v"} we define a trie as follows: @@ -67,7 +67,7 @@ "update t (a#as) v = (let tt = (case assoc (alist t) a of None \ Trie None [] | Some at \ at) - in Trie (value t) ((a,update tt as v)#alist t))"; + in Trie (value t) ((a,update tt as v) # alist t))"; text{*\noindent The base case is obvious. In the recursive case the subtrie diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/Trie/document/Trie.tex --- a/doc-src/TutorialI/Trie/document/Trie.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/Trie/document/Trie.tex Fri Jan 05 18:32:57 2001 +0100 @@ -4,7 +4,7 @@ % \begin{isamarkuptext}% To minimize running time, each node of a trie should contain an array that maps -letters to subtries. We have chosen a (sometimes) more space efficient +letters to subtries. We have chosen a representation where the subtries are held in an association list, i.e.\ a list of (letter,trie) pairs. Abstracting over the alphabet \isa{{\isacharprime}a} and the values \isa{{\isacharprime}v} we define a trie as follows:% @@ -59,7 +59,7 @@ \ \ {\isachardoublequote}update\ t\ {\isacharparenleft}a{\isacharhash}as{\isacharparenright}\ v\ {\isacharequal}\isanewline \ \ \ \ \ {\isacharparenleft}let\ tt\ {\isacharequal}\ {\isacharparenleft}case\ assoc\ {\isacharparenleft}alist\ t{\isacharparenright}\ a\ of\isanewline \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ None\ {\isasymRightarrow}\ Trie\ None\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharbar}\ Some\ at\ {\isasymRightarrow}\ at{\isacharparenright}\isanewline -\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}{\isacharhash}alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}% +\ \ \ \ \ \ in\ Trie\ {\isacharparenleft}value\ t{\isacharparenright}\ {\isacharparenleft}{\isacharparenleft}a{\isacharcomma}update\ tt\ as\ v{\isacharparenright}\ {\isacharhash}\ alist\ t{\isacharparenright}{\isacharparenright}{\isachardoublequote}% \begin{isamarkuptext}% \noindent The base case is obvious. In the recursive case the subtrie diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/basics.tex --- a/doc-src/TutorialI/basics.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/basics.tex Fri Jan 05 18:32:57 2001 +0100 @@ -82,7 +82,7 @@ \label{sec:TypesTermsForms} \indexbold{type} -Embedded in a theory are the types, terms and formulae of HOL. HOL is a typed +Embedded in a theory are the types, terms and formulae of HOL\@. HOL is a typed logic whose type system resembles that of functional programming languages like ML or Haskell. Thus there are \begin{description} @@ -102,7 +102,7 @@ which abbreviates \isa{$\tau@1$ \isasymFun~$\cdots$ \isasymFun~$\tau@n$ \isasymFun~$\tau$}. \item[type variables,]\indexbold{type variable}\indexbold{variable!type} - denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML. They give rise + denoted by \ttindexboldpos{'a}{$Isatype}, \isa{'b} etc., just like in ML\@. They give rise to polymorphic types like \isa{'a \isasymFun~'a}, the type of the identity function. \end{description} @@ -172,7 +172,7 @@ \isa{$t@1$~\isasymnoteq~$t@2$} is merely an abbreviation for \isa{\isasymnot($t@1$ = $t@2$)}. -The syntax for quantifiers is +Quantifiers are written as \isa{\isasymforall{}x.~$P$}\indexbold{$HOL0All@\isasymforall} and \isa{\isasymexists{}x.~$P$}\indexbold{$HOL0Ex@\isasymexists}. There is even \isa{\isasymuniqex{}x.~$P$}\index{$HOL0ExU@\isasymuniqex|bold}, which @@ -185,7 +185,7 @@ \isa{$t$::$\tau$} as in \isa{x < (y::nat)}. Note that \ttindexboldpos{::}{$Isatype} binds weakly and should therefore be enclosed in parentheses: \isa{x < y::nat} is ill-typed because it is interpreted as -\isa{(x < y)::nat}. The main reason for type constraints are overloaded +\isa{(x < y)::nat}. The main reason for type constraints is overloading of functions like \isa{+}, \isa{*} and \isa{<}. See {\S}\ref{sec:overloading} for a full discussion of overloading and Table~\ref{tab:overloading} for the most important overloaded function symbols. @@ -195,10 +195,10 @@ functional programming and mathematics. Below we list the main rules that you should be familiar with to avoid certain syntactic traps. A particular problem for novices can be the priority of operators. If you are unsure, use -more rather than fewer parentheses. In those cases where Isabelle echoes your +additional parentheses. In those cases where Isabelle echoes your input, you can see which parentheses are dropped---they were superfluous. If you are unsure how to interpret Isabelle's output because you don't know -where the (dropped) parentheses go, set (and possibly reset) the \rmindex{flag} +where the (dropped) parentheses go, set the \rmindex{flag} \isaindexbold{show_brackets}: \begin{ttbox} ML "set show_brackets"; $\dots$; ML "reset show_brackets"; @@ -300,4 +300,4 @@ type each command into the file first and then enter it into Isabelle by copy-and-paste, thus ensuring that you have a complete record of your theory. As mentioned above, Proof General offers a much superior interface. -If you have installed Proof General, you can start it with \texttt{Isabelle}. +If you have installed Proof General, you can start it by typing \texttt{Isabelle}. diff -r 65d18005d802 -r 9e888d60d3e5 doc-src/TutorialI/fp.tex --- a/doc-src/TutorialI/fp.tex Fri Jan 05 18:32:33 2001 +0100 +++ b/doc-src/TutorialI/fp.tex Fri Jan 05 18:32:57 2001 +0100 @@ -29,8 +29,8 @@ {\makeatother\input{ToyList/document/ToyList.tex}} -The complete proof script is shown in figure~\ref{fig:ToyList-proofs}. The -concatenation of figures \ref{fig:ToyList} and \ref{fig:ToyList-proofs} +The complete proof script is shown in Fig.\ts\ref{fig:ToyList-proofs}. The +concatenation of Figs.\ts\ref{fig:ToyList} and~\ref{fig:ToyList-proofs} constitutes the complete theory \texttt{ToyList} and should reside in file \texttt{ToyList.thy}. It is good practice to present all declarations and definitions at the beginning of a theory to facilitate browsing. @@ -159,7 +159,10 @@ The latter contains many further operations. For example, the functions \isaindexbold{hd} (``head'') and \isaindexbold{tl} (``tail'') return the first element and the remainder of a list. (However, pattern-matching is usually -preferable to \isa{hd} and \isa{tl}.) Theory \isa{List} also contains +preferable to \isa{hd} and \isa{tl}.) +Also available are the higher-order +functions \isa{map}, \isa{filter}, \isa{foldl} and \isa{foldr}. +Theory \isa{List} also contains more syntactic sugar: \isa{[}$x@1$\isa{,}\dots\isa{,}$x@n$\isa{]} abbreviates $x@1$\isa{\#}\dots\isa{\#}$x@n$\isa{\#[]}. In the rest of the tutorial we always use HOL's predefined lists. @@ -193,7 +196,7 @@ \isa{1 +} the sum of the sizes of all arguments of type $t$. Note that because \isa{size} is defined on every datatype, it is overloaded; on lists \isa{size} is also called \isaindexbold{length}, which is not overloaded. -Isbelle will always show \isa{size} on lists as \isa{length}. +Isabelle will always show \isa{size} on lists as \isa{length}. \subsection{Primitive recursion} @@ -261,7 +264,7 @@ \subsection{Type synonyms} \indexbold{type synonym} -Type synonyms are similar to those found in ML. Their syntax is fairly self +Type synonyms are similar to those found in ML\@. Their syntax is fairly self explanatory: \input{Misc/document/types.tex}% @@ -294,7 +297,7 @@ \label{sec:Simplification} \index{simplification|(} -So far we have proved our theorems by \isa{auto}, which ``simplifies'' +So far we have proved our theorems by \isa{auto}, which simplifies \emph{all} subgoals. In fact, \isa{auto} can do much more than that, except that it did not need to so far. However, when you go beyond toy examples, you need to understand the ingredients of \isa{auto}. This section covers the @@ -363,7 +366,8 @@ \begin{isabelle} \isacommand{datatype} t = C "t \isasymRightarrow\ bool" \end{isabelle} -is a real can of worms: in HOL it must be ruled out because it requires a type +This declaration is a real can of worms. +In HOL it must be ruled out because it requires a type \isa{t} such that \isa{t} and its power set \isa{t \isasymFun\ bool} have the same cardinality---an impossibility. For the same reason it is not possible to allow recursion involving the type \isa{set}, which is isomorphic to @@ -384,8 +388,10 @@ \begin{isabelle} \isacommand{datatype} lam = C "lam \isasymrightarrow\ lam" \end{isabelle} -do indeed make sense (but note the intentionally different arrow -\isa{\isasymrightarrow}). There is even a version of LCF on top of HOL, +do indeed make sense. Note the different arrow, +\isa{\isasymrightarrow} instead of \isa{\isasymRightarrow}, +expressing the type of \textbf{continuous} functions. +There is even a version of LCF on top of HOL, called HOLCF~\cite{MuellerNvOS99}. \index{*primrec|)}