1.1 --- a/doc-src/IsarOverview/Isar/Logic.thy Sun Jun 11 00:42:22 2006 +0200
1.2 +++ b/doc-src/IsarOverview/Isar/Logic.thy Sun Jun 11 19:36:10 2006 +0200
1.3 @@ -247,6 +247,7 @@
1.4 \end{center}
1.5 *}
1.6
1.7 +
1.8 subsection{*Avoiding duplication*}
1.9
1.10 text{* So far our examples have been a bit unnatural: normally we want to
1.11 @@ -346,6 +347,24 @@
1.12 qed
1.13 qed
1.14
1.15 +text{* Too many names can easily clutter a proof. We already learned
1.16 +about @{text this} as a means of avoiding explicit names. Another
1.17 +handy device is to refer to a fact not by name but by contents: for
1.18 +example, writing @{text "`A \<or> B`"} (enclosing the formula in back quotes)
1.19 +refers to the fact @{text"A \<or> B"}
1.20 +without the need to name it. Here is a simple example, a revised version
1.21 +of the previous proof *}
1.22 +
1.23 +lemma assumes "A \<or> B" shows "B \<or> A"
1.24 +proof -
1.25 + from `A \<or> B` show ?thesis
1.26 +(*<*)oops(*>*)
1.27 +text{*\noindent which continues as before.
1.28 +
1.29 +Clearly, this device of quoting facts by contents is only advisable
1.30 +for small formulae. In such cases it is superior to naming because the
1.31 +reader immediately sees what the fact is without needing to search for
1.32 +it in the preceding proof text. *}
1.33
1.34 subsection{*Predicate calculus*}
1.35
1.36 @@ -415,14 +434,14 @@
1.37 show "?S \<notin> range f"
1.38 proof
1.39 assume "?S \<in> range f"
1.40 - then obtain y where fy: "?S = f y" ..
1.41 + then obtain y where "?S = f y" ..
1.42 show False
1.43 proof cases
1.44 assume "y \<in> ?S"
1.45 - with fy show False by blast
1.46 + with `?S = f y` show False by blast
1.47 next
1.48 assume "y \<notin> ?S"
1.49 - with fy show False by blast
1.50 + with `?S = f y` show False by blast
1.51 qed
1.52 qed
1.53 qed
1.54 @@ -450,17 +469,17 @@
1.55 show "?S \<notin> range f"
1.56 proof
1.57 assume "?S \<in> range f"
1.58 - then obtain y where fy: "?S = f y" ..
1.59 + then obtain y where "?S = f y" ..
1.60 show False
1.61 proof cases
1.62 assume "y \<in> ?S"
1.63 hence "y \<notin> f y" by simp
1.64 - hence "y \<notin> ?S" by(simp add:fy)
1.65 + hence "y \<notin> ?S" by(simp add: `?S = f y`)
1.66 thus False by contradiction
1.67 next
1.68 assume "y \<notin> ?S"
1.69 hence "y \<in> f y" by simp
1.70 - hence "y \<in> ?S" by(simp add:fy)
1.71 + hence "y \<in> ?S" by(simp add: `?S = f y`)
1.72 thus False by contradiction
1.73 qed
1.74 qed
2.1 --- a/doc-src/IsarOverview/Isar/document/Logic.tex Sun Jun 11 00:42:22 2006 +0200
2.2 +++ b/doc-src/IsarOverview/Isar/document/Logic.tex Sun Jun 11 19:36:10 2006 +0200
2.3 @@ -794,6 +794,46 @@
2.4 %
2.5 \endisadelimproof
2.6 %
2.7 +\begin{isamarkuptext}%
2.8 +Too many names can easily clutter a proof. We already learned
2.9 +about \isa{this} as a means of avoiding explicit names. Another
2.10 +handy device is to refer to a fact not by name but by contents: for
2.11 +example, writing \isa{{\isacharbackquote}A\ {\isasymor}\ B{\isacharbackquote}} (enclosing the formula in back quotes)
2.12 +refers to the fact \isa{A\ {\isasymor}\ B}
2.13 +without the need to name it. Here is a simple example, a revised version
2.14 +of the previous proof%
2.15 +\end{isamarkuptext}%
2.16 +\isamarkuptrue%
2.17 +\isacommand{lemma}\isamarkupfalse%
2.18 +\ \isakeyword{assumes}\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{shows}\ {\isachardoublequoteopen}B\ {\isasymor}\ A{\isachardoublequoteclose}\isanewline
2.19 +%
2.20 +\isadelimproof
2.21 +%
2.22 +\endisadelimproof
2.23 +%
2.24 +\isatagproof
2.25 +\isacommand{proof}\isamarkupfalse%
2.26 +\ {\isacharminus}\isanewline
2.27 +\ \ \isacommand{from}\isamarkupfalse%
2.28 +\ {\isacharbackquoteopen}A\ {\isasymor}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
2.29 +\ {\isacharquery}thesis%
2.30 +\endisatagproof
2.31 +{\isafoldproof}%
2.32 +%
2.33 +\isadelimproof
2.34 +%
2.35 +\endisadelimproof
2.36 +%
2.37 +\begin{isamarkuptext}%
2.38 +\noindent which continues as before.
2.39 +
2.40 +Clearly, this device of quoting facts by contents is only advisable
2.41 +for small formulae. In such cases it is superior to naming because the
2.42 +reader immediately sees what the fact is without needing to search for
2.43 +it in the preceding proof text.%
2.44 +\end{isamarkuptext}%
2.45 +\isamarkuptrue%
2.46 +%
2.47 \isamarkupsubsection{Predicate calculus%
2.48 }
2.49 \isamarkuptrue%
2.50 @@ -991,7 +1031,7 @@
2.51 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline
2.52 \ \ \ \ \isacommand{then}\isamarkupfalse%
2.53 \ \isacommand{obtain}\isamarkupfalse%
2.54 -\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.55 +\ y\ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.56 \isanewline
2.57 \ \ \ \ \isacommand{show}\isamarkupfalse%
2.58 \ False\isanewline
2.59 @@ -1000,7 +1040,7 @@
2.60 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
2.61 \ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
2.62 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
2.63 -\ fy\ \isacommand{show}\isamarkupfalse%
2.64 +\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
2.65 \ False\ \isacommand{by}\isamarkupfalse%
2.66 \ blast\isanewline
2.67 \ \ \ \ \isacommand{next}\isamarkupfalse%
2.68 @@ -1008,7 +1048,7 @@
2.69 \ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
2.70 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\isanewline
2.71 \ \ \ \ \ \ \isacommand{with}\isamarkupfalse%
2.72 -\ fy\ \isacommand{show}\isamarkupfalse%
2.73 +\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
2.74 \ False\ \isacommand{by}\isamarkupfalse%
2.75 \ blast\isanewline
2.76 \ \ \ \ \isacommand{qed}\isamarkupfalse%
2.77 @@ -1064,7 +1104,7 @@
2.78 \ {\isachardoublequoteopen}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequoteclose}\isanewline
2.79 \ \ \ \ \isacommand{then}\isamarkupfalse%
2.80 \ \isacommand{obtain}\isamarkupfalse%
2.81 -\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.82 +\ y\ \isakeyword{where}\ {\isachardoublequoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
2.83 \isanewline
2.84 \ \ \ \ \isacommand{show}\isamarkupfalse%
2.85 \ False\isanewline
2.86 @@ -1077,7 +1117,7 @@
2.87 \ simp\isanewline
2.88 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
2.89 \ {\isachardoublequoteopen}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse%
2.90 -{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
2.91 +{\isacharparenleft}simp\ add{\isacharcolon}\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}{\isacharparenright}\isanewline
2.92 \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
2.93 \ False\ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
2.94 \ contradiction\isanewline
2.95 @@ -1090,7 +1130,7 @@
2.96 \ simp\isanewline
2.97 \ \ \ \ \ \ \isacommand{hence}\isamarkupfalse%
2.98 \ {\isachardoublequoteopen}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequoteclose}\ \ \ \ \isacommand{by}\isamarkupfalse%
2.99 -{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
2.100 +{\isacharparenleft}simp\ add{\isacharcolon}\ {\isacharbackquoteopen}{\isacharquery}S\ {\isacharequal}\ f\ y{\isacharbackquoteclose}{\isacharparenright}\isanewline
2.101 \ \ \ \ \ \ \isacommand{thus}\isamarkupfalse%
2.102 \ False\ \ \ \ \ \ \ \ \ \isacommand{by}\isamarkupfalse%
2.103 \ contradiction\isanewline