author nipkow Tue, 24 Apr 2012 09:09:55 +0200 changeset 47711 c1cca2a052e4 parent 47710 4ced56100757 child 47712 81c3c4e01263
doc update
--- a/doc-src/ProgProve/Thys/Bool_nat_list.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Bool_nat_list.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -138,11 +138,11 @@
Throughout this book, \concept{IH} will stand for induction hypothesis''.

We have now seen three proofs of @{prop"add m 0 = 0"}: the Isabelle one, the
-terse 4 lines explaining the base case and the induction step, and just now a
+terse four lines explaining the base case and the induction step, and just now a
model of a traditional inductive proof. The three proofs differ in the level
of detail given and the intended reader: the Isabelle proof is for the
machine, the informal proofs are for humans. Although this book concentrates
-of Isabelle proofs, it is important to be able to rephrase those proofs
+on Isabelle proofs, it is important to be able to rephrase those proofs
mathematical proofs. Later on we will introduce an Isabelle proof language
that is closer to traditional informal mathematical language and is often
@@ -162,7 +162,7 @@

text{*
\begin{itemize}
-\item Type @{typ "'a list"} is the type of list over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
+\item Type @{typ "'a list"} is the type of lists over elements of type @{typ 'a}. Because @{typ 'a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
\item Lists have two constructors: @{const Nil}, the empty list, and @{const Cons}, which puts an element (of type @{typ 'a}) in front of a list (of type @{typ "'a list"}).
Hence all lists are of the form @{const Nil}, or @{term"Cons x Nil"},
or @{term"Cons x (Cons y Nil)"} etc.
@@ -218,7 +218,7 @@
you need to prove
\begin{enumerate}
\item the base case @{prop"P(Nil)"} and
-\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text xs}.
+\item the inductive case @{prop"P(Cons x xs)"} under the assumption @{prop"P(xs)"}, for some arbitrary but fixed @{text x} and @{text xs}.
\end{enumerate}
This is often called \concept{structural induction}.

@@ -302,7 +302,7 @@
We find that this time @{text"auto"} solves the base case, but the
induction step merely simplifies to
@{subgoals[display,indent=0,goals_limit=1]}
-The the missing lemma is associativity of @{const app},
+The missing lemma is associativity of @{const app},
which we insert in front of the failed lemma @{text rev_app}.

\subsubsection{Associativity of @{const app}}
--- a/doc-src/ProgProve/Thys/Isar.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Isar.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -172,7 +172,7 @@
\end{tabular}
\medskip

-\noindent The \isacom{using} idiom de-emphasises the used facts by moving them
+\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
behind the proposition.

\subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
@@ -228,7 +228,7 @@
default. The patterns are phrased in terms of \isacom{show} but work for
\isacom{have} and \isacom{lemma}, too.

starting from a formula @{text P} we have the two cases @{text P} and
@{prop"~P"}, and starting from a fact @{prop"P \<or> Q"}
we have the two cases @{text P} and @{text Q}:
@@ -548,7 +548,7 @@

Sometimes one would like to prove some lemma locally within a proof.
A lemma that shares the current context of assumptions but that
-has its own assumptions and is generalised over its locally fixed
+has its own assumptions and is generalized over its locally fixed
variables at the end. This is what a \concept{raw proof block} does:
\begin{quote}
@{text"{"} \isacom{fix} @{text"x\<^isub>1 \<dots> x\<^isub>n"}\\
@@ -590,14 +590,14 @@
the fact just proved, in this case the preceding block. In general,
\isacom{note} introduces a new name for one or more facts.

-\section{Case distinction and induction}
+\section{Case analysis and induction}

-\subsection{Datatype case distinction}
+\subsection{Datatype case analysis}

-We have seen case distinction on formulas. Now we want to distinguish
+We have seen case analysis on formulas. Now we want to distinguish
which form some term takes: is it @{text 0} or of the form @{term"Suc n"},
is it @{term"[]"} or of the form @{term"x#xs"}, etc. Here is a typical example
-proof by case distinction on the form of @{text xs}:
+proof by case analysis on the form of @{text xs}:
*}

lemma "length(tl xs) = length xs - 1"
@@ -650,12 +650,12 @@
Never mind the details, just focus on the pattern:
*}

-lemma "\<Sum>{0..n::nat} = n*(n+1) div 2" (is "?P n")
+lemma "\<Sum>{0..n::nat} = n*(n+1) div 2"
proof (induction n)
show "\<Sum>{0..0::nat} = 0*(0+1) div 2" by simp
next
fix n assume "\<Sum>{0..n::nat} = n*(n+1) div 2"
-  thus "\<Sum>{0..Suc n::nat} = Suc n*(Suc n+1) div 2" by simp
+  thus "\<Sum>{0..Suc n} = Suc n*(Suc n+1) div 2" by simp
qed

text{* Except for the rewrite steps, everything is explicitly given. This
@@ -920,13 +920,13 @@

\subsection{Rule inversion}

-Rule inversion is case distinction on which rule could have been used to
+Rule inversion is case analysis of which rule could have been used to
derive some fact. The name \concept{rule inversion} emphasizes that we are
reasoning backwards: by which rules could some given fact have been proved?
For the inductive definition of @{const ev}, rule inversion can be summarized
like this:
@{prop[display]"ev n \<Longrightarrow> n = 0 \<or> (EX k. n = Suc(Suc k) \<and> ev k)"}
-The realisation in Isabelle is a case distinction.
+The realisation in Isabelle is a case analysis.
A simple example is the proof that @{prop"ev n \<Longrightarrow> ev (n - 2)"}. We
already went through the details informally in \autoref{sec:Logic:even}. This
is the Isar proof:
@@ -946,7 +946,7 @@
end
(*>*)

-text{* The key point here is that a case distinction over some inductively
+text{* The key point here is that a case analysis over some inductively
defined predicate is triggered by piping the given fact
(here: \isacom{from}~@{text this}) into a proof by @{text cases}.
Let us examine the assumptions available in each case. In case @{text ev0}
--- a/doc-src/ProgProve/Thys/Logic.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Logic.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -5,12 +5,12 @@
(*>*)
text{*
\vspace{-5ex}
-\section{Logic and Proof Beyond Equality}
+\section{Logic and proof beyond equality}
\label{sec:Logic}

\subsection{Formulas}

-The basic syntax of formulas (\textit{form} below)
+The core syntax of formulas (\textit{form} below)
provides the standard logical constructs, in decreasing precedence:
$\begin{array}{rcl} @@ -27,14 +27,14 @@ &\mid& @{prop"\<forall>x. form"} ~\mid~ @{prop"\<exists>x. form"} \end{array}$
-Terms are the ones we have seen all along, built from constant, variables,
+Terms are the ones we have seen all along, built from constants, variables,
function application and @{text"\<lambda>"}-abstraction, including all the syntactic
sugar like infix symbols, @{text "if"}, @{text "case"} etc.
\begin{warn}
Remember that formulas are simply terms of type @{text bool}. Hence
@{text "="} also works for formulas. Beware that @{text"="} has a higher
precedence than the other logical operators. Hence @{prop"s = t \<and> A"} means
-@{text"(s = t) \<and> A"}, and @{prop"A\<and>B = B\<and>A"} means @{text"A \<and> (B = A) \<and> B"}.
+@{text"(s = t) \<and> A"}, and @{prop"A\<and>B = B\<and>A"} means @{text"A \<and> (B = B) \<and> A"}.
Logical equivalence can also be written with
@{text "\<longleftrightarrow>"} instead of @{text"="}, where @{text"\<longleftrightarrow>"} has the same low
precedence as @{text"\<longrightarrow>"}. Hence @{text"A \<and> B \<longleftrightarrow> B \<and> A"} really means
@@ -51,7 +51,7 @@
@{text "\<exists>"} & \xsymbol{exists} & \texttt{EX}\\
@{text "\<lambda>"} & \xsymbol{lambda} & \texttt{\%}\\
@{text "\<longrightarrow>"} & \texttt{-{}->}\\
-@{text "\<longleftrightarrow>"} & \texttt{<-{}->}\\
+@{text "\<longleftrightarrow>"} & \texttt{<->}\\
@{text "\<and>"} & \texttt{/\char\\} & \texttt{\&}\\
@{text "\<or>"} & \texttt{\char\\/} & \texttt{|}\\
@{text "\<not>"} & \xsymbol{not} & \texttt{\char~}\\
@@ -63,7 +63,7 @@
and the third column shows ASCII representations that stay fixed.
\begin{warn}
The implication @{text"\<Longrightarrow>"} is part of the Isabelle framework. It structures
-theorems and proof states, separating assumptions from conclusion.
+theorems and proof states, separating assumptions from conclusions.
The implication @{text"\<longrightarrow>"} is part of the logic HOL and can occur inside the
formulas that make up the assumptions and conclusion.
Theorems should be of the form @{text"\<lbrakk> A\<^isub>1; \<dots>; A\<^isub>n \<rbrakk> \<Longrightarrow> A"},
@@ -74,7 +74,7 @@
\subsection{Sets}

Sets of elements of type @{typ 'a} have type @{typ"'a set"}.
-They can be finite or infinite. Sets come with the usual notations:
+They can be finite or infinite. Sets come with the usual notation:
\begin{itemize}
\item @{prop"e \<in> A"},\quad @{prop"A \<subseteq> B"}
@@ -87,7 +87,7 @@
\begin{warn}
In @{term"{x. P}"} the @{text x} must be a variable. Set comprehension
involving a proper term @{text t} must be written
-@{term[source]"{t |x y z. P}"},
+@{term[source]"{t | x y z. P}"},
where @{text "x y z"} are the free variables in @{text t}.
This is just a shorthand for @{term"{v. EX x y z. v = t \<and> P}"}, where
@{text v} is a new variable.
@@ -153,8 +153,8 @@
succeeds where @{text fastforce} fails.

The method of choice for complex logical goals is @{text blast}. In the
-following example, @{text T} and @{text A} are two binary predicates, and it
-is shown that @{text T} is total, @{text A} is antisymmetric and @{text T} is
+following example, @{text T} and @{text A} are two binary predicates. It
+is shown that if @{text T} is total, @{text A} is antisymmetric and @{text T} is
a subset of @{text A}, then @{text A} is a subset of @{text T}:
*}

@@ -344,12 +344,12 @@
automatically selects the appropriate rule for the current subgoal.

You can also turn your own theorems into introduction rules by giving them
-them @{text"intro"} attribute, analogous to the @{text simp} attribute.  In
+the @{text"intro"} attribute, analogous to the @{text simp} attribute.  In
that case @{text blast}, @{text fastforce} and (to a limited extent) @{text
auto} will automatically backchain with those theorems. The @{text intro}
attribute should be used with care because it increases the search space and
-can lead to nontermination.  Sometimes it is better to use it only in a
-particular calls of @{text blast} and friends. For example,
+can lead to nontermination.  Sometimes it is better to use it only in
+specific calls of @{text blast} and friends. For example,
@{thm[source] le_trans}, transitivity of @{text"\<le>"} on type @{typ nat},
is not an introduction rule by default because of the disastrous effect
on the search space, but can be useful in specific situations:
@@ -419,8 +419,11 @@
\label{sec:inductive-defs}

Inductive definitions are the third important definition facility, after
-datatypes and recursive function. In fact, they are the key construct in the
+datatypes and recursive function.
+\sem
+In fact, they are the key construct in the
definition of operational semantics in the second part of the book.
+\endsem

\subsection{An example: even numbers}
\label{sec:Logic:even}
@@ -506,9 +509,9 @@
case @{thm[source]evSS} we have \mbox{@{prop"m = n+(2::nat)"}} and may assume
@{prop"ev n"}, which implies @{prop"ev (m - 2)"} because @{text"m - 2 = (n +
2) - 2 = n"}. We did not need the induction hypothesis at all for this proof,
-it is just a case distinction on which rule was used, but having @{prop"ev
+it is just a case analysis of which rule was used, but having @{prop"ev
n"} at our disposal in case @{thm[source]evSS} was essential.
-This case distinction over rules is also called rule inversion''
+This case analysis of rules is also called rule inversion''
and is discussed in more detail in \autoref{ch:Isar}.

\subsubsection{In Isabelle}
@@ -589,7 +592,7 @@
definition only expresses the positive information directly. The negative
information, for example, that @{text 1} is not even, has to be proved from
it (by induction or rule inversion). On the other hand, rule induction is
-Taylor made for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you
+tailor-made for proving \mbox{@{prop"ev n \<Longrightarrow> P n"}} because it only asks you
to prove the positive cases. In the proof of @{prop"even n \<Longrightarrow> P n"} by
computation induction via @{thm[source]even.induct}, we are also presented
with the trivial negative cases. If you want the convenience of both
@@ -599,8 +602,8 @@

But many concepts do not admit a recursive definition at all because there is
no datatype for the recursion (for example, the transitive closure of a
-relation), or the recursion would not terminate (for example, the operational
-semantics in the second part of this book). Even if there is a recursive
+relation), or the recursion would not terminate (for example,
+an interpreter for a programming language). Even if there is a recursive
definition, if we are only interested in the positive information, the
inductive definition may be much simpler.

@@ -609,8 +612,11 @@

Evenness is really more conveniently expressed recursively than inductively.
As a second and very typical example of an inductive definition we define the
-reflexive transitive closure. It will also be an important building block for
+reflexive transitive closure.
+\sem
+It will also be an important building block for
some of the semantics considered in the second part of the book.
+\endsem

The reflexive transitive closure, called @{text star} below, is a function
that maps a binary predicate to another binary predicate: if @{text r} is of
@@ -628,8 +634,8 @@

text{* The base case @{thm[source] refl} is reflexivity: @{term "x=y"}. The
step case @{thm[source]step} combines an @{text r} step (from @{text x} to
-@{text y}) and a @{const star} step (from @{text y} to @{text z}) into a
-@{const star} step (from @{text x} to @{text z}).
+@{text y}) and a @{term"star r"} step (from @{text y} to @{text z}) into a
+@{term"star r"} step (from @{text x} to @{text z}).
The \isacom{for}~@{text r}'' in the header is merely a hint to Isabelle
that @{text r} is a fixed parameter of @{const star}, in contrast to the
further parameters of @{const star}, which change. As a result, Isabelle
--- a/doc-src/ProgProve/Thys/Types_and_funs.thy	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/Types_and_funs.thy	Tue Apr 24 09:09:55 2012 +0200
@@ -132,12 +132,12 @@
function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by
subtracting @{term"f n"} on both sides.

-Isabelle automatic termination checker requires that the arguments of
+Isabelle's automatic termination checker requires that the arguments of
recursive calls on the right-hand side must be strictly smaller than the
arguments on the left-hand side. In the simplest case, this means that one
fixed argument position decreases in size with each recursive call. The size
is measured as the number of constructors (excluding 0-ary ones, e.g.\ @{text
-Nil}). Lexicographic combinations are also recognised. In more complicated
+Nil}). Lexicographic combinations are also recognized. In more complicated
situations, the user may have to prove termination by hand. For details
see~\cite{Krauss}.

@@ -152,7 +152,7 @@
"div2 (Suc(Suc n)) = Suc(div2 n)"

text{* does not just define @{const div2} but also proves a
-customised induction rule:
+customized induction rule:
$\inferrule{ \mbox{@{thm (prem 1) div2.induct}}\\ @@ -160,7 +160,7 @@ \mbox{@{thm (prem 3) div2.induct}}} {\mbox{@{thm (concl) div2.induct[of _ "m"]}}}$
-This customised induction rule can simplify inductive proofs. For example,
+This customized induction rule can simplify inductive proofs. For example,
*}

lemma "div2(n+n) = n"
@@ -171,7 +171,7 @@
An application of @{text auto} finishes the proof.
Had we used ordinary structural induction on @{text n},
the proof would have needed an additional
-case distinction in the induction step.
+case analysis in the induction step.

The general case is often called \concept{computation induction},
because the induction follows the (terminating!) computation.
@@ -202,7 +202,7 @@
if the function is defined by recursion on argument number $i$.}
\end{quote}
The key heuristic, and the main point of this section, is to
-\emph{generalise the goal before induction}.
+\emph{generalize the goal before induction}.
The reason is simple: if the goal is
too specific, the induction hypothesis is too weak to allow the induction
step to go through. Let us illustrate the idea with an example.
@@ -218,12 +218,12 @@
done
(*>*)
fun itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where
-"itrev []     ys = ys" |
+"itrev []        ys = ys" |
"itrev (x#xs) ys = itrev xs (x#ys)"

text{* The behaviour of @{const itrev} is simple: it reverses
its first argument by stacking its elements onto the second argument,
-and returning that second argument when the first one becomes
+and it returns that second argument when the first one becomes
empty. Note that @{const itrev} is tail-recursive: it can be
compiled into a loop, no stack is necessary for executing it.

@@ -247,10 +247,10 @@
argument,~@{term"[]"}, prevents it from rewriting the conclusion.
This example suggests a heuristic:
\begin{quote}
-\emph{Generalise goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
Of course one cannot do this na\"{\i}vely: @{prop"itrev xs ys = rev xs"} is
-just not true.  The correct generalisation is
+just not true.  The correct generalization is
*};
(*<*)oops;(*>*)
lemma "itrev xs ys = rev xs @ ys"
@@ -258,7 +258,7 @@
txt{*
If @{text ys} is replaced by @{term"[]"}, the right-hand side simplifies to
@{term"rev xs"}, as required.
-In this instance it was easy to guess the right generalisation.
+In this instance it was easy to guess the right generalization.
Other situations can require a good deal of creativity.

Although we now have two variables, only @{text xs} is suitable for
@@ -266,12 +266,12 @@
not there:
@{subgoals[display,margin=65]}
The induction hypothesis is still too weak, but this time it takes no
-intuition to generalise: the problem is that the @{text ys}
+intuition to generalize: the problem is that the @{text ys}
in the induction hypothesis is fixed,
but the induction hypothesis needs to be applied with
@{term"a # ys"} instead of @{text ys}. Hence we prove the theorem
for all @{text ys} instead of a fixed one. We can instruct induction
-to perform this generalisation for us by adding @{text "arbitrary: ys"}.
+to perform this generalization for us by adding @{text "arbitrary: ys"}.
*}
(*<*)oops
lemma "itrev xs ys = rev xs @ ys"
@@ -287,12 +287,12 @@
done

text{*
-This leads to another heuristic for generalisation:
+This leads to another heuristic for generalization:
\begin{quote}
-\emph{Generalise induction by generalising all free
+\emph{Generalize induction by generalizing all free
variables\\ {\em(except the induction variable itself)}.}
\end{quote}
-Generalisation is best performed with @{text"arbitrary: y\<^isub>1 \<dots> y\<^isub>k"}.
+Generalization is best performed with @{text"arbitrary: y\<^isub>1 \<dots> y\<^isub>k"}.
This heuristic prevents trivial failures like the one above.
However, it should not be applied blindly.
It is not always required, and the additional quantifiers can complicate
@@ -306,7 +306,7 @@
\item using equations $l = r$ from left to right (only),
\item as long as possible.
\end{itemize}
-To emphasise the directionality, equations that have been given the
+To emphasize the directionality, equations that have been given the
@{text"simp"} attribute are called \concept{simplification}
rules. Logically, they are still symmetric, but proofs by
simplification use them only in the left-to-right direction.  The proof tool
--- a/doc-src/ProgProve/Thys/document/Bool_nat_list.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Bool_nat_list.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -192,11 +192,11 @@
Throughout this book, \concept{IH} will stand for induction hypothesis''.

-terse 4 lines explaining the base case and the induction step, and just now a
+terse four lines explaining the base case and the induction step, and just now a
model of a traditional inductive proof. The three proofs differ in the level
of detail given and the intended reader: the Isabelle proof is for the
machine, the informal proofs are for humans. Although this book concentrates
-of Isabelle proofs, it is important to be able to rephrase those proofs
+on Isabelle proofs, it is important to be able to rephrase those proofs
mathematical proofs. Later on we will introduce an Isabelle proof language
that is closer to traditional informal mathematical language and is often
@@ -219,7 +219,7 @@
\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{3D}{\isacharequal}}\ Nil\ {\isaliteral{7C}{\isacharbar}}\ Cons\ {\isaliteral{27}{\isacharprime}}a\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
\begin{itemize}
-\item Type \isa{{\isaliteral{27}{\isacharprime}}a\ list} is the type of list over elements of type \isa{{\isaliteral{27}{\isacharprime}}a}. Because \isa{{\isaliteral{27}{\isacharprime}}a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
+\item Type \isa{{\isaliteral{27}{\isacharprime}}a\ list} is the type of lists over elements of type \isa{{\isaliteral{27}{\isacharprime}}a}. Because \isa{{\isaliteral{27}{\isacharprime}}a} is a type variable, lists are in fact \concept{polymorphic}: the elements of a list can be of arbitrary type (but must all be of the same type).
\item Lists have two constructors: \isa{Nil}, the empty list, and \isa{Cons}, which puts an element (of type \isa{{\isaliteral{27}{\isacharprime}}a}) in front of a list (of type \isa{{\isaliteral{27}{\isacharprime}}a\ list}).
Hence all lists are of the form \isa{Nil}, or \isa{Cons\ x\ Nil},
or \isa{Cons\ x\ {\isaliteral{28}{\isacharparenleft}}Cons\ y\ Nil{\isaliteral{29}{\isacharparenright}}} etc.
@@ -282,7 +282,7 @@
you need to prove
\begin{enumerate}
\item the base case \isa{P\ Nil} and
-\item the inductive case \isa{P\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}} under the assumption \isa{P\ xs}, for some arbitrary but fixed \isa{xs}.
+\item the inductive case \isa{P\ {\isaliteral{28}{\isacharparenleft}}Cons\ x\ xs{\isaliteral{29}{\isacharparenright}}} under the assumption \isa{P\ xs}, for some arbitrary but fixed \isa{x} and \isa{xs}.
\end{enumerate}
This is often called \concept{structural induction}.

@@ -435,7 +435,7 @@
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }app\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }app\ {\isaliteral{28}{\isacharparenleft}}rev\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}app\ {\isaliteral{28}{\isacharparenleft}}rev\ xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}Cons\ a\ Nil{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
-The the missing lemma is associativity of \isa{app},
+The missing lemma is associativity of \isa{app},
which we insert in front of the failed lemma \isa{rev{\isaliteral{5F}{\isacharunderscore}}app}.

\subsubsection{Associativity of \isa{app}}
--- a/doc-src/ProgProve/Thys/document/Isar.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Isar.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -263,7 +263,7 @@
\end{tabular}
\medskip

-\noindent The \isacom{using} idiom de-emphasises the used facts by moving them
+\noindent The \isacom{using} idiom de-emphasizes the used facts by moving them
behind the proposition.

\subsection{Structured lemma statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
@@ -339,7 +339,7 @@
default. The patterns are phrased in terms of \isacom{show} but work for
\isacom{have} and \isacom{lemma}, too.

starting from a formula \isa{P} we have the two cases \isa{P} and
\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ P}, and starting from a fact \isa{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}
we have the two cases \isa{P} and \isa{Q}:%
@@ -946,7 +946,7 @@

Sometimes one would like to prove some lemma locally within a proof.
A lemma that shares the current context of assumptions but that
-has its own assumptions and is generalised over its locally fixed
+has its own assumptions and is generalized over its locally fixed
variables at the end. This is what a \concept{raw proof block} does:
\begin{quote}
\isa{{\isaliteral{7B}{\isacharbraceleft}}} \isacom{fix} \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ x\isaliteral{5C3C5E697375623E}{}\isactrlisub n}\\
@@ -1016,14 +1016,14 @@
the fact just proved, in this case the preceding block. In general,
\isacom{note} introduces a new name for one or more facts.

-\section{Case distinction and induction}
+\section{Case analysis and induction}

-\subsection{Datatype case distinction}
+\subsection{Datatype case analysis}

-We have seen case distinction on formulas. Now we want to distinguish
+We have seen case analysis on formulas. Now we want to distinguish
which form some term takes: is it \isa{{\isadigit{0}}} or of the form \isa{Suc\ n},
is it \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} or of the form \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}, etc. Here is a typical example
-proof by case distinction on the form of \isa{xs}:%
+proof by case analysis on the form of \isa{xs}:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -1123,7 +1123,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
%
%
@@ -1141,7 +1141,7 @@
\ n\ \isacommand{assume}\isamarkupfalse%
\ \ \isacommand{thus}\isamarkupfalse%
\ simp\isanewline
\isacommand{qed}\isamarkupfalse%
%
@@ -1548,7 +1548,7 @@

