summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 06 Oct 2014 19:40:22 +0200 | |

changeset 58603 | bca419a7f9eb |

parent 58601 | 85fa90262807 (current diff) |

parent 58602 | ab56811d76c6 (diff) |

child 58604 | 13dfea1621b2 |

merged

--- a/src/Doc/Prog_Prove/Isar.thy Mon Oct 06 19:19:16 2014 +0200 +++ b/src/Doc/Prog_Prove/Isar.thy Mon Oct 06 19:40:22 2014 +0200 @@ -73,7 +73,7 @@ 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. But facts can also be composed with @{text OF} and @{text of} as shown in -\autoref{sec:forward-proof}---hence the \dots\ in the above grammar. Note +\autoref{sec:forward-proof} --- hence the \dots\ in the above grammar. Note that assumptions, intermediate \isacom{have} statements and global lemmas all have the same status and are thus collectively referred to as \conceptidx{facts}{fact}. @@ -110,7 +110,7 @@ \] In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}. Thus we may assume @{prop"surj f"}. The proof shows that names of propositions -may be (single!) digits---meaningful names are hard to invent and are often +may be (single!) digits --- meaningful names are hard to invent and are often not necessary. Both \isacom{have} steps are obvious. The second one introduces the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof. If you wonder why @{text 2} directly implies @{text False}: from @{text 2} @@ -207,7 +207,7 @@ \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 be asking -Isabelle to try some suitable introduction rule on the goal @{const False}---but +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} In the \isacom{have} step the assumption @{prop"surj f"} is now @@ -945,7 +945,7 @@ \end{warn} More complicated inductive proofs than the ones we have seen so far -often need to refer to specific assumptions---just @{text name} or even +often need to refer to specific assumptions --- just @{text name} or even @{text name.prems} and @{text name.IH} can be too unspecific. This is where the indexing of fact lists comes in handy, e.g., @{text"name.IH(2)"} or @{text"name.prems(1-2)"}.

--- a/src/Doc/Prog_Prove/Types_and_funs.thy Mon Oct 06 19:19:16 2014 +0200 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy Mon Oct 06 19:40:22 2014 +0200 @@ -136,7 +136,7 @@ Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching 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 +total. This simplifies the logic --- terms are always defined --- but means that recursive functions must terminate. Otherwise one could define a function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by subtracting @{term"f n"} on both sides. @@ -435,7 +435,7 @@ responsibility not to include simplification rules that can lead to nontermination, either on their own or in combination with other simplification rules. The right-hand side of a simplification rule should -always be ``simpler'' than the left-hand side---in some sense. But since +always be ``simpler'' than the left-hand side --- in some sense. But since termination is undecidable, such a check cannot be automated completely and Isabelle makes little attempt to detect nontermination.