all headings in upper case
Mon, 10 Jun 2013 16:04:18 +0200
changeset 52361 7d5ad23b8245
parent 52357 a5d3730043c2
child 52362 6b80ba92c4fe
all headings in upper case
--- 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 @@
-\subsection{Types, Terms and Formulae}
+\subsection{Types, Terms and Formulas}
 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 @@
-\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}
 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 @@
-\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)\""}
-\subsection{Rule induction}
+\subsection{Rule Induction}
 Recall the inductive and recursive definitions of even numbers in
@@ -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}
 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}
 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}
 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
@@ -271,7 +271,7 @@
 There is also a lightweight variant \isacom{try0} that does not call
-\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 @@
 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 @@
 Of course this is just an example and could be proved by @{text arith}, too.
-\subsection{Forward proof}
+\subsection{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 @@
-\section{Inductive definitions}
+\section{Inductive Definitions}
 Inductive definitions are the third important definition facility, after
@@ -460,7 +460,7 @@
 definition of operational semantics in the second part of the book.
-\subsection{An example: even numbers}
+\subsection{An Example: Even Numbers}
 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"}
-\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}
 Evenness is really more conveniently expressed recursively than inductively.
@@ -709,7 +709,7 @@
-\subsection{The general case}
+\subsection{The General Case}
 Inductive definitions have approximately the following general form:
--- 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 @@
-\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}
 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}
 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}
 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