\subsection{Rule inversion}

-Rule inversion is case distinction on which rule could have been used to
+Rule inversion is case analysis of which rule could have been used to
derive some fact. The name \concept{rule inversion} emphasizes that we are
reasoning backwards: by which rules could some given fact have been proved?
For the inductive definition of \isa{ev}, rule inversion can be summarized
@@ -1556,7 +1556,7 @@
\begin{isabelle}%
ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}k{\isaliteral{2E}{\isachardot}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ k{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ ev\ k{\isaliteral{29}{\isacharparenright}}%
\end{isabelle}
-The realisation in Isabelle is a case distinction.
+The realisation in Isabelle is a case analysis.
A simple example is the proof that \isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ ev\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}}. We
already went through the details informally in \autoref{sec:Logic:even}. This
is the Isar proof:%
@@ -1595,7 +1595,7 @@
%
\begin{isamarkuptext}%
-The key point here is that a case distinction over some inductively
+The key point here is that a case analysis over some inductively
defined predicate is triggered by piping the given fact
(here: \isacom{from}~\isa{this}) into a proof by \isa{cases}.
Let us examine the assumptions available in each case. In case \isa{ev{\isadigit{0}}}
--- a/doc-src/ProgProve/Thys/document/Logic.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Logic.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -17,12 +17,12 @@
%
\begin{isamarkuptext}%
\vspace{-5ex}
-\section{Logic and Proof Beyond Equality}
+\section{Logic and proof beyond equality}
\label{sec:Logic}

