114 not necessary. Both \isacom{have} steps are obvious. The second one introduces |
114 not necessary. Both \isacom{have} steps are obvious. The second one introduces |
115 the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof. |
115 the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof. |
116 If you wonder why @{text 2} directly implies @{text False}: from @{text 2} |
116 If you wonder why @{text 2} directly implies @{text False}: from @{text 2} |
117 it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}. |
117 it follows that @{prop"a \<notin> f a \<longleftrightarrow> a \<in> f a"}. |
118 |
118 |
119 \subsection{@{text this}, @{text then}, @{text hence} and @{text thus}} |
119 \subsection{@{text this}, \isacom{then}, \isacom{hence} and \isacom{thus}} |
120 |
120 |
121 Labels should be avoided. They interrupt the flow of the reader who has to |
121 Labels should be avoided. They interrupt the flow of the reader who has to |
122 scan the context for the point where the label was introduced. Ideally, the |
122 scan the context for the point where the label was introduced. Ideally, the |
123 proof is a linear flow, where the output of one step becomes the input of the |
123 proof is a linear flow, where the output of one step becomes the input of the |
124 next step, piping the previously proved fact into the next proof, just like |
124 next step, piping the previously proved fact into the next proof, just like |
139 steps into one. |
139 steps into one. |
140 |
140 |
141 To compact the text further, Isar has a few convenient abbreviations: |
141 To compact the text further, Isar has a few convenient abbreviations: |
142 \medskip |
142 \medskip |
143 |
143 |
144 \begin{tabular}{rcl} |
144 \begin{tabular}{r@ {\quad=\quad}l} |
145 \isacom{then} &=& \isacom{from} @{text this}\\ |
145 \isacom{then} & \isacom{from} @{text this}\\ |
146 \isacom{thus} &=& \isacom{then} \isacom{show}\\ |
146 \isacom{thus} & \isacom{then} \isacom{show}\\ |
147 \isacom{hence} &=& \isacom{then} \isacom{have} |
147 \isacom{hence} & \isacom{then} \isacom{have} |
148 \end{tabular} |
148 \end{tabular} |
149 \medskip |
149 \medskip |
150 |
150 |
151 \noindent |
151 \noindent |
152 With the help of these abbreviations the proof becomes |
152 With the help of these abbreviations the proof becomes |
162 text{* |
162 text{* |
163 |
163 |
164 There are two further linguistic variations: |
164 There are two further linguistic variations: |
165 \medskip |
165 \medskip |
166 |
166 |
167 \begin{tabular}{rcl} |
167 \begin{tabular}{r@ {\quad=\quad}l} |
168 (\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts} |
168 (\isacom{have}$\mid$\isacom{show}) \ \textit{prop} \ \isacom{using} \ \textit{facts} |
169 &=& |
169 & |
170 \isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\ |
170 \isacom{from} \ \textit{facts} \ (\isacom{have}$\mid$\isacom{show}) \ \textit{prop}\\ |
171 \isacom{with} \ \textit{facts} &=& \isacom{from} \ \textit{facts} \isa{this} |
171 \isacom{with} \ \textit{facts} & \isacom{from} \ \textit{facts} \isa{this} |
172 \end{tabular} |
172 \end{tabular} |
173 \medskip |
173 \medskip |
174 |
174 |
175 \noindent The \isacom{using} idiom de-emphasizes the used facts by moving them |
175 \noindent The \isacom{using} idiom de-emphasizes the used facts by moving them |
176 behind the proposition. |
176 behind the proposition. |