Replaced Raw Proof Blocks by Local Lemmas
authornipkow
Thu Nov 09 10:24:00 2017 +0100 (7 months ago)
changeset 67039690b4b334889
parent 67038 db3e2240f830
child 67040 c1b87d15774a
Replaced Raw Proof Blocks by Local Lemmas
src/Doc/Prog_Prove/Isar.thy
     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}