\subsection{Formulas}

-The basic syntax of formulas (\textit{form} below)
+The core syntax of formulas (\textit{form} below)
provides the standard logical constructs, in decreasing precedence:
$\begin{array}{rcl} @@ -39,14 +39,14 @@ &\mid& \isa{{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ form} ~\mid~ \isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ form} \end{array}$
-Terms are the ones we have seen all along, built from constant, variables,
+Terms are the ones we have seen all along, built from constants, variables,
function application and \isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}}-abstraction, including all the syntactic
sugar like infix symbols, \isa{if}, \isa{case} etc.
\begin{warn}
Remember that formulas are simply terms of type \isa{bool}. Hence
\isa{{\isaliteral{3D}{\isacharequal}}} also works for formulas. Beware that \isa{{\isaliteral{3D}{\isacharequal}}} has a higher
precedence than the other logical operators. Hence \isa{s\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means
-\isa{{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A}, and \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{3D}{\isacharequal}}\ A{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B}.
+\isa{{\isaliteral{28}{\isacharparenleft}}s\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A}, and \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{3D}{\isacharequal}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} means \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}B\ {\isaliteral{3D}{\isacharequal}}\ B{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A}.
Logical equivalence can also be written with
\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} instead of \isa{{\isaliteral{3D}{\isacharequal}}}, where \isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} has the same low
precedence as \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}}. Hence \isa{A\ {\isaliteral{5C3C616E643E}{\isasymand}}\ B\ {\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}\ B\ {\isaliteral{5C3C616E643E}{\isasymand}}\ A} really means
@@ -63,7 +63,7 @@
\isa{{\isaliteral{5C3C6578697374733E}{\isasymexists}}} & \xsymbol{exists} & \texttt{EX}\\
\isa{{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}} & \xsymbol{lambda} & \texttt{\%}\\
\isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} & \texttt{-{}->}\\
-\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} & \texttt{<-{}->}\\
+\isa{{\isaliteral{5C3C6C6F6E676C65667472696768746172726F773E}{\isasymlongleftrightarrow}}} & \texttt{<->}\\
\isa{{\isaliteral{5C3C616E643E}{\isasymand}}} & \texttt{/\char\\} & \texttt{\&}\\
\isa{{\isaliteral{5C3C6F723E}{\isasymor}}} & \texttt{\char\\/} & \texttt{|}\\
\isa{{\isaliteral{5C3C6E6F743E}{\isasymnot}}} & \xsymbol{not} & \texttt{\char~}\\
@@ -75,7 +75,7 @@
and the third column shows ASCII representations that stay fixed.
\begin{warn}
The implication \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} is part of the Isabelle framework. It structures
-theorems and proof states, separating assumptions from conclusion.
+theorems and proof states, separating assumptions from conclusions.
The implication \isa{{\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}} is part of the logic HOL and can occur inside the
formulas that make up the assumptions and conclusion.
Theorems should be of the form \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{3B}{\isacharsemicolon}}\ A\isaliteral{5C3C5E697375623E}{}\isactrlisub n\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ A},
@@ -86,7 +86,7 @@
\subsection{Sets}

