author nipkow Thu Nov 09 10:24:00 2017 +0100 (16 months ago) changeset 67039 690b4b334889 parent 67038 db3e2240f830 child 67040 c1b87d15774a
Replaced Raw Proof Blocks by Local Lemmas
     1.1 --- a/src/Doc/Prog_Prove/Isar.thy	Thu Nov 09 09:08:14 2017 +0100
1.2 +++ b/src/Doc/Prog_Prove/Isar.thy	Thu Nov 09 10:24:00 2017 +0100
1.3 @@ -625,26 +625,21 @@
1.4  The \isacom{moreover} version is no shorter but expresses the structure
1.5  a bit more clearly and avoids new names.
1.6
1.7 -\subsection{Raw Proof Blocks}
1.8 +\subsection{Local Lemmas}
1.9
1.10  Sometimes one would like to prove some lemma locally within a proof,
1.11  a lemma that shares the current context of assumptions but that
1.12  has its own assumptions and is generalized over its locally fixed
1.13 -variables at the end. This is what a \concept{raw proof block} does:
1.14 -\begin{quote}\index{$IMP053@@{text"{ ... }"} (proof block)} 1.15 -@{text"{"} \isacom{fix} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\ 1.16 -\mbox{}\ \ \isacom{assume} @{text"A\<^sub>1 \<dots> A\<^sub>m"}\\ 1.17 -\mbox{}\ \$\vdots\$\\
1.18 -\mbox{}\ \ \isacom{have} @{text"B"}\ \isasymproof\\
1.19 -@{text"}"}
1.20 +variables at the end. This is simply an extension of the basic
1.21 +\indexed{\isacom{have}}{have} construct:
1.22 +\begin{quote}
1.23 +\indexed{\isacom{have}}{have} @{text"B"}\
1.24 + \indexed{\isacom{if}}{if} \<open>name:\<close> @{text"A\<^sub>1 \<dots> A\<^sub>m"}\
1.25 + \indexed{\isacom{for}}{for} @{text"x\<^sub>1 \<dots> x\<^sub>n"}\\
1.26 +\isasymproof
1.27  \end{quote}
1.28  proves @{text"\<lbrakk> A\<^sub>1; \<dots> ; A\<^sub>m \<rbrakk> \<Longrightarrow> B"}
1.29  where all @{text"x\<^sub>i"} have been replaced by unknowns @{text"?x\<^sub>i"}.
1.30 -\begin{warn}
1.31 -The conclusion of a raw proof block is \emph{not} indicated by \isacom{show}
1.32 -but is simply the final \isacom{have}.
1.33 -\end{warn}
1.34 -
1.35  As an example we prove a simple fact about divisibility on integers.
1.36  The definition of @{text "dvd"} is @{thm dvd_def}.
1.37  \end{isamarkuptext}%
1.38 @@ -652,24 +647,14 @@
1.39
1.40  lemma fixes a b :: int assumes "b dvd (a+b)" shows "b dvd a"
1.41  proof -
1.42 -  { fix k assume k: "a+b = b*k"
1.43 -    have "\<exists>k'. a = b*k'"
1.44 -    proof
1.45 -      show "a = b*(k - 1)" using k by(simp add: algebra_simps)
1.46 -    qed }
1.47 +  have "\<exists>k'. a = b*k'" if asm: "a+b = b*k" for k
1.48 +  proof
1.49 +    show "a = b*(k - 1)" using asm by(simp add: algebra_simps)
1.50 +  qed
1.51    then show ?thesis using assms by(auto simp add: dvd_def)
1.52  qed
1.53
1.54 -text{* Note that the result of a raw proof block has no name. In this example
1.55 -it was directly piped (via \isacom{then}) into the final proof, but it can
1.56 -also be named for later reference: you simply follow the block directly by a
1.57 -\isacom{note} command:
1.58 -\begin{quote}
1.59 -\indexed{\isacom{note}}{note} \ @{text"name = this"}
1.60 -\end{quote}
1.61 -This introduces a new name @{text name} that refers to @{text this},
1.62 -the fact just proved, in this case the preceding block. In general,
1.63 -\isacom{note} introduces a new name for one or more facts.
1.64 +text{*
1.65
1.66  \subsection*{Exercises}
1.67
1.68 @@ -687,8 +672,8 @@
1.69  \exercise
1.70  Give a readable, structured proof of the following lemma:
1.71  *}
1.72 -lemma "(\<exists>ys zs. xs = ys @ zs \<and> length ys = length zs)
1.73 -      \<or> (\<exists>ys zs. xs = ys @ zs \<and> length ys = length zs + 1)"
1.74 +lemma "\<exists>ys zs. xs = ys @ zs \<and>
1.75 +            (length ys = length zs \<or> length ys = length zs + 1)"
1.76  (*<*)oops(*>*)
1.77  text{*
1.78  Hint: There are predefined functions @{const_typ take} and @{const_typ drop}