# HG changeset patch # User nipkow # Date 1370873074 -7200 # Node ID 6b80ba92c4fe95d29579e6c3f89a173a56f9a77c # Parent ac7ac2b242a2dfdcdac1f75224af91778649fc72# Parent 7d5ad23b8245162922f3c9f9283d3be72453c9c5 merged diff -r ac7ac2b242a2 -r 6b80ba92c4fe src/Doc/ProgProve/Basics.thy --- a/src/Doc/ProgProve/Basics.thy Mon Jun 10 06:08:17 2013 -0700 +++ b/src/Doc/ProgProve/Basics.thy Mon Jun 10 16:04:34 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 "\"}-abstractions. For example, @{term "\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"\"}, @{text"\"}, @{text"\"}, @{text"\"}. @@ -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 diff -r ac7ac2b242a2 -r 6b80ba92c4fe src/Doc/ProgProve/Bool_nat_list.thy --- a/src/Doc/ProgProve/Bool_nat_list.thy Mon Jun 10 06:08:17 2013 -0700 +++ b/src/Doc/ProgProve/Bool_nat_list.thy Mon Jun 10 16:04:34 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 diff -r ac7ac2b242a2 -r 6b80ba92c4fe src/Doc/ProgProve/Isar.thy --- a/src/Doc/ProgProve/Isar.thy Mon Jun 10 06:08:17 2013 -0700 +++ b/src/Doc/ProgProve/Isar.thy Mon Jun 10 16:04:34 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"\ 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"\"}) of the first @{text n} natural numbers @@ -768,7 +768,7 @@ \item \isacom{let} @{text"?case = \"P(C x\<^isub>1 \ 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 \ 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"\ 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 \ \"} diff -r ac7ac2b242a2 -r 6b80ba92c4fe src/Doc/ProgProve/Logic.thy --- a/src/Doc/ProgProve/Logic.thy Mon Jun 10 06:08:17 2013 -0700 +++ b/src/Doc/ProgProve/Logic.thy Mon Jun 10 16:04:34 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 \ ev (0 + 2) \ 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} diff -r ac7ac2b242a2 -r 6b80ba92c4fe src/Doc/ProgProve/Types_and_funs.thy --- a/src/Doc/ProgProve/Types_and_funs.thy Mon Jun 10 06:08:17 2013 -0700 +++ b/src/Doc/ProgProve/Types_and_funs.thy Mon Jun 10 16:04:34 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"\"} 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