Sets of elements of type \isa{{\isaliteral{27}{\isacharprime}}a} have type \isa{{\isaliteral{27}{\isacharprime}}a\ set}.
-They can be finite or infinite. Sets come with the usual notations:
+They can be finite or infinite. Sets come with the usual notation:
\begin{itemize}
\item \isa{e\ {\isaliteral{5C3C696E3E}{\isasymin}}\ A},\quad \isa{A\ {\isaliteral{5C3C73756273657465713E}{\isasymsubseteq}}\ B}
@@ -99,7 +99,7 @@
\begin{warn}
In \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}} the \isa{x} must be a variable. Set comprehension
involving a proper term \isa{t} must be written
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}t\ {\isaliteral{7C}{\isacharbar}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}},
+\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{7B}{\isacharbraceleft}}t\ {\isaliteral{7C}{\isacharbar}}\ x\ y\ z{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}},
where \isa{x\ y\ z} are the free variables in \isa{t}.
This is just a shorthand for \isa{{\isaliteral{7B}{\isacharbraceleft}}v{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}x\ y\ z{\isaliteral{2E}{\isachardot}}\ v\ {\isaliteral{3D}{\isacharequal}}\ t\ {\isaliteral{5C3C616E643E}{\isasymand}}\ P{\isaliteral{7D}{\isacharbraceright}}}, where
\isa{v} is a new variable.
@@ -210,8 +210,8 @@
succeeds where \isa{fastforce} fails.

