
diff -r 4ced56100757 -r c1cca2a052e4 doc-src/ProgProve/Thys/document/Logic.tex
--- 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{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}},\quad \isa{{\isaliteral{7B}{\isacharbraceleft}}e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}{\isaliteral{2C}{\isacharcomma}}{\isaliteral{5C3C646F74733E}{\isasymdots}}{\isaliteral{2C}{\isacharcomma}}e\isaliteral{5C3C5E697375623E}{}\isactrlisub n{\isaliteral{7D}{\isacharbraceright}}}
 \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 @@
 from \isa{ev\ {\isadigit{0}}} because \isa{{\isadigit{0}}\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}} on type \isa{nat}. In
 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




