--- a/src/Doc/ProgProve/Basics.thy Mon Jun 10 08:39:48 2013 -0400
+++ b/src/Doc/ProgProve/Basics.thy Mon Jun 10 16:04:18 2013 +0200
@@ -9,7 +9,7 @@
\section{Basics}
-\subsection{Types, Terms and Formulae}
+\subsection{Types, Terms and Formulas}
\label{sec:TypesTermsForms}
HOL is a typed logic whose type system resembles that of functional
@@ -58,7 +58,7 @@
Terms may also contain @{text "\<lambda>"}-abstractions. For example,
@{term "\<lambda>x. x"} is the identity function.
-\concept{Formulae} are terms of type @{text bool}.
+\concept{Formulas} are terms of type @{text bool}.
There are the basic constants @{term True} and @{term False} and
the usual logical connectives (in decreasing order of precedence):
@{text"\<not>"}, @{text"\<and>"}, @{text"\<or>"}, @{text"\<longrightarrow>"}.
@@ -133,7 +133,7 @@
The textual definition of a theory follows a fixed syntax with keywords like
\isacommand{begin} and \isacommand{datatype}. Embedded in this syntax are
-the types and formulae of HOL. To distinguish the two levels, everything
+the types and formulas of HOL. To distinguish the two levels, everything
HOL-specific (terms and types) must be enclosed in quotation marks:
\texttt{"}\dots\texttt{"}. To lessen this burden, quotation marks around a
single identifier can be dropped. When Isabelle prints a syntax error
--- a/src/Doc/ProgProve/Bool_nat_list.thy Mon Jun 10 08:39:48 2013 -0400
+++ b/src/Doc/ProgProve/Bool_nat_list.thy Mon Jun 10 16:04:18 2013 +0200
@@ -109,7 +109,7 @@
overloaded.
\end{warn}
-\subsubsection{An informal proof}
+\subsubsection{An Informal Proof}
Above we gave some terse informal explanation of the proof of
@{prop"add m 0 = m"}. A more detailed informal exposition of the lemma
@@ -335,7 +335,7 @@
Finally the proofs of @{thm[source] rev_app} and @{thm[source] rev_rev}
succeed, too.
-\subsubsection{Another informal proof}
+\subsubsection{Another Informal Proof}
Here is the informal proof of associativity of @{const app}
corresponding to the Isabelle proof above.
@@ -377,7 +377,7 @@
@{text s} is @{term"app (app Nil ys) zs"}, @{text t} is @{term"app Nil (app
ys zs)"}, and @{text u} is @{term"app ys zs"}.
-\subsection{Predefined lists}
+\subsection{Predefined Lists}
\label{sec:predeflists}
Isabelle's predefined lists are the same as the ones above, but with
--- a/src/Doc/ProgProve/Isar.thy Mon Jun 10 08:39:48 2013 -0400
+++ b/src/Doc/ProgProve/Isar.thy Mon Jun 10 16:04:18 2013 +0200
@@ -84,7 +84,7 @@
writing @{text"f.simps(2)"}, whole sublists by @{text"f.simps(2-4)"}.
-\section{Isar by example}
+\section{Isar by Example}
We show a number of proofs of Cantor's theorem that a function from a set to
its powerset cannot be surjective, illustrating various features of Isar. The
@@ -175,7 +175,7 @@
\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}}
+\subsection{Structured Lemma Statements: \isacom{fixes}, \isacom{assumes}, \isacom{shows}}
Lemmas can also be stated in a more structured fashion. To demonstrate this
feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}
@@ -221,7 +221,7 @@
to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc,
thus obviating the need to name them individually.
-\section{Proof patterns}
+\section{Proof Patterns}
We show a number of important basic proof patterns. Many of them arise from
the rules of natural deduction that are applied by \isacom{proof} by
@@ -428,9 +428,9 @@
\end{minipage}
\end{tabular}
\begin{isamarkuptext}%
-\section{Streamlining proofs}
+\section{Streamlining Proofs}
-\subsection{Pattern matching and quotations}
+\subsection{Pattern Matching and Quotations}
In the proof patterns shown above, formulas are often duplicated.
This can make the text harder to read, write and maintain. Pattern matching
@@ -544,7 +544,7 @@
The \isacom{moreover} version is no shorter but expresses the structure more
clearly and avoids new names.
-\subsection{Raw proof blocks}
+\subsection{Raw Proof Blocks}
Sometimes one would like to prove some lemma locally within a proof.
A lemma that shares the current context of assumptions but that
@@ -590,9 +590,9 @@
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 analysis and induction}
+\section{Case Analysis and Induction}
-\subsection{Datatype case analysis}
+\subsection{Datatype Case Analysis}
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"},
@@ -642,7 +642,7 @@
are not used because they are directly piped (via \isacom{thus})
into the proof of the claim.
-\subsection{Structural induction}
+\subsection{Structural Induction}
We illustrate structural induction with an example based on natural numbers:
the sum (@{text"\<Sum>"}) of the first @{text n} natural numbers
@@ -768,7 +768,7 @@
\item \isacom{let} @{text"?case = \"P(C x\<^isub>1 \<dots> x\<^isub>n)\""}
\end{enumerate}
-\subsection{Rule induction}
+\subsection{Rule Induction}
Recall the inductive and recursive definitions of even numbers in
\autoref{sec:inductive-defs}:
@@ -893,7 +893,7 @@
free variables in rule @{text i} to @{text"x\<^isub>1 \<dots> x\<^isub>k"},
going through rule @{text i} from left to right.
-\subsection{Assumption naming}
+\subsection{Assumption Naming}
\label{sec:assm-naming}
In any induction, \isacom{case}~@{text name} sets up a list of assumptions
@@ -919,7 +919,8 @@
This is where the indexing of fact lists comes in handy, e.g.\
@{text"name.IH(2)"} or @{text"name.prems(1-2)"}.
-\subsection{Rule inversion}
+\subsection{Rule Inversion}
+\label{sec:rule-inversion}
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
@@ -980,7 +981,7 @@
text{* Normally not all cases will be impossible. As a simple exercise,
prove that \mbox{@{prop"\<not> ev(Suc(Suc(Suc 0)))"}.}
-\subsection{Advanced rule induction}
+\subsection{Advanced Rule Induction}
\label{sec:advanced-rule-induction}
So far, rule induction was always applied to goals of the form @{text"I x y z \<Longrightarrow> \<dots>"}
--- a/src/Doc/ProgProve/Logic.thy Mon Jun 10 08:39:48 2013 -0400
+++ b/src/Doc/ProgProve/Logic.thy Mon Jun 10 16:04:18 2013 +0200
@@ -119,7 +119,7 @@
See \cite{Nipkow-Main} for the wealth of further predefined functions in theory
@{theory Main}.
-\section{Proof automation}
+\section{Proof Automation}
So far we have only seen @{text simp} and @{text auto}: Both perform
rewriting, both can also prove linear arithmetic facts (no multiplication),
@@ -258,7 +258,7 @@
but we will not enlarge on that here.
-\subsection{Trying them all}
+\subsection{Trying Them All}
If you want to try all of the above automatic proof methods you simply type
\begin{isabelle}
@@ -271,7 +271,7 @@
There is also a lightweight variant \isacom{try0} that does not call
sledgehammer.
-\section{Single step proofs}
+\section{Single Step Proofs}
Although automation is nice, it often fails, at least initially, and you need
to find out why. When @{text fastforce} or @{text blast} simply fail, you have
@@ -284,7 +284,7 @@
\]
to the proof state. We will now examine the details of this process.
-\subsection{Instantiating unknowns}
+\subsection{Instantiating Unknowns}
We had briefly mentioned earlier that after proving some theorem,
Isabelle replaces all free variables @{text x} by so called \concept{unknowns}
@@ -312,7 +312,7 @@
@{text "conjI[where ?P = \"a=b\" and ?Q = \"False\"]"}.
-\subsection{Rule application}
+\subsection{Rule Application}
\concept{Rule application} means applying a rule backwards to a proof state.
For example, applying rule @{thm[source]conjI} to a proof state
@@ -338,7 +338,7 @@
\end{quote}
This is also called \concept{backchaining} with rule @{text xyz}.
-\subsection{Introduction rules}
+\subsection{Introduction Rules}
Conjunction introduction (@{thm[source] conjI}) is one example of a whole
class of rules known as \concept{introduction rules}. They explain under which
@@ -388,7 +388,7 @@
text{*
Of course this is just an example and could be proved by @{text arith}, too.
-\subsection{Forward proof}
+\subsection{Forward Proof}
\label{sec:forward-proof}
Forward proof means deriving new theorems from old theorems. We have already
@@ -437,7 +437,7 @@
text{* In this particular example we could have backchained with
@{thm[source] Suc_leD}, too, but because the premise is more complicated than the conclusion this can easily lead to nontermination.
-\subsection{Finding theorems}
+\subsection{Finding Theorems}
Command \isacom{find{\isacharunderscorekeyword}theorems} searches for specific theorems in the current
theory. Search criteria include pattern matching on terms and on names.
@@ -450,7 +450,7 @@
\end{warn}
-\section{Inductive definitions}
+\section{Inductive Definitions}
\label{sec:inductive-defs}
Inductive definitions are the third important definition facility, after
@@ -460,7 +460,7 @@
definition of operational semantics in the second part of the book.
\endsem
-\subsection{An example: even numbers}
+\subsection{An Example: Even Numbers}
\label{sec:Logic:even}
Here is a simple example of an inductively defined predicate:
@@ -486,7 +486,7 @@
@{text "ev 0 \<Longrightarrow> ev (0 + 2) \<Longrightarrow> ev((0 + 2) + 2) = ev 4"}
\end{quote}
-\subsubsection{Rule induction}
+\subsubsection{Rule Induction}
Showing that all even numbers have some property is more complicated. For
example, let us prove that the inductive definition of even numbers agrees
@@ -617,7 +617,7 @@
default because, in contrast to recursive functions, there is no termination
requirement for inductive definitions.
-\subsubsection{Inductive versus recursive}
+\subsubsection{Inductive Versus Recursive}
We have seen two definitions of the notion of evenness, an inductive and a
recursive one. Which one is better? Much of the time, the recursive one is
@@ -642,7 +642,7 @@
definition, if we are only interested in the positive information, the
inductive definition may be much simpler.
-\subsection{The reflexive transitive closure}
+\subsection{The Reflexive Transitive Closure}
\label{sec:star}
Evenness is really more conveniently expressed recursively than inductively.
@@ -709,7 +709,7 @@
text{*
-\subsection{The general case}
+\subsection{The General Case}
Inductive definitions have approximately the following general form:
\begin{quote}
--- a/src/Doc/ProgProve/Types_and_funs.thy Mon Jun 10 08:39:48 2013 -0400
+++ b/src/Doc/ProgProve/Types_and_funs.thy Mon Jun 10 16:04:18 2013 +0200
@@ -5,7 +5,7 @@
(*>*)
text{*
\vspace{-5ex}
-\section{Type and function definitions}
+\section{Type and Function Definitions}
Type synonyms are abbreviations for existing types, for example
*}
@@ -129,7 +129,7 @@
The ASCII representation of @{text"\<equiv>"} is \texttt{==} or \xsymbol{equiv}.
-\subsection{Recursive functions}
+\subsection{Recursive Functions}
\label{sec:recursive-funs}
Recursive functions are defined with \isacom{fun} by pattern matching
@@ -200,7 +200,7 @@
But note that the induction rule does not mention @{text f} at all,
except in its name, and is applicable independently of @{text f}.
-\section{Induction heuristics}
+\section{Induction Heuristics}
We have already noted that theorems about recursive functions are proved by
induction. In case the function has more than one argument, we have followed
@@ -345,7 +345,7 @@
Simplification is often also called \concept{rewriting}
and simplification rules \concept{rewrite rules}.
-\subsection{Simplification rules}
+\subsection{Simplification Rules}
The attribute @{text"simp"} declares theorems to be simplification rules,
which the simplifier will use automatically. In addition,
@@ -363,7 +363,7 @@
Distributivity laws, for example, alter the structure of terms
and can produce an exponential blow-up.
-\subsection{Conditional simplification rules}
+\subsection{Conditional Simplification Rules}
Simplification rules can be conditional. Before applying such a rule, the
simplifier will first try to prove the preconditions, again by
@@ -401,7 +401,7 @@
leads to nontermination: when trying to rewrite @{prop"n<m"} to @{const True}
one first has to prove \mbox{@{prop"Suc n < m"}}, which can be rewritten to @{const True} provided @{prop"Suc(Suc n) < m"}, \emph{ad infinitum}.
-\subsection{The @{text simp} proof method}
+\subsection{The @{text simp} Proof Method}
\label{sec:simp}
So far we have only used the proof method @{text auto}. Method @{text simp}
@@ -436,7 +436,7 @@
subgoals. There is also @{text simp_all}, which applies @{text simp} to
all subgoals.
-\subsection{Rewriting with definitions}
+\subsection{Rewriting With Definitions}
\label{sec:rewr-defs}
Definitions introduced by the command \isacom{definition}
@@ -457,7 +457,7 @@
In particular, let-expressions can be unfolded by
making @{thm[source] Let_def} a simplification rule.
-\subsection{Case splitting with @{text simp}}
+\subsection{Case Splitting With @{text simp}}
Goals containing if-expressions are automatically split into two cases by
@{text simp} using the rule