# HG changeset patch # User nipkow # Date 1400437744 -7200 # Node ID fafcf43ded4aec6b60d3e835a54fbea238c92a87 # Parent e8c0d894a205f67d2ed53b5f75ee66a18fc03ff7 typos diff -r e8c0d894a205 -r fafcf43ded4a src/Doc/Prog_Prove/Basics.thy --- a/src/Doc/Prog_Prove/Basics.thy Sun May 18 17:01:37 2014 +0200 +++ b/src/Doc/Prog_Prove/Basics.thy Sun May 18 20:29:04 2014 +0200 @@ -27,7 +27,7 @@ \item[function types,] denoted by @{text"\"}. \item[type variables,] - denoted by @{typ 'a}, @{typ 'b} etc., just like in ML\@. + denoted by @{typ 'a}, @{typ 'b}, etc., just like in ML\@. \end{description} Note that @{typ"'a \ 'b list"} means @{typ[source]"'a \ ('b list)"}, not @{typ"('a \ 'b) list"}: postfix type constructors have precedence @@ -87,7 +87,7 @@ Right-arrows of all kinds always associate to the right. In particular, the formula @{text"A\<^sub>1 \ A\<^sub>2 \ A\<^sub>3"} means @{text "A\<^sub>1 \ (A\<^sub>2 \ A\<^sub>3)"}. -The (Isabelle specific) notation \mbox{@{text"\ A\<^sub>1; \; A\<^sub>n \ \ A"}} +The (Isabelle-specific) notation \mbox{@{text"\ A\<^sub>1; \; A\<^sub>n \ \ A"}} is short for the iterated implication \mbox{@{text"A\<^sub>1 \ \ \ A\<^sub>n \ A"}}. Sometimes we also employ inference rule notation: \inferrule{\mbox{@{text "A\<^sub>1"}}\\ \mbox{@{text "\"}}\\ \mbox{@{text "A\<^sub>n"}}} diff -r e8c0d894a205 -r fafcf43ded4a src/Doc/Prog_Prove/Bool_nat_list.thy --- a/src/Doc/Prog_Prove/Bool_nat_list.thy Sun May 18 17:01:37 2014 +0200 +++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Sun May 18 20:29:04 2014 +0200 @@ -18,7 +18,7 @@ @{datatype[display] bool} with the two values \indexed{@{const True}}{True} and \indexed{@{const False}}{False} and with many predefined functions: @{text "\"}, @{text "\"}, @{text "\"}, @{text -"\"} etc. Here is how conjunction could be defined by pattern matching: +"\"}, etc. Here is how conjunction could be defined by pattern matching: *} fun conj :: "bool \ bool \ bool" where @@ -34,7 +34,7 @@ @{datatype[display] nat}\index{Suc@@{const Suc}} All values of type @{typ nat} are generated by the constructors @{text 0} and @{const Suc}. Thus the values of type @{typ nat} are -@{text 0}, @{term"Suc 0"}, @{term"Suc(Suc 0)"} etc. +@{text 0}, @{term"Suc 0"}, @{term"Suc(Suc 0)"}, etc. There are many predefined functions: @{text "+"}, @{text "*"}, @{text "\"}, etc. Here is how you could define your own addition: *} @@ -80,7 +80,7 @@ txt{* which displays @{thm[show_question_marks,display] add_02} The free variable @{text m} has been replaced by the \concept{unknown} -@{text"?m"}. There is no logical difference between the two but an +@{text"?m"}. There is no logical difference between the two but there is an operational one: unknowns can be instantiated, which is what you want after some lemma has been proved. @@ -165,7 +165,7 @@ \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. +or @{term"Cons x (Cons y Nil)"}, etc. \item \isacom{datatype} requires no quotation marks on the left-hand side, but on the right-hand side each of the argument types of a constructor needs to be enclosed in quotation marks, unless @@ -196,12 +196,12 @@ \medskip Figure~\ref{fig:MyList} shows the theory created so far. -Because @{text list}, @{const Nil}, @{const Cons} etc are already predefined, +Because @{text list}, @{const Nil}, @{const Cons}, etc.\ are already predefined, Isabelle prints qualified (long) names when executing this theory, for example, @{text MyList.Nil} instead of @{const Nil}. To suppress the qualified names you can insert the command \texttt{declare [[names\_short]]}. - This is not recommended in general but just for this unusual example. + This is not recommended in general but is convenient for this unusual example. % Notice where the %quotations marks are needed that we mostly sweep under the carpet. In %particular, notice that \isacom{datatype} requires no quotation marks on the diff -r e8c0d894a205 -r fafcf43ded4a src/Doc/Prog_Prove/Isar.thy --- a/src/Doc/Prog_Prove/Isar.thy Sun May 18 17:01:37 2014 +0200 +++ b/src/Doc/Prog_Prove/Isar.thy Sun May 18 20:29:04 2014 +0200 @@ -9,7 +9,7 @@ for larger proofs is \concept{Isar}. The two key features of Isar are: \begin{itemize} \item It is structured, not linear. -\item It is readable without running it because +\item It is readable without its being run because you need to state what you are proving at any given point. \end{itemize} Whereas apply-scripts are like assembly language programs, Isar proofs @@ -57,7 +57,7 @@ \noindent A proof can either be an atomic \isacom{by} with a single proof method which must finish off the statement being proved, for example @{text -auto}. Or it can be a \isacom{proof}--\isacom{qed} block of multiple +auto}, or it can be a \isacom{proof}--\isacom{qed} block of multiple steps. Such a block can optionally begin with a proof method that indicates how to start off the proof, e.g.\ \mbox{@{text"(induction xs)"}}. @@ -65,10 +65,10 @@ together with its proof. The optional \isacom{from} clause indicates which facts are to be used in the proof. Intermediate propositions are stated with \isacom{have}, the overall goal -with \isacom{show}. A step can also introduce new local variables with +is stated with \isacom{show}. A step can also introduce new local variables with \isacom{fix}. Logically, \isacom{fix} introduces @{text"\"}-quantified variables, \isacom{assume} introduces the assumption of an implication -(@{text"\"}) and \isacom{have}/\isacom{show} the conclusion. +(@{text"\"}) and \isacom{have}/\isacom{show} introduce the conclusion. Propositions are optionally named formulas. These names can be referred to in later \isacom{from} clauses. In the simplest case, a fact is such a name. @@ -81,7 +81,7 @@ Fact names can stand for whole lists of facts. For example, if @{text f} is defined by command \isacom{fun}, @{text"f.simps"} refers to the whole list of recursion equations defining @{text f}. Individual facts can be selected by -writing @{text"f.simps(2)"}, whole sublists by @{text"f.simps(2-4)"}. +writing @{text"f.simps(2)"}, whole sublists by writing @{text"f.simps(2-4)"}. \section{Isar by Example} @@ -100,7 +100,7 @@ qed text{* -The \isacom{proof} command lacks an explicit method how to perform +The \isacom{proof} command lacks an explicit method by which to perform the proof. In such cases Isabelle tries to use some standard introduction rule, in the above case for @{text"\"}: \[ @@ -206,7 +206,7 @@ text{* \begin{warn} Note the hyphen after the \isacom{proof} command. -It is the null method that does nothing to the goal. Leaving it out would ask +It is the null method that does nothing to the goal. Leaving it out would be asking Isabelle to try some suitable introduction rule on the goal @{const False}---but there is no such rule and \isacom{proof} would fail. \end{warn} @@ -217,7 +217,7 @@ Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer -to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc, +to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc.\ thus obviating the need to name them individually. \section{Proof Patterns} @@ -489,7 +489,7 @@ $\vdots$\\ \isacom{from} @{text "x_gr_0"} \dots \end{quote} -The name is longer than the fact it stands for! Short facts do not need names, +The name is longer than the fact it stands for! Short facts do not need names; one can refer to them easily by quoting them: \begin{quote} \isacom{have} \ @{text"\"x > 0\""}\\ @@ -544,8 +544,8 @@ \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 +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 generalized over its locally fixed variables at the end. This is what a \concept{raw proof block} does: \begin{quote}\index{$IMP053@@{text"{ ... }"} (proof block)} @@ -780,7 +780,7 @@ \isacom{let} @{text"?case = \"P(Suc n)\""} \end{quote} The list of assumptions @{text Suc} is actually subdivided -into @{text"Suc.IH"}, the induction hypotheses (here @{text"A(n) \ P(n)"}) +into @{text"Suc.IH"}, the induction hypotheses (here @{text"A(n) \ P(n)"}), and @{text"Suc.prems"}, the premises of the goal being proved (here @{text"A(Suc n)"}). @@ -986,7 +986,7 @@ Let us examine the assumptions available in each case. In case @{text ev0} we have @{text"n = 0"} and in case @{text evSS} we have @{prop"n = Suc(Suc k)"} and @{prop"ev k"}. In each case the assumptions are available under the name -of the case; there is no fine grained naming schema like for induction. +of the case; there is no fine-grained naming schema like there is for induction. Sometimes some rules could not have been used to derive the given fact because constructors clash. As an extreme example consider @@ -1030,7 +1030,7 @@ \begin{isabelle} \isacom{lemma} @{text[source]"I x y z \ x = r \ y = s \ z = t \ \"} \end{isabelle} -Standard rule induction will worke fine now, provided the free variables in +Standard rule induction will work fine now, provided the free variables in @{text r}, @{text s}, @{text t} are generalized via @{text"arbitrary"}. However, induction can do the above transformation for us, behind the curtains, so we never @@ -1077,7 +1077,8 @@ \begin{warn} This advanced form of induction does not support the @{text IH} naming schema explained in \autoref{sec:assm-naming}: -the induction hypotheses are instead found under the name @{text hyps}, like for the simpler +the induction hypotheses are instead found under the name @{text hyps}, +as they are for the simpler @{text induct} method. \end{warn} \index{induction|)} @@ -1109,7 +1110,7 @@ \begin{exercise} Recall predicate @{text star} from \autoref{sec:star} and @{text iter} from Exercise~\ref{exe:iter}. Prove @{prop "iter r n x y \ star r x y"} -in a structured style, do not just sledgehammer each case of the +in a structured style; do not just sledgehammer each case of the required induction. \end{exercise} diff -r e8c0d894a205 -r fafcf43ded4a src/Doc/Prog_Prove/Logic.thy --- a/src/Doc/Prog_Prove/Logic.thy Sun May 18 17:01:37 2014 +0200 +++ b/src/Doc/Prog_Prove/Logic.thy Sun May 18 20:29:04 2014 +0200 @@ -26,7 +26,7 @@ \] Terms are the ones we have seen all along, built from constants, variables, function application and @{text"\"}-abstraction, including all the syntactic -sugar like infix symbols, @{text "if"}, @{text "case"} etc. +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 @@ -155,7 +155,7 @@ Define a function @{text "set ::"} @{typ "'a tree \ 'a set"} that returns the elements in a tree and a function @{text "ord ::"} @{typ "int tree \ bool"} -the tests if an @{typ "int tree"} is ordered. +that tests if an @{typ "int tree"} is ordered. Define a function @{text ins} that inserts an element into an ordered @{typ "int tree"} while maintaining the order of the tree. If the element is already in the tree, the @@ -259,7 +259,7 @@ not the translations from Isabelle's logic to those tools!) and insists on a proof that it can check. This is what \indexed{@{text metis}}{metis} does. It is given a list of lemmas and tries to find a proof just using those lemmas -(and pure logic). In contrast to @{text simp} and friends that know a lot of +(and pure logic). In contrast to using @{text simp} and friends who know a lot of lemmas already, using @{text metis} manually is tedious because one has to find all the relevant lemmas first. But that is precisely what \isacom{sledgehammer} does for us. @@ -284,7 +284,7 @@ connectives @{text"\"}, @{text"\"}, @{text"\"}, @{text"\"}, @{text"\"}. Strictly speaking, this is known as \concept{linear arithmetic} because it does not involve multiplication, although multiplication with -numbers, e.g.\ @{text"2*n"} is allowed. Such formulas can be proved by +numbers, e.g.\ @{text"2*n"}, is allowed. Such formulas can be proved by \indexed{@{text arith}}{arith}: *} @@ -588,9 +588,9 @@ from @{prop"ev 0"} because @{prop"0 - 2 = (0::nat)"} on type @{typ nat}. In 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 analysis of which rule was used, but having @{prop"ev -n"} at our disposal in case @{thm[source]evSS} was essential. +2) - 2 = n"}. We did not need the induction hypothesis at all for this proof (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 analysis of rules is also called ``rule inversion'' and is discussed in more detail in \autoref{ch:Isar}. @@ -844,8 +844,8 @@ \] as two inductive predicates. If you think of @{text a} and @{text b} as ``@{text "("}'' and ``@{text ")"}'', -the grammars defines strings of balanced parentheses. -Prove @{prop"T w \ S w"} and @{prop "S w \ T w"} separately and conclude +the grammar defines strings of balanced parentheses. +Prove @{prop"T w \ S w"} and \mbox{@{prop "S w \ T w"}} separately and conclude @{prop "S w = T w"}. \end{exercise} diff -r e8c0d894a205 -r fafcf43ded4a src/Doc/Prog_Prove/Types_and_funs.thy --- a/src/Doc/Prog_Prove/Types_and_funs.thy Sun May 18 17:01:37 2014 +0200 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy Sun May 18 20:29:04 2014 +0200 @@ -99,7 +99,7 @@ \subsection{Definitions} -Non recursive functions can be defined as in the following example: +Non-recursive functions can be defined as in the following example: \index{definition@\isacom{definition}}*} definition sq :: "nat \ nat" where @@ -133,7 +133,7 @@ \label{sec:recursive-funs} Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching -over datatype constructors. The order of equations matters. Just as in +over datatype constructors. The order of equations matters, as in functional programming languages. However, all HOL functions must be total. This simplifies the logic---terms are always defined---but means that recursive functions must terminate. Otherwise one could define a @@ -175,7 +175,7 @@ apply(induction n rule: div2.induct) txt{* (where the infix @{text div} is the predefined division operation) -yields the 3 subgoals +yields the subgoals @{subgoals[display,margin=65]} An application of @{text auto} finishes the proof. Had we used ordinary structural induction on @{text n}, @@ -271,7 +271,7 @@ its first argument by stacking its elements onto the second argument, 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. +compiled into a loop; no stack is necessary for executing it. Naturally, we would like to show that @{const itrev} does indeed reverse its first argument provided the second one is empty: @@ -487,7 +487,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} @@ -557,7 +557,7 @@ Find an equation expressing the size of a tree after exploding it (\noquotes{@{term [source] "nodes (explode n t)"}}) as a function of @{term "nodes t"} and @{text n}. Prove your equation. -You may use the usual arithmetic operators including the exponentiation +You may use the usual arithmetic operators, including the exponentiation operator ``@{text"^"}''. For example, \noquotes{@{prop [source] "2 ^ 2 = 4"}}. Hint: simplifying with the list of theorems @{thm[source] algebra_simps} diff -r e8c0d894a205 -r fafcf43ded4a src/Doc/Prog_Prove/document/intro-isabelle.tex --- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Sun May 18 17:01:37 2014 +0200 +++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Sun May 18 20:29:04 2014 +0200 @@ -3,7 +3,7 @@ of Isabelle for HOL, which abbreviates Higher-Order Logic. We introduce HOL step by step following the equation \[ \mbox{HOL} = \mbox{Functional Programming} + \mbox{Logic}. \] -We assume that the reader is used to logical and set theoretic notation +We assume that the reader is used to logical and set-theoretic notation and is familiar with the basic concepts of functional programming. \ifsem Open-minded readers have been known to pick up functional @@ -20,8 +20,8 @@ optimization and compilation. \fi \autoref{ch:Logic} introduces the rest of HOL: the -language of formulas beyond equality, automatic proof tools, single -step proofs, and inductive definitions, an essential specification construct. +language of formulas beyond equality, automatic proof tools, single-step +proofs, and inductive definitions, an essential specification construct. \autoref{ch:Isar} introduces Isar, Isabelle's language for writing structured proofs.