The method of choice for complex logical goals is \isa{blast}. In the
-following example, \isa{T} and \isa{A} are two binary predicates, and it
-is shown that \isa{T} is total, \isa{A} is antisymmetric and \isa{T} is
+following example, \isa{T} and \isa{A} are two binary predicates. It
+is shown that if \isa{T} is total, \isa{A} is antisymmetric and \isa{T} is
a subset of \isa{A}, then \isa{A} is a subset of \isa{T}:%
\end{isamarkuptext}%
\isamarkuptrue%
@@ -449,11 +449,11 @@
automatically selects the appropriate rule for the current subgoal.

You can also turn your own theorems into introduction rules by giving them
-them \isa{intro} attribute, analogous to the \isa{simp} attribute.  In
+the \isa{intro} attribute, analogous to the \isa{simp} attribute.  In
that case \isa{blast}, \isa{fastforce} and (to a limited extent) \isa{auto} will automatically backchain with those theorems. The \isa{intro}
attribute should be used with care because it increases the search space and
-can lead to nontermination.  Sometimes it is better to use it only in a
-particular calls of \isa{blast} and friends. For example,
+can lead to nontermination.  Sometimes it is better to use it only in
+specific calls of \isa{blast} and friends. For example,
\isa{le{\isaliteral{5F}{\isacharunderscore}}trans}, transitivity of \isa{{\isaliteral{5C3C6C653E}{\isasymle}}} on type \isa{nat},
is not an introduction rule by default because of the disastrous effect
on the search space, but can be useful in specific situations:%
@@ -550,8 +550,11 @@
\label{sec:inductive-defs}

Inductive definitions are the third important definition facility, after
-datatypes and recursive function. In fact, they are the key construct in the
+datatypes and recursive function.
+\sem
+In fact, they are the key construct in the
definition of operational semantics in the second part of the book.
+\endsem

\subsection{An example: even numbers}
\label{sec:Logic:even}
@@ -639,8 +642,8 @@
case \isa{evSS} we have \mbox{\isa{m\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}}} and may assume
\isa{ev\ n}, which implies \isa{ev\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}} because \isa{m\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ n}. We did not need the induction hypothesis at all for this proof,
-it is just a case distinction on which rule was used, but having \isa{ev\ n} at our disposal in case \isa{evSS} was essential.
-This case distinction over rules is also called rule inversion''
+it is just a case analysis of which rule was used, but having \isa{ev\ n} at our disposal in case \isa{evSS} was essential.
+This case analysis of rules is also called rule inversion''
and is discussed in more detail in \autoref{ch:Isar}.

\subsubsection{In Isabelle}
@@ -789,7 +792,7 @@
definition only expresses the positive information directly. The negative
information, for example, that \isa{{\isadigit{1}}} is not even, has to be proved from
it (by induction or rule inversion). On the other hand, rule induction is
-Taylor made for proving \mbox{\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}} because it only asks you
+tailor-made for proving \mbox{\isa{ev\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n}} because it only asks you
to prove the positive cases. In the proof of \isa{even\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ n} by
computation induction via \isa{even{\isaliteral{2E}{\isachardot}}induct}, we are also presented
with the trivial negative cases. If you want the convenience of both
@@ -799,8 +802,8 @@

But many concepts do not admit a recursive definition at all because there is
no datatype for the recursion (for example, the transitive closure of a
-relation), or the recursion would not terminate (for example, the operational
-semantics in the second part of this book). Even if there is a recursive
+relation), or the recursion would not terminate (for example,
+an interpreter for a programming language). Even if there is a recursive
definition, if we are only interested in the positive information, the
inductive definition may be much simpler.

@@ -809,8 +812,11 @@

Evenness is really more conveniently expressed recursively than inductively.
As a second and very typical example of an inductive definition we define the
-reflexive transitive closure. It will also be an important building block for
+reflexive transitive closure.
+\sem
+It will also be an important building block for
some of the semantics considered in the second part of the book.
+\endsem

The reflexive transitive closure, called \isa{star} below, is a function
that maps a binary predicate to another binary predicate: if \isa{r} is of
@@ -828,8 +834,8 @@
\begin{isamarkuptext}%
The base case \isa{refl} is reflexivity: \isa{x\ {\isaliteral{3D}{\isacharequal}}\ y}. The
step case \isa{step} combines an \isa{r} step (from \isa{x} to
-\isa{y}) and a \isa{star} step (from \isa{y} to \isa{z}) into a
-\isa{star} step (from \isa{x} to \isa{z}).
+\isa{y}) and a \isa{star\ r} step (from \isa{y} to \isa{z}) into a
+\isa{star\ r} step (from \isa{x} to \isa{z}).
The \isacom{for}~\isa{r}'' in the header is merely a hint to Isabelle
that \isa{r} is a fixed parameter of \isa{star}, in contrast to the
further parameters of \isa{star}, which change. As a result, Isabelle
--- a/doc-src/ProgProve/Thys/document/Types_and_funs.tex	Mon Apr 23 23:55:06 2012 +0200
+++ b/doc-src/ProgProve/Thys/document/Types_and_funs.tex	Tue Apr 24 09:09:55 2012 +0200
@@ -169,11 +169,11 @@
subtracting \isa{f\ n} on both sides.

-Isabelle automatic termination checker requires that the arguments of
+Isabelle's automatic termination checker requires that the arguments of
recursive calls on the right-hand side must be strictly smaller than the
arguments on the left-hand side. In the simplest case, this means that one
fixed argument position decreases in size with each recursive call. The size
-is measured as the number of constructors (excluding 0-ary ones, e.g.\ \isa{Nil}). Lexicographic combinations are also recognised. In more complicated
+is measured as the number of constructors (excluding 0-ary ones, e.g.\ \isa{Nil}). Lexicographic combinations are also recognized. In more complicated
situations, the user may have to prove termination by hand. For details
see~\cite{Krauss}.

@@ -189,7 +189,7 @@
\begin{isamarkuptext}%
does not just define \isa{div{\isadigit{2}}} but also proves a
-customised induction rule:
+customized induction rule:
$\inferrule{ \mbox{\isa{P\ {\isadigit{0}}}}\\ @@ -197,7 +197,7 @@ \mbox{\isa{{\isaliteral{5C3C416E643E}{\isasymAnd}}n{\isaliteral{2E}{\isachardot}}\ P\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}}} {\mbox{\isa{P\ m}}}$
-This customised induction rule can simplify inductive proofs. For example,%
+This customized induction rule can simplify inductive proofs. For example,%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{lemma}\isamarkupfalse%
@@ -221,7 +221,7 @@
An application of \isa{auto} finishes the proof.
Had we used ordinary structural induction on \isa{n},
the proof would have needed an additional
-case distinction in the induction step.
+case analysis in the induction step.

The general case is often called \concept{computation induction},
because the induction follows the (terminating!) computation.
@@ -252,7 +252,7 @@
if the function is defined by recursion on argument number $i$.}
\end{quote}
The key heuristic, and the main point of this section, is to
-\emph{generalise the goal before induction}.
+\emph{generalize the goal before induction}.
The reason is simple: if the goal is
too specific, the induction hypothesis is too weak to allow the induction
step to go through. Let us illustrate the idea with an example.
@@ -273,12 +273,12 @@
\isacommand{fun}\isamarkupfalse%
\ itrev\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ list{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
-{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ ys\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
+{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \ \ \ \ \ \ \ ys\ {\isaliteral{3D}{\isacharequal}}\ ys{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline
{\isaliteral{22}{\isachardoublequoteopen}}itrev\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}xs{\isaliteral{29}{\isacharparenright}}\ ys\ {\isaliteral{3D}{\isacharequal}}\ itrev\ xs\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{23}{\isacharhash}}ys{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
\begin{isamarkuptext}%
The behaviour of \isa{itrev} is simple: it reverses
its first argument by stacking its elements onto the second argument,
-and returning that second argument when the first one becomes
+and it returns that second argument when the first one becomes
empty. Note that \isa{itrev} is tail-recursive: it can be
compiled into a loop, no stack is necessary for executing it.

@@ -312,10 +312,10 @@
argument,~\isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, prevents it from rewriting the conclusion.
This example suggests a heuristic:
\begin{quote}
-\emph{Generalise goals for induction by replacing constants by variables.}
+\emph{Generalize goals for induction by replacing constants by variables.}
\end{quote}
Of course one cannot do this na\"{\i}vely: \isa{itrev\ xs\ ys\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs} is
-just not true.  The correct generalisation is%
+just not true.  The correct generalization is%
\end{isamarkuptxt}%
\isamarkuptrue%
%
@@ -336,7 +336,7 @@
\begin{isamarkuptxt}%
If \isa{ys} is replaced by \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}}, the right-hand side simplifies to
\isa{rev\ xs}, as required.
-In this instance it was easy to guess the right generalisation.
+In this instance it was easy to guess the right generalization.
Other situations can require a good deal of creativity.

Although we now have two variables, only \isa{xs} is suitable for
@@ -348,12 +348,12 @@
\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ \ \ \ }itrev\ xs\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{23}{\isacharhash}}\ ys{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ rev\ xs\ {\isaliteral{40}{\isacharat}}\ a\ {\isaliteral{23}{\isacharhash}}\ ys%
\end{isabelle}
The induction hypothesis is still too weak, but this time it takes no
-intuition to generalise: the problem is that the \isa{ys}
+intuition to generalize: the problem is that the \isa{ys}
in the induction hypothesis is fixed,
but the induction hypothesis needs to be applied with
\isa{a\ {\isaliteral{23}{\isacharhash}}\ ys} instead of \isa{ys}. Hence we prove the theorem
for all \isa{ys} instead of a fixed one. We can instruct induction
-to perform this generalisation for us by adding \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ ys}.%
+to perform this generalization for us by adding \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ ys}.%
\end{isamarkuptxt}%
\isamarkuptrue%
%
@@ -394,12 +394,12 @@
%
\begin{isamarkuptext}%
-This leads to another heuristic for generalisation:
+This leads to another heuristic for generalization:
\begin{quote}
-\emph{Generalise induction by generalising all free
+\emph{Generalize induction by generalizing all free
variables\\ {\em(except the induction variable itself)}.}
\end{quote}
-Generalisation is best performed with \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub k}.
+Generalization is best performed with \isa{arbitrary{\isaliteral{3A}{\isacharcolon}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{5C3C646F74733E}{\isasymdots}}\ y\isaliteral{5C3C5E697375623E}{}\isactrlisub k}.
This heuristic prevents trivial failures like the one above.
However, it should not be applied blindly.
It is not always required, and the additional quantifiers can complicate
@@ -413,7 +413,7 @@
\item using equations $l = r$ from left to right (only),
\item as long as possible.
\end{itemize}
-To emphasise the directionality, equations that have been given the
+To emphasize the directionality, equations that have been given the
\isa{simp} attribute are called \concept{simplification}
rules. Logically, they are still symmetric, but proofs by
simplification use them only in the left-to-right direction.  The proof tool