doc-src/IsarOverview/Isar/document/Logic.tex
changeset 16459 7efee005e568
parent 15909 5f0c8a3f0226
child 17125 e6a82d1a1829
     1.1 --- a/doc-src/IsarOverview/Isar/document/Logic.tex	Fri Jun 17 18:35:27 2005 +0200
     1.2 +++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Fri Jun 17 18:36:25 2005 +0200
     1.3 @@ -22,11 +22,14 @@
     1.4  \isamarkuptrue%
     1.5  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
     1.6  \isamarkupfalse%
     1.7 -\isamarkupfalse%
     1.8 -\isamarkupfalse%
     1.9 +\isacommand{proof}\ {\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
    1.10 +\ \ \isamarkupfalse%
    1.11 +\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    1.12 +\ \ \isamarkupfalse%
    1.13 +\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
    1.14 +\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
    1.15  \isamarkupfalse%
    1.16 -\isamarkupfalse%
    1.17 -\isamarkupfalse%
    1.18 +\isacommand{qed}\isamarkupfalse%
    1.19  %
    1.20  \begin{isamarkuptext}%
    1.21  \noindent
    1.22 @@ -42,11 +45,14 @@
    1.23  \isamarkuptrue%
    1.24  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
    1.25  \isamarkupfalse%
    1.26 -\isamarkupfalse%
    1.27 -\isamarkupfalse%
    1.28 +\isacommand{proof}\isanewline
    1.29 +\ \ \isamarkupfalse%
    1.30 +\isacommand{assume}\ a{\isacharcolon}\ A\isanewline
    1.31 +\ \ \isamarkupfalse%
    1.32 +\isacommand{show}\ A\ \isamarkupfalse%
    1.33 +\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
    1.34  \isamarkupfalse%
    1.35 -\isamarkupfalse%
    1.36 -\isamarkupfalse%
    1.37 +\isacommand{qed}\isamarkupfalse%
    1.38  %
    1.39  \begin{isamarkuptext}%
    1.40  \noindent Single-identifier formulae such as \isa{A} need not
    1.41 @@ -60,11 +66,14 @@
    1.42  \isamarkuptrue%
    1.43  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
    1.44  \isamarkupfalse%
    1.45 -\isamarkupfalse%
    1.46 -\isamarkupfalse%
    1.47 +\isacommand{proof}\isanewline
    1.48 +\ \ \isamarkupfalse%
    1.49 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    1.50 +\ \ \isamarkupfalse%
    1.51 +\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
    1.52 +\isacommand{{\isachardot}}\isanewline
    1.53  \isamarkupfalse%
    1.54 -\isamarkupfalse%
    1.55 -\isamarkupfalse%
    1.56 +\isacommand{qed}\isamarkupfalse%
    1.57  %
    1.58  \begin{isamarkuptext}%
    1.59  To hide proofs by assumption further, \isakeyword{by}\isa{{\isacharparenleft}method{\isacharparenright}}
    1.60 @@ -74,11 +83,14 @@
    1.61  \isamarkuptrue%
    1.62  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
    1.63  \isamarkupfalse%
    1.64 -\isamarkupfalse%
    1.65 -\isamarkupfalse%
    1.66 +\isacommand{proof}\isanewline
    1.67 +\ \ \isamarkupfalse%
    1.68 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    1.69 +\ \ \isamarkupfalse%
    1.70 +\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
    1.71 +\isacommand{by}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
    1.72  \isamarkupfalse%
    1.73 -\isamarkupfalse%
    1.74 -\isamarkupfalse%
    1.75 +\isacommand{qed}\isamarkupfalse%
    1.76  %
    1.77  \begin{isamarkuptext}%
    1.78  \noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}.
    1.79 @@ -92,11 +104,14 @@
    1.80  \isamarkuptrue%
    1.81  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
    1.82  \isamarkupfalse%
    1.83 -\isamarkupfalse%
    1.84 -\isamarkupfalse%
    1.85 +\isacommand{proof}\isanewline
    1.86 +\ \ \isamarkupfalse%
    1.87 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    1.88 +\ \ \isamarkupfalse%
    1.89 +\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
    1.90 +\isacommand{{\isachardot}{\isachardot}}\isanewline
    1.91  \isamarkupfalse%
    1.92 -\isamarkupfalse%
    1.93 -\isamarkupfalse%
    1.94 +\isacommand{qed}\isamarkupfalse%
    1.95  %
    1.96  \begin{isamarkuptext}%
    1.97  \noindent
    1.98 @@ -121,15 +136,25 @@
    1.99  \isamarkuptrue%
   1.100  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.101  \isamarkupfalse%
   1.102 -\isamarkupfalse%
   1.103 -\isamarkupfalse%
   1.104 -\isamarkupfalse%
   1.105 -\isamarkupfalse%
   1.106 +\isacommand{proof}\isanewline
   1.107 +\ \ \isamarkupfalse%
   1.108 +\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.109 +\ \ \isamarkupfalse%
   1.110 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.111 +\ \ \isamarkupfalse%
   1.112 +\isacommand{proof}\ {\isacharparenleft}rule\ conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}{\isacharparenright}\ \ %
   1.113 +\isamarkupcmt{\isa{conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}}: \isa{{\isacharparenleft}{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
   1.114 +}
   1.115 +\isanewline
   1.116 +\ \ \ \ \isamarkupfalse%
   1.117 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   1.118 +\ \ \ \ \isamarkupfalse%
   1.119 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.120 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.121 +\ \ \isamarkupfalse%
   1.122 +\isacommand{qed}\isanewline
   1.123  \isamarkupfalse%
   1.124 -\isamarkupfalse%
   1.125 -\isamarkupfalse%
   1.126 -\isamarkupfalse%
   1.127 -\isamarkupfalse%
   1.128 +\isacommand{qed}\isamarkupfalse%
   1.129  %
   1.130  \begin{isamarkuptext}%
   1.131  \noindent Note that the term \isa{{\isacharquery}thesis} always stands for the
   1.132 @@ -155,16 +180,23 @@
   1.133  \isamarkuptrue%
   1.134  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.135  \isamarkupfalse%
   1.136 -\isamarkupfalse%
   1.137 -\isamarkupfalse%
   1.138 -\isamarkupfalse%
   1.139 -\isamarkupfalse%
   1.140 +\isacommand{proof}\isanewline
   1.141 +\ \ \isamarkupfalse%
   1.142 +\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.143 +\ \ \isamarkupfalse%
   1.144 +\isacommand{from}\ AB\ \isamarkupfalse%
   1.145 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.146 +\ \ \isamarkupfalse%
   1.147 +\isacommand{proof}\isanewline
   1.148 +\ \ \ \ \isamarkupfalse%
   1.149 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   1.150 +\ \ \ \ \isamarkupfalse%
   1.151 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.152 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.153 +\ \ \isamarkupfalse%
   1.154 +\isacommand{qed}\isanewline
   1.155  \isamarkupfalse%
   1.156 -\isamarkupfalse%
   1.157 -\isamarkupfalse%
   1.158 -\isamarkupfalse%
   1.159 -\isamarkupfalse%
   1.160 -\isamarkupfalse%
   1.161 +\isacommand{qed}\isamarkupfalse%
   1.162  %
   1.163  \begin{isamarkuptext}%
   1.164  Now we come to a second important principle:
   1.165 @@ -178,16 +210,23 @@
   1.166  \isamarkuptrue%
   1.167  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.168  \isamarkupfalse%
   1.169 -\isamarkupfalse%
   1.170 -\isamarkupfalse%
   1.171 -\isamarkupfalse%
   1.172 -\isamarkupfalse%
   1.173 +\isacommand{proof}\isanewline
   1.174 +\ \ \isamarkupfalse%
   1.175 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.176 +\ \ \isamarkupfalse%
   1.177 +\isacommand{from}\ this\ \isamarkupfalse%
   1.178 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.179 +\ \ \isamarkupfalse%
   1.180 +\isacommand{proof}\isanewline
   1.181 +\ \ \ \ \isamarkupfalse%
   1.182 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   1.183 +\ \ \ \ \isamarkupfalse%
   1.184 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.185 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.186 +\ \ \isamarkupfalse%
   1.187 +\isacommand{qed}\isanewline
   1.188  \isamarkupfalse%
   1.189 -\isamarkupfalse%
   1.190 -\isamarkupfalse%
   1.191 -\isamarkupfalse%
   1.192 -\isamarkupfalse%
   1.193 -\isamarkupfalse%
   1.194 +\isacommand{qed}\isamarkupfalse%
   1.195  %
   1.196  \begin{isamarkuptext}%
   1.197  \noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations:
   1.198 @@ -203,18 +242,23 @@
   1.199  \isamarkuptrue%
   1.200  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.201  \isamarkupfalse%
   1.202 -\isamarkupfalse%
   1.203 -\isamarkupfalse%
   1.204 -\isamarkupfalse%
   1.205 -\isamarkupfalse%
   1.206 -\isamarkupfalse%
   1.207 +\isacommand{proof}\isanewline
   1.208 +\ \ \isamarkupfalse%
   1.209 +\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.210 +\ \ \isamarkupfalse%
   1.211 +\isacommand{from}\ ab\ \isamarkupfalse%
   1.212 +\isacommand{have}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   1.213 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.214 +\ \ \isamarkupfalse%
   1.215 +\isacommand{from}\ ab\ \isamarkupfalse%
   1.216 +\isacommand{have}\ b{\isacharcolon}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   1.217 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.218 +\ \ \isamarkupfalse%
   1.219 +\isacommand{from}\ b\ a\ \isamarkupfalse%
   1.220 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
   1.221 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.222  \isamarkupfalse%
   1.223 -\isamarkupfalse%
   1.224 -\isamarkupfalse%
   1.225 -\isamarkupfalse%
   1.226 -\isamarkupfalse%
   1.227 -\isamarkupfalse%
   1.228 -\isamarkupfalse%
   1.229 +\isacommand{qed}\isamarkupfalse%
   1.230  %
   1.231  \begin{isamarkuptext}%
   1.232  \noindent It is worth examining this text in detail because it
   1.233 @@ -265,19 +309,25 @@
   1.234  \isamarkuptrue%
   1.235  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.236  \isamarkupfalse%
   1.237 -\isamarkupfalse%
   1.238 -\isamarkupfalse%
   1.239 -\isamarkupfalse%
   1.240 -\isamarkupfalse%
   1.241 -\isamarkupfalse%
   1.242 -\isamarkupfalse%
   1.243 +\isacommand{proof}\isanewline
   1.244 +\ \ \isamarkupfalse%
   1.245 +\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   1.246 +\ \ \isamarkupfalse%
   1.247 +\isacommand{from}\ ab\ \isamarkupfalse%
   1.248 +\isacommand{have}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   1.249 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.250 +\ \ \isamarkupfalse%
   1.251 +\isacommand{moreover}\isanewline
   1.252 +\ \ \isamarkupfalse%
   1.253 +\isacommand{from}\ ab\ \isamarkupfalse%
   1.254 +\isacommand{have}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   1.255 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.256 +\ \ \isamarkupfalse%
   1.257 +\isacommand{ultimately}\ \isamarkupfalse%
   1.258 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
   1.259 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.260  \isamarkupfalse%
   1.261 -\isamarkupfalse%
   1.262 -\isamarkupfalse%
   1.263 -\isamarkupfalse%
   1.264 -\isamarkupfalse%
   1.265 -\isamarkupfalse%
   1.266 -\isamarkupfalse%
   1.267 +\isacommand{qed}\isamarkupfalse%
   1.268  %
   1.269  \begin{isamarkuptext}%
   1.270  \noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with
   1.271 @@ -296,36 +346,56 @@
   1.272  \isamarkuptrue%
   1.273  \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
   1.274  \isamarkupfalse%
   1.275 -\isamarkupfalse%
   1.276 -\isamarkupfalse%
   1.277 -\isamarkupfalse%
   1.278 -\isamarkupfalse%
   1.279 -\isamarkupfalse%
   1.280 -\isamarkupfalse%
   1.281 -\isamarkupfalse%
   1.282 -\isamarkupfalse%
   1.283 -\isamarkupfalse%
   1.284 -\isamarkupfalse%
   1.285 -\isamarkupfalse%
   1.286 -\isamarkupfalse%
   1.287 -\isamarkupfalse%
   1.288 -\isamarkupfalse%
   1.289 +\isacommand{proof}\isanewline
   1.290 +\ \ \isamarkupfalse%
   1.291 +\isacommand{assume}\ n{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   1.292 +\ \ \isamarkupfalse%
   1.293 +\isacommand{show}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
   1.294 +\ \ \isamarkupfalse%
   1.295 +\isacommand{proof}\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
   1.296 +\ \ \ \ \isamarkupfalse%
   1.297 +\isacommand{assume}\ nn{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   1.298 +\ \ \ \ \isamarkupfalse%
   1.299 +\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline
   1.300 +\ \ \ \ \isamarkupfalse%
   1.301 +\isacommand{proof}\isanewline
   1.302 +\ \ \ \ \ \ \isamarkupfalse%
   1.303 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
   1.304 +\ \ \ \ \ \ \isamarkupfalse%
   1.305 +\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ B{\isachardoublequote}\isanewline
   1.306 +\ \ \ \ \ \ \isamarkupfalse%
   1.307 +\isacommand{proof}\isanewline
   1.308 +\ \ \ \ \ \ \ \ \isamarkupfalse%
   1.309 +\isacommand{assume}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   1.310 +\ \ \ \ \ \ \ \ \isamarkupfalse%
   1.311 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.312 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.313 +\ \ \ \ \ \ \ \ \isamarkupfalse%
   1.314 +\isacommand{with}\ n\ \isamarkupfalse%
   1.315 +\isacommand{show}\ False\ \isamarkupfalse%
   1.316 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.317 +\ \ \ \ \ \ \isamarkupfalse%
   1.318 +\isacommand{qed}\isanewline
   1.319 +\ \ \ \ \ \ \isamarkupfalse%
   1.320 +\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.321 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.322 +\ \ \ \ \ \ \isamarkupfalse%
   1.323 +\isacommand{with}\ nn\ \isamarkupfalse%
   1.324 +\isacommand{show}\ False\ \isamarkupfalse%
   1.325 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.326 +\ \ \ \ \isamarkupfalse%
   1.327 +\isacommand{qed}\isanewline
   1.328 +\ \ \ \ \isamarkupfalse%
   1.329 +\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.330 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.331 +\ \ \ \ \isamarkupfalse%
   1.332 +\isacommand{with}\ nn\ \isamarkupfalse%
   1.333 +\isacommand{show}\ False\ \isamarkupfalse%
   1.334 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.335 +\ \ \isamarkupfalse%
   1.336 +\isacommand{qed}\isanewline
   1.337  \isamarkupfalse%
   1.338 -\isamarkupfalse%
   1.339 -\isamarkupfalse%
   1.340 -\isamarkupfalse%
   1.341 -\isamarkupfalse%
   1.342 -\isamarkupfalse%
   1.343 -\isamarkupfalse%
   1.344 -\isamarkupfalse%
   1.345 -\isamarkupfalse%
   1.346 -\isamarkupfalse%
   1.347 -\isamarkupfalse%
   1.348 -\isamarkupfalse%
   1.349 -\isamarkupfalse%
   1.350 -\isamarkupfalse%
   1.351 -\isamarkupfalse%
   1.352 -\isamarkupfalse%
   1.353 +\isacommand{qed}\isamarkupfalse%
   1.354  %
   1.355  \begin{isamarkuptext}%
   1.356  \noindent
   1.357 @@ -355,15 +425,19 @@
   1.358  \isamarkuptrue%
   1.359  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   1.360  \isamarkupfalse%
   1.361 -\isamarkupfalse%
   1.362 -\isamarkupfalse%
   1.363 -\isamarkupfalse%
   1.364 -\isamarkupfalse%
   1.365 +\isacommand{proof}\isanewline
   1.366 +\ \ \isamarkupfalse%
   1.367 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.368 +\isacommand{thus}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   1.369 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.370  \isamarkupfalse%
   1.371 -\isamarkupfalse%
   1.372 +\isacommand{next}\isanewline
   1.373 +\ \ \isamarkupfalse%
   1.374 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   1.375 +\isacommand{thus}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   1.376 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.377  \isamarkupfalse%
   1.378 -\isamarkupfalse%
   1.379 -\isamarkupfalse%
   1.380 +\isacommand{qed}\isamarkupfalse%
   1.381  %
   1.382  \begin{isamarkuptext}%
   1.383  \noindent The \isakeyword{proof} always works on the conclusion,
   1.384 @@ -394,15 +468,19 @@
   1.385  \isacommand{lemma}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\isanewline
   1.386  \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   1.387  \isamarkupfalse%
   1.388 -\isamarkupfalse%
   1.389 -\isamarkupfalse%
   1.390 -\isamarkupfalse%
   1.391 -\isamarkupfalse%
   1.392 +\isacommand{proof}\isanewline
   1.393 +\ \ \isamarkupfalse%
   1.394 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
   1.395 +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   1.396 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.397  \isamarkupfalse%
   1.398 -\isamarkupfalse%
   1.399 +\isacommand{next}\isanewline
   1.400 +\ \ \isamarkupfalse%
   1.401 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
   1.402 +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
   1.403 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.404  \isamarkupfalse%
   1.405 -\isamarkupfalse%
   1.406 -\isamarkupfalse%
   1.407 +\isacommand{qed}\isamarkupfalse%
   1.408  %
   1.409  \begin{isamarkuptext}%
   1.410  \noindent Any formula may be followed by
   1.411 @@ -419,15 +497,19 @@
   1.412  \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
   1.413  \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   1.414  \isamarkupfalse%
   1.415 -\isamarkupfalse%
   1.416 -\isamarkupfalse%
   1.417 -\isamarkupfalse%
   1.418 -\isamarkupfalse%
   1.419 +\isacommand{proof}\isanewline
   1.420 +\ \ \isamarkupfalse%
   1.421 +\isacommand{from}\ AB\ \isamarkupfalse%
   1.422 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   1.423 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.424  \isamarkupfalse%
   1.425 -\isamarkupfalse%
   1.426 +\isacommand{next}\isanewline
   1.427 +\ \ \isamarkupfalse%
   1.428 +\isacommand{from}\ AB\ \isamarkupfalse%
   1.429 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
   1.430 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.431  \isamarkupfalse%
   1.432 -\isamarkupfalse%
   1.433 -\isamarkupfalse%
   1.434 +\isacommand{qed}\isamarkupfalse%
   1.435  %
   1.436  \begin{isamarkuptext}%
   1.437  \noindent Note the difference between \isa{{\isacharquery}AB}, a term, and
   1.438 @@ -441,12 +523,15 @@
   1.439  \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
   1.440  \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   1.441  \isamarkupfalse%
   1.442 -\isamarkupfalse%
   1.443 -\isamarkupfalse%
   1.444 +\isacommand{using}\ AB\isanewline
   1.445  \isamarkupfalse%
   1.446 -\isamarkupfalse%
   1.447 +\isacommand{proof}\isanewline
   1.448 +\ \ \isamarkupfalse%
   1.449 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   1.450 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.451 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.452  \isamarkupfalse%
   1.453 -\isamarkupfalse%
   1.454 +\isacommand{qed}\isamarkupfalse%
   1.455  %
   1.456  \begin{isamarkuptext}%
   1.457  \noindent Command \isakeyword{using} can appear before a proof
   1.458 @@ -468,19 +553,26 @@
   1.459  \isamarkuptrue%
   1.460  \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}B\ {\isasymor}\ A{\isachardoublequote}\isanewline
   1.461  \isamarkupfalse%
   1.462 -\isamarkupfalse%
   1.463 -\isamarkupfalse%
   1.464 -\isamarkupfalse%
   1.465 -\isamarkupfalse%
   1.466 -\isamarkupfalse%
   1.467 -\isamarkupfalse%
   1.468 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.469 +\ \ \isamarkupfalse%
   1.470 +\isacommand{from}\ AB\ \isamarkupfalse%
   1.471 +\isacommand{show}\ {\isacharquery}thesis\isanewline
   1.472 +\ \ \isamarkupfalse%
   1.473 +\isacommand{proof}\isanewline
   1.474 +\ \ \ \ \isamarkupfalse%
   1.475 +\isacommand{assume}\ A\ \isamarkupfalse%
   1.476 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.477 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.478 +\ \ \isamarkupfalse%
   1.479 +\isacommand{next}\isanewline
   1.480 +\ \ \ \ \isamarkupfalse%
   1.481 +\isacommand{assume}\ B\ \isamarkupfalse%
   1.482 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.483 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.484 +\ \ \isamarkupfalse%
   1.485 +\isacommand{qed}\isanewline
   1.486  \isamarkupfalse%
   1.487 -\isamarkupfalse%
   1.488 -\isamarkupfalse%
   1.489 -\isamarkupfalse%
   1.490 -\isamarkupfalse%
   1.491 -\isamarkupfalse%
   1.492 -\isamarkupfalse%
   1.493 +\isacommand{qed}\isamarkupfalse%
   1.494  %
   1.495  \isamarkupsubsection{Predicate calculus%
   1.496  }
   1.497 @@ -497,12 +589,21 @@
   1.498  \isamarkuptrue%
   1.499  \isacommand{lemma}\ \isakeyword{assumes}\ P{\isacharcolon}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline
   1.500  \isamarkupfalse%
   1.501 -\isamarkupfalse%
   1.502 -\isamarkupfalse%
   1.503 +\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
   1.504 +\isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}%
   1.505 +}
   1.506 +\isanewline
   1.507 +\ \ \isamarkupfalse%
   1.508 +\isacommand{fix}\ a\isanewline
   1.509 +\ \ \isamarkupfalse%
   1.510 +\isacommand{from}\ P\ \isamarkupfalse%
   1.511 +\isacommand{show}\ {\isachardoublequote}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   1.512 +\isacommand{{\isachardot}{\isachardot}}\ \ %
   1.513 +\isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
   1.514 +}
   1.515 +\isanewline
   1.516  \isamarkupfalse%
   1.517 -\isamarkupfalse%
   1.518 -\isamarkupfalse%
   1.519 -\isamarkupfalse%
   1.520 +\isacommand{qed}\isamarkupfalse%
   1.521  %
   1.522  \begin{isamarkuptext}%
   1.523  \noindent Note that in the proof we have chosen to call the bound
   1.524 @@ -514,16 +615,29 @@
   1.525  \isamarkuptrue%
   1.526  \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline
   1.527  \isamarkupfalse%
   1.528 -\isamarkupfalse%
   1.529 -\isamarkupfalse%
   1.530 -\isamarkupfalse%
   1.531 -\isamarkupfalse%
   1.532 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.533 +\ \ \isamarkupfalse%
   1.534 +\isacommand{from}\ Pf\ \isamarkupfalse%
   1.535 +\isacommand{show}\ {\isacharquery}thesis\isanewline
   1.536 +\ \ \isamarkupfalse%
   1.537 +\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ %
   1.538 +\isamarkupcmt{\isa{exE}: \isa{{\isasymlbrakk}{\isasymexists}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x\ {\isasymLongrightarrow}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}Q}%
   1.539 +}
   1.540 +\isanewline
   1.541 +\ \ \ \ \isamarkupfalse%
   1.542 +\isacommand{fix}\ x\isanewline
   1.543 +\ \ \ \ \isamarkupfalse%
   1.544 +\isacommand{assume}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline
   1.545 +\ \ \ \ \isamarkupfalse%
   1.546 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.547 +\isacommand{{\isachardot}{\isachardot}}\ \ %
   1.548 +\isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}%
   1.549 +}
   1.550 +\isanewline
   1.551 +\ \ \isamarkupfalse%
   1.552 +\isacommand{qed}\isanewline
   1.553  \isamarkupfalse%
   1.554 -\isamarkupfalse%
   1.555 -\isamarkupfalse%
   1.556 -\isamarkupfalse%
   1.557 -\isamarkupfalse%
   1.558 -\isamarkupfalse%
   1.559 +\isacommand{qed}\isamarkupfalse%
   1.560  %
   1.561  \begin{isamarkuptext}%
   1.562  \noindent Explicit $\exists$-elimination as seen above can become
   1.563 @@ -534,13 +648,16 @@
   1.564  \isamarkuptrue%
   1.565  \isacommand{lemma}\ \isakeyword{assumes}\ Pf{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\isanewline
   1.566  \isamarkupfalse%
   1.567 -\isamarkupfalse%
   1.568 -\isamarkupfalse%
   1.569 -\isamarkupfalse%
   1.570 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.571 +\ \ \isamarkupfalse%
   1.572 +\isacommand{from}\ Pf\ \isamarkupfalse%
   1.573 +\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   1.574 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.575 +\ \ \isamarkupfalse%
   1.576 +\isacommand{thus}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\ \isamarkupfalse%
   1.577 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.578  \isamarkupfalse%
   1.579 -\isamarkupfalse%
   1.580 -\isamarkupfalse%
   1.581 -\isamarkupfalse%
   1.582 +\isacommand{qed}\isamarkupfalse%
   1.583  %
   1.584  \begin{isamarkuptext}%
   1.585  \noindent Note how the proof text follows the usual mathematical style
   1.586 @@ -555,16 +672,21 @@
   1.587  \isamarkuptrue%
   1.588  \isacommand{lemma}\ \isakeyword{assumes}\ ex{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ {\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ {\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\isanewline
   1.589  \isamarkupfalse%
   1.590 -\isamarkupfalse%
   1.591 -\isamarkupfalse%
   1.592 -\isamarkupfalse%
   1.593 -\isamarkupfalse%
   1.594 +\isacommand{proof}\isanewline
   1.595 +\ \ \isamarkupfalse%
   1.596 +\isacommand{fix}\ y\isanewline
   1.597 +\ \ \isamarkupfalse%
   1.598 +\isacommand{from}\ ex\ \isamarkupfalse%
   1.599 +\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   1.600 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.601 +\ \ \isamarkupfalse%
   1.602 +\isacommand{hence}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   1.603 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.604 +\ \ \isamarkupfalse%
   1.605 +\isacommand{thus}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   1.606 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.607  \isamarkupfalse%
   1.608 -\isamarkupfalse%
   1.609 -\isamarkupfalse%
   1.610 -\isamarkupfalse%
   1.611 -\isamarkupfalse%
   1.612 -\isamarkupfalse%
   1.613 +\isacommand{qed}\isamarkupfalse%
   1.614  %
   1.615  \isamarkupsubsection{Making bigger steps%
   1.616  }
   1.617 @@ -579,28 +701,43 @@
   1.618  \isamarkuptrue%
   1.619  \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   1.620  \isamarkupfalse%
   1.621 -\isamarkupfalse%
   1.622 -\isamarkupfalse%
   1.623 -\isamarkupfalse%
   1.624 -\isamarkupfalse%
   1.625 -\isamarkupfalse%
   1.626 -\isamarkupfalse%
   1.627 -\isamarkupfalse%
   1.628 -\isamarkupfalse%
   1.629 -\isamarkupfalse%
   1.630 -\isamarkupfalse%
   1.631 +\isacommand{proof}\isanewline
   1.632 +\ \ \isamarkupfalse%
   1.633 +\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
   1.634 +\ \ \isamarkupfalse%
   1.635 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
   1.636 +\ \ \isamarkupfalse%
   1.637 +\isacommand{proof}\isanewline
   1.638 +\ \ \ \ \isamarkupfalse%
   1.639 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
   1.640 +\ \ \ \ \isamarkupfalse%
   1.641 +\isacommand{then}\ \isamarkupfalse%
   1.642 +\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
   1.643 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.644 +\ \ \ \ \isamarkupfalse%
   1.645 +\isacommand{show}\ False\isanewline
   1.646 +\ \ \ \ \isamarkupfalse%
   1.647 +\isacommand{proof}\ cases\isanewline
   1.648 +\ \ \ \ \ \ \isamarkupfalse%
   1.649 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   1.650 +\ \ \ \ \ \ \isamarkupfalse%
   1.651 +\isacommand{with}\ fy\ \isamarkupfalse%
   1.652 +\isacommand{show}\ False\ \isamarkupfalse%
   1.653 +\isacommand{by}\ blast\isanewline
   1.654 +\ \ \ \ \isamarkupfalse%
   1.655 +\isacommand{next}\isanewline
   1.656 +\ \ \ \ \ \ \isamarkupfalse%
   1.657 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   1.658 +\ \ \ \ \ \ \isamarkupfalse%
   1.659 +\isacommand{with}\ fy\ \isamarkupfalse%
   1.660 +\isacommand{show}\ False\ \isamarkupfalse%
   1.661 +\isacommand{by}\ blast\isanewline
   1.662 +\ \ \ \ \isamarkupfalse%
   1.663 +\isacommand{qed}\isanewline
   1.664 +\ \ \isamarkupfalse%
   1.665 +\isacommand{qed}\isanewline
   1.666  \isamarkupfalse%
   1.667 -\isamarkupfalse%
   1.668 -\isamarkupfalse%
   1.669 -\isamarkupfalse%
   1.670 -\isamarkupfalse%
   1.671 -\isamarkupfalse%
   1.672 -\isamarkupfalse%
   1.673 -\isamarkupfalse%
   1.674 -\isamarkupfalse%
   1.675 -\isamarkupfalse%
   1.676 -\isamarkupfalse%
   1.677 -\isamarkupfalse%
   1.678 +\isacommand{qed}\isamarkupfalse%
   1.679  %
   1.680  \begin{isamarkuptext}%
   1.681  \noindent
   1.682 @@ -624,34 +761,53 @@
   1.683  \isamarkuptrue%
   1.684  \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   1.685  \isamarkupfalse%
   1.686 -\isamarkupfalse%
   1.687 -\isamarkupfalse%
   1.688 -\isamarkupfalse%
   1.689 -\isamarkupfalse%
   1.690 -\isamarkupfalse%
   1.691 -\isamarkupfalse%
   1.692 -\isamarkupfalse%
   1.693 -\isamarkupfalse%
   1.694 -\isamarkupfalse%
   1.695 -\isamarkupfalse%
   1.696 -\isamarkupfalse%
   1.697 -\isamarkupfalse%
   1.698 -\isamarkupfalse%
   1.699 +\isacommand{proof}\isanewline
   1.700 +\ \ \isamarkupfalse%
   1.701 +\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
   1.702 +\ \ \isamarkupfalse%
   1.703 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
   1.704 +\ \ \isamarkupfalse%
   1.705 +\isacommand{proof}\isanewline
   1.706 +\ \ \ \ \isamarkupfalse%
   1.707 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
   1.708 +\ \ \ \ \isamarkupfalse%
   1.709 +\isacommand{then}\ \isamarkupfalse%
   1.710 +\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
   1.711 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   1.712 +\ \ \ \ \isamarkupfalse%
   1.713 +\isacommand{show}\ False\isanewline
   1.714 +\ \ \ \ \isamarkupfalse%
   1.715 +\isacommand{proof}\ cases\isanewline
   1.716 +\ \ \ \ \ \ \isamarkupfalse%
   1.717 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   1.718 +\ \ \ \ \ \ \isamarkupfalse%
   1.719 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
   1.720 +\isacommand{by}\ simp\isanewline
   1.721 +\ \ \ \ \ \ \isamarkupfalse%
   1.722 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
   1.723 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
   1.724 +\ \ \ \ \ \ \isamarkupfalse%
   1.725 +\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
   1.726 +\isacommand{by}\ contradiction\isanewline
   1.727 +\ \ \ \ \isamarkupfalse%
   1.728 +\isacommand{next}\isanewline
   1.729 +\ \ \ \ \ \ \isamarkupfalse%
   1.730 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   1.731 +\ \ \ \ \ \ \isamarkupfalse%
   1.732 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
   1.733 +\isacommand{by}\ simp\isanewline
   1.734 +\ \ \ \ \ \ \isamarkupfalse%
   1.735 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
   1.736 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
   1.737 +\ \ \ \ \ \ \isamarkupfalse%
   1.738 +\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
   1.739 +\isacommand{by}\ contradiction\isanewline
   1.740 +\ \ \ \ \isamarkupfalse%
   1.741 +\isacommand{qed}\isanewline
   1.742 +\ \ \isamarkupfalse%
   1.743 +\isacommand{qed}\isanewline
   1.744  \isamarkupfalse%
   1.745 -\isamarkupfalse%
   1.746 -\isamarkupfalse%
   1.747 -\isamarkupfalse%
   1.748 -\isamarkupfalse%
   1.749 -\isamarkupfalse%
   1.750 -\isamarkupfalse%
   1.751 -\isamarkupfalse%
   1.752 -\isamarkupfalse%
   1.753 -\isamarkupfalse%
   1.754 -\isamarkupfalse%
   1.755 -\isamarkupfalse%
   1.756 -\isamarkupfalse%
   1.757 -\isamarkupfalse%
   1.758 -\isamarkupfalse%
   1.759 +\isacommand{qed}\isamarkupfalse%
   1.760  %
   1.761  \begin{isamarkuptext}%
   1.762  \noindent Method \isa{contradiction} succeeds if both $P$ and
   1.763 @@ -664,7 +820,7 @@
   1.764  \isamarkuptrue%
   1.765  \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   1.766  \isamarkupfalse%
   1.767 -\isamarkupfalse%
   1.768 +\isacommand{by}\ best\isamarkupfalse%
   1.769  %
   1.770  \isamarkupsubsection{Raw proof blocks%
   1.771  }
   1.772 @@ -680,19 +836,28 @@
   1.773  \isamarkupfalse%
   1.774  \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   1.775  \isamarkupfalse%
   1.776 -\isamarkupfalse%
   1.777 -\isamarkupfalse%
   1.778 -\isamarkupfalse%
   1.779 -\isamarkupfalse%
   1.780 -\isamarkupfalse%
   1.781 -\isamarkupfalse%
   1.782 +\isacommand{proof}\isanewline
   1.783 +\ \ \isamarkupfalse%
   1.784 +\isacommand{fix}\ x\ \isamarkupfalse%
   1.785 +\isacommand{show}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   1.786 +\ \ \isamarkupfalse%
   1.787 +\isacommand{proof}\isanewline
   1.788 +\ \ \ \ \isamarkupfalse%
   1.789 +\isacommand{fix}\ y\ \isamarkupfalse%
   1.790 +\isacommand{show}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   1.791 +\ \ \ \ \isamarkupfalse%
   1.792 +\isacommand{proof}\isanewline
   1.793 +\ \ \ \ \ \ \isamarkupfalse%
   1.794 +\isacommand{assume}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequote}\isanewline
   1.795 +\ \ \ \ \ \ \isamarkupfalse%
   1.796 +\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   1.797 +\isacommand{sorry}\isanewline
   1.798 +\ \ \ \ \isamarkupfalse%
   1.799 +\isacommand{qed}\isanewline
   1.800 +\ \ \isamarkupfalse%
   1.801 +\isacommand{qed}\isanewline
   1.802  \isamarkupfalse%
   1.803 -\isamarkupfalse%
   1.804 -\isamarkupfalse%
   1.805 -\isamarkupfalse%
   1.806 -\isamarkupfalse%
   1.807 -\isamarkupfalse%
   1.808 -\isamarkupfalse%
   1.809 +\isacommand{qed}\isamarkupfalse%
   1.810  %
   1.811  \begin{isamarkuptext}%
   1.812  \noindent Since we are only interested in the decomposition and not the
   1.813 @@ -706,17 +871,24 @@
   1.814  \isamarkuptrue%
   1.815  \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   1.816  \isamarkupfalse%
   1.817 -\isamarkupfalse%
   1.818 -\isamarkupfalse%
   1.819 -\isamarkupfalse%
   1.820 -\isamarkupfalse%
   1.821 -\isamarkupfalse%
   1.822 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.823 +\ \ \isamarkupfalse%
   1.824 +\isacommand{have}\ {\isachardoublequote}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   1.825 +\ \ \isamarkupfalse%
   1.826 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.827 +\ \ \ \ \isamarkupfalse%
   1.828 +\isacommand{fix}\ x\ y\ \isamarkupfalse%
   1.829 +\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
   1.830 +\ \ \ \ \isamarkupfalse%
   1.831 +\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   1.832 +\isacommand{sorry}\isanewline
   1.833 +\ \ \isamarkupfalse%
   1.834 +\isacommand{qed}\isanewline
   1.835 +\ \ \isamarkupfalse%
   1.836 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.837 +\isacommand{by}\ blast\isanewline
   1.838  \isamarkupfalse%
   1.839 -\isamarkupfalse%
   1.840 -\isamarkupfalse%
   1.841 -\isamarkupfalse%
   1.842 -\isamarkupfalse%
   1.843 -\isamarkupfalse%
   1.844 +\isacommand{qed}\isamarkupfalse%
   1.845  %
   1.846  \begin{isamarkuptext}%
   1.847  \noindent
   1.848 @@ -726,16 +898,20 @@
   1.849  \isamarkuptrue%
   1.850  \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   1.851  \isamarkupfalse%
   1.852 -\isamarkupfalse%
   1.853 -\isamarkupfalse%
   1.854 -\isamarkupfalse%
   1.855 -\isamarkupfalse%
   1.856 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.857 +\ \ \isamarkupfalse%
   1.858 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.859 +\isacommand{fix}\ x\ y\ \isamarkupfalse%
   1.860 +\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
   1.861 +\ \ \ \ \isamarkupfalse%
   1.862 +\isacommand{have}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   1.863 +\isacommand{sorry}\ \isamarkupfalse%
   1.864 +\isacommand{{\isacharbraceright}}\isanewline
   1.865 +\ \ \isamarkupfalse%
   1.866 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.867 +\isacommand{by}\ blast\isanewline
   1.868  \isamarkupfalse%
   1.869 -\isamarkupfalse%
   1.870 -\isamarkupfalse%
   1.871 -\isamarkupfalse%
   1.872 -\isamarkupfalse%
   1.873 -\isamarkupfalse%
   1.874 +\isacommand{qed}\isamarkupfalse%
   1.875  %
   1.876  \begin{isamarkuptext}%
   1.877  \noindent The result of the raw proof block is the same theorem
   1.878 @@ -771,31 +947,67 @@
   1.879  %
   1.880  \renewcommand{\isamarkupcmt}[1]{#1}
   1.881  \isamarkupfalse%
   1.882 -\isamarkupfalse%
   1.883 -\isamarkupfalse%
   1.884 -\isamarkupfalse%
   1.885 -\isamarkupfalse%
   1.886 -\isamarkupfalse%
   1.887 -\isamarkupfalse%
   1.888 -\isamarkupfalse%
   1.889 -\isamarkupfalse%
   1.890 -\isamarkupfalse%
   1.891 -\isamarkupfalse%
   1.892 -\isamarkupfalse%
   1.893 -\isamarkupfalse%
   1.894 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.895 +\ \ \isamarkupfalse%
   1.896 +\isacommand{have}\ {\isachardoublequote}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
   1.897 +\ %
   1.898 +\isamarkupcmt{\dots%
   1.899 +}
   1.900 +\isanewline
   1.901 +\ \ \isamarkupfalse%
   1.902 +\isacommand{moreover}\isanewline
   1.903 +\ \ \isamarkupfalse%
   1.904 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.905 +\isacommand{assume}\ P\isactrlisub {\isadigit{1}}\isanewline
   1.906 +\ \ \ \ %
   1.907 +\isamarkupcmt{\dots%
   1.908 +}
   1.909 +\isanewline
   1.910 +\ \ \ \ \isamarkupfalse%
   1.911 +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.912 +\ %
   1.913 +\isamarkupcmt{\dots%
   1.914 +}
   1.915 +\ \isamarkupfalse%
   1.916 +\isacommand{{\isacharbraceright}}\isanewline
   1.917 +\ \ \isamarkupfalse%
   1.918 +\isacommand{moreover}\isanewline
   1.919 +\ \ \isamarkupfalse%
   1.920 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.921 +\isacommand{assume}\ P\isactrlisub {\isadigit{2}}\isanewline
   1.922 +\ \ \ \ %
   1.923 +\isamarkupcmt{\dots%
   1.924 +}
   1.925 +\isanewline
   1.926 +\ \ \ \ \isamarkupfalse%
   1.927 +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.928 +\ %
   1.929 +\isamarkupcmt{\dots%
   1.930 +}
   1.931 +\ \isamarkupfalse%
   1.932 +\isacommand{{\isacharbraceright}}\isanewline
   1.933 +\ \ \isamarkupfalse%
   1.934 +\isacommand{moreover}\isanewline
   1.935 +\ \ \isamarkupfalse%
   1.936 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   1.937 +\isacommand{assume}\ P\isactrlisub {\isadigit{3}}\isanewline
   1.938 +\ \ \ \ %
   1.939 +\isamarkupcmt{\dots%
   1.940 +}
   1.941 +\isanewline
   1.942 +\ \ \ \ \isamarkupfalse%
   1.943 +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.944 +\ %
   1.945 +\isamarkupcmt{\dots%
   1.946 +}
   1.947 +\ \isamarkupfalse%
   1.948 +\isacommand{{\isacharbraceright}}\isanewline
   1.949 +\ \ \isamarkupfalse%
   1.950 +\isacommand{ultimately}\ \isamarkupfalse%
   1.951 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   1.952 +\isacommand{by}\ blast\isanewline
   1.953  \isamarkupfalse%
   1.954 -\isamarkupfalse%
   1.955 -\isamarkupfalse%
   1.956 -\isamarkupfalse%
   1.957 -\isamarkupfalse%
   1.958 -\isamarkupfalse%
   1.959 -\isamarkupfalse%
   1.960 -\isamarkupfalse%
   1.961 -\isamarkupfalse%
   1.962 -\isamarkupfalse%
   1.963 -\isamarkupfalse%
   1.964 -\isamarkupfalse%
   1.965 -\isamarkupfalse%
   1.966 +\isacommand{qed}\isamarkupfalse%
   1.967  %
   1.968  \renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   1.969  %
   1.970 @@ -878,7 +1090,7 @@
   1.971  \ \ \ \ \ \ \ \ \ \ mono{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}x\ y\ z{\isacharcolon}{\isacharcolon}{\isacharprime}a{\isachardot}\ x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ x\ {\isacharplus}{\isacharplus}\ z\ {\isachargreater}\ y\ {\isacharplus}{\isacharplus}\ z{\isachardoublequote}\isanewline
   1.972  \ \ \isakeyword{shows}\ {\isachardoublequote}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequote}\isanewline
   1.973  \isamarkupfalse%
   1.974 -\isamarkupfalse%
   1.975 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}\isamarkupfalse%
   1.976  %
   1.977  \begin{isamarkuptext}%
   1.978  \noindent The concrete syntax is dropped at the end of the proof and the
   1.979 @@ -902,10 +1114,11 @@
   1.980  \isamarkuptrue%
   1.981  \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isasymexists}x\ y{\isachardot}\ P\ x\ y\ {\isasymand}\ Q\ x\ y{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}R{\isachardoublequote}\isanewline
   1.982  \isamarkupfalse%
   1.983 -\isamarkupfalse%
   1.984 -\isamarkupfalse%
   1.985 -\isamarkupfalse%
   1.986 -\isamarkupfalse%
   1.987 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.988 +\ \ \isamarkupfalse%
   1.989 +\isacommand{from}\ A\ \isamarkupfalse%
   1.990 +\isacommand{obtain}\ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequote}Q\ x\ y{\isachardoublequote}\ \ \isamarkupfalse%
   1.991 +\isacommand{by}\ blast\isamarkupfalse%
   1.992  \isamarkupfalse%
   1.993  %
   1.994  \begin{isamarkuptext}%
   1.995 @@ -926,15 +1139,23 @@
   1.996  \isamarkuptrue%
   1.997  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
   1.998  \isamarkupfalse%
   1.999 -\isamarkupfalse%
  1.1000 -\isamarkupfalse%
  1.1001 -\isamarkupfalse%
  1.1002 -\isamarkupfalse%
  1.1003 +\isacommand{proof}\isanewline
  1.1004 +\ \ \isamarkupfalse%
  1.1005 +\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
  1.1006 +\ \ \isamarkupfalse%
  1.1007 +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
  1.1008 +\ \ \ \ \isamarkupfalse%
  1.1009 +\isacommand{apply}{\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
  1.1010 +\ \ \ \ \isamarkupfalse%
  1.1011 +\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
  1.1012 +\ \ \ \ \isamarkupfalse%
  1.1013 +\isacommand{apply}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
  1.1014 +\ \ \ \ \isamarkupfalse%
  1.1015 +\isacommand{apply}\ assumption\isanewline
  1.1016 +\ \ \ \ \isamarkupfalse%
  1.1017 +\isacommand{done}\isanewline
  1.1018  \isamarkupfalse%
  1.1019 -\isamarkupfalse%
  1.1020 -\isamarkupfalse%
  1.1021 -\isamarkupfalse%
  1.1022 -\isamarkupfalse%
  1.1023 +\isacommand{qed}\isamarkupfalse%
  1.1024  %
  1.1025  \begin{isamarkuptext}%
  1.1026  \noindent You may need to resort to this technique if an