updated;
authorwenzelm
Fri Jun 17 18:36:25 2005 +0200 (2005-06-17)
changeset 164597efee005e568
parent 16458 4c6fd0c01d28
child 16460 72a08d509d62
updated;
doc-src/IsarOverview/Isar/document/Induction.tex
doc-src/IsarOverview/Isar/document/Logic.tex
     1.1 --- a/doc-src/IsarOverview/Isar/document/Induction.tex	Fri Jun 17 18:35:27 2005 +0200
     1.2 +++ b/doc-src/IsarOverview/Isar/document/Induction.tex	Fri Jun 17 18:36:25 2005 +0200
     1.3 @@ -26,15 +26,19 @@
     1.4  \isamarkuptrue%
     1.5  \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline
     1.6  \isamarkupfalse%
     1.7 -\isamarkupfalse%
     1.8 -\isamarkupfalse%
     1.9 -\isamarkupfalse%
    1.10 -\isamarkupfalse%
    1.11 +\isacommand{proof}\ cases\isanewline
    1.12 +\ \ \isamarkupfalse%
    1.13 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
    1.14 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
    1.15 +\isacommand{{\isachardot}{\isachardot}}\isanewline
    1.16  \isamarkupfalse%
    1.17 -\isamarkupfalse%
    1.18 +\isacommand{next}\isanewline
    1.19 +\ \ \isamarkupfalse%
    1.20 +\isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isamarkupfalse%
    1.21 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
    1.22 +\isacommand{{\isachardot}{\isachardot}}\isanewline
    1.23  \isamarkupfalse%
    1.24 -\isamarkupfalse%
    1.25 -\isamarkupfalse%
    1.26 +\isacommand{qed}\isamarkupfalse%
    1.27  %
    1.28  \begin{isamarkuptext}%
    1.29  \noindent The two cases must come in this order because \isa{cases} merely abbreviates \isa{{\isacharparenleft}rule\ case{\isacharunderscore}split{\isacharunderscore}thm{\isacharparenright}} where
    1.30 @@ -51,15 +55,19 @@
    1.31  \isamarkuptrue%
    1.32  \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ A{\isachardoublequote}\isanewline
    1.33  \isamarkupfalse%
    1.34 -\isamarkupfalse%
    1.35 -\isamarkupfalse%
    1.36 -\isamarkupfalse%
    1.37 -\isamarkupfalse%
    1.38 +\isacommand{proof}\ {\isacharparenleft}cases\ {\isachardoublequote}A{\isachardoublequote}{\isacharparenright}\isanewline
    1.39 +\ \ \isamarkupfalse%
    1.40 +\isacommand{case}\ True\ \isamarkupfalse%
    1.41 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
    1.42 +\isacommand{{\isachardot}{\isachardot}}\isanewline
    1.43  \isamarkupfalse%
    1.44 -\isamarkupfalse%
    1.45 +\isacommand{next}\isanewline
    1.46 +\ \ \isamarkupfalse%
    1.47 +\isacommand{case}\ False\ \isamarkupfalse%
    1.48 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
    1.49 +\isacommand{{\isachardot}{\isachardot}}\isanewline
    1.50  \isamarkupfalse%
    1.51 -\isamarkupfalse%
    1.52 -\isamarkupfalse%
    1.53 +\isacommand{qed}\isamarkupfalse%
    1.54  %
    1.55  \begin{isamarkuptext}%
    1.56  \noindent which is like the previous proof but instantiates
    1.57 @@ -76,15 +84,19 @@
    1.58  \isamarkupfalse%
    1.59  \isacommand{lemma}\ {\isachardoublequote}length{\isacharparenleft}tl\ xs{\isacharparenright}\ {\isacharequal}\ length\ xs\ {\isacharminus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
    1.60  \isamarkupfalse%
    1.61 -\isamarkupfalse%
    1.62 -\isamarkupfalse%
    1.63 -\isamarkupfalse%
    1.64 -\isamarkupfalse%
    1.65 +\isacommand{proof}\ {\isacharparenleft}cases\ xs{\isacharparenright}\isanewline
    1.66 +\ \ \isamarkupfalse%
    1.67 +\isacommand{case}\ Nil\ \isamarkupfalse%
    1.68 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
    1.69 +\isacommand{by}\ simp\isanewline
    1.70  \isamarkupfalse%
    1.71 -\isamarkupfalse%
    1.72 +\isacommand{next}\isanewline
    1.73 +\ \ \isamarkupfalse%
    1.74 +\isacommand{case}\ Cons\ \isamarkupfalse%
    1.75 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
    1.76 +\isacommand{by}\ simp\isanewline
    1.77  \isamarkupfalse%
    1.78 -\isamarkupfalse%
    1.79 -\isamarkupfalse%
    1.80 +\isacommand{qed}\isamarkupfalse%
    1.81  %
    1.82  \begin{isamarkuptext}%
    1.83  \noindent Here `\isakeyword{case}~\isa{Nil}' abbreviates
    1.84 @@ -117,7 +129,7 @@
    1.85  \isamarkuptrue%
    1.86  \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
    1.87  \isamarkupfalse%
    1.88 -\isamarkupfalse%
    1.89 +\isacommand{by}\ {\isacharparenleft}induct\ n{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isamarkupfalse%
    1.90  %
    1.91  \begin{isamarkuptext}%
    1.92  \noindent The constraint \isa{{\isacharcolon}{\isacharcolon}nat} is needed because all of
    1.93 @@ -130,15 +142,20 @@
    1.94  \isamarkuptrue%
    1.95  \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharequal}\ {\isadigit{0}}{\isachardot}{\isachardot}{\isacharless}n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
    1.96  \isamarkupfalse%
    1.97 -\isamarkupfalse%
    1.98 -\isamarkupfalse%
    1.99 -\isamarkupfalse%
   1.100 -\isamarkupfalse%
   1.101 +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
   1.102 +\ \ \isamarkupfalse%
   1.103 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse%
   1.104 +\isacommand{by}\ simp\isanewline
   1.105  \isamarkupfalse%
   1.106 -\isamarkupfalse%
   1.107 +\isacommand{next}\isanewline
   1.108 +\ \ \isamarkupfalse%
   1.109 +\isacommand{fix}\ n\ \isamarkupfalse%
   1.110 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline
   1.111 +\ \ \isamarkupfalse%
   1.112 +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}P{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   1.113 +\isacommand{by}\ simp\isanewline
   1.114  \isamarkupfalse%
   1.115 -\isamarkupfalse%
   1.116 -\isamarkupfalse%
   1.117 +\isacommand{qed}\isamarkupfalse%
   1.118  %
   1.119  \begin{isamarkuptext}%
   1.120  \noindent We could refine this further to show more of the equational
   1.121 @@ -148,15 +165,19 @@
   1.122  \isamarkuptrue%
   1.123  \isacommand{lemma}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i{\isacharcolon}{\isacharcolon}nat\ {\isacharless}\ n{\isacharplus}{\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}n{\isacharplus}{\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
   1.124  \isamarkupfalse%
   1.125 -\isamarkupfalse%
   1.126 -\isamarkupfalse%
   1.127 -\isamarkupfalse%
   1.128 -\isamarkupfalse%
   1.129 +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
   1.130 +\ \ \isamarkupfalse%
   1.131 +\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
   1.132 +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
   1.133 +\isacommand{by}\ simp\isanewline
   1.134  \isamarkupfalse%
   1.135 -\isamarkupfalse%
   1.136 +\isacommand{next}\isanewline
   1.137 +\ \ \isamarkupfalse%
   1.138 +\isacommand{case}\ Suc\ \isamarkupfalse%
   1.139 +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
   1.140 +\isacommand{by}\ simp\isanewline
   1.141  \isamarkupfalse%
   1.142 -\isamarkupfalse%
   1.143 -\isamarkupfalse%
   1.144 +\isacommand{qed}\isamarkupfalse%
   1.145  %
   1.146  \begin{isamarkuptext}%
   1.147  \noindent The implicitly defined \isa{{\isacharquery}case} refers to the
   1.148 @@ -171,15 +192,19 @@
   1.149  \isamarkuptrue%
   1.150  \isacommand{lemma}\ \isakeyword{fixes}\ n{\isacharcolon}{\isacharcolon}nat\ \isakeyword{shows}\ {\isachardoublequote}n\ {\isacharless}\ n{\isacharasterisk}n\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\isanewline
   1.151  \isamarkupfalse%
   1.152 -\isamarkupfalse%
   1.153 -\isamarkupfalse%
   1.154 -\isamarkupfalse%
   1.155 -\isamarkupfalse%
   1.156 +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
   1.157 +\ \ \isamarkupfalse%
   1.158 +\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
   1.159 +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
   1.160 +\isacommand{by}\ simp\isanewline
   1.161  \isamarkupfalse%
   1.162 -\isamarkupfalse%
   1.163 +\isacommand{next}\isanewline
   1.164 +\ \ \isamarkupfalse%
   1.165 +\isacommand{case}\ {\isacharparenleft}Suc\ i{\isacharparenright}\ \isamarkupfalse%
   1.166 +\isacommand{thus}\ {\isachardoublequote}Suc\ i\ {\isacharless}\ Suc\ i\ {\isacharasterisk}\ Suc\ i\ {\isacharplus}\ {\isadigit{1}}{\isachardoublequote}\ \isamarkupfalse%
   1.167 +\isacommand{by}\ simp\isanewline
   1.168  \isamarkupfalse%
   1.169 -\isamarkupfalse%
   1.170 -\isamarkupfalse%
   1.171 +\isacommand{qed}\isamarkupfalse%
   1.172  %
   1.173  \begin{isamarkuptext}%
   1.174  \noindent Of course we could again have written
   1.175 @@ -211,33 +236,56 @@
   1.176  \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isasymAnd}n{\isachardot}\ {\isacharparenleft}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isacharparenright}\ {\isasymLongrightarrow}\ P\ n{\isacharparenright}{\isachardoublequote}\isanewline
   1.177  \ \ \isakeyword{shows}\ {\isachardoublequote}P{\isacharparenleft}n{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequote}\isanewline
   1.178  \isamarkupfalse%
   1.179 -\isamarkupfalse%
   1.180 -\isamarkupfalse%
   1.181 -\isamarkupfalse%
   1.182 -\isamarkupfalse%
   1.183 -\isamarkupfalse%
   1.184 -\isamarkupfalse%
   1.185 -\isamarkupfalse%
   1.186 -\isamarkupfalse%
   1.187 -\isamarkupfalse%
   1.188 -\isamarkupfalse%
   1.189 -\isamarkupfalse%
   1.190 -\isamarkupfalse%
   1.191 -\isamarkupfalse%
   1.192 +\isacommand{proof}\ {\isacharparenleft}rule\ A{\isacharparenright}\isanewline
   1.193 +\ \ \isamarkupfalse%
   1.194 +\isacommand{show}\ {\isachardoublequote}{\isasymAnd}m{\isachardot}\ m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ m{\isachardoublequote}\isanewline
   1.195 +\ \ \isamarkupfalse%
   1.196 +\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
   1.197 +\ \ \ \ \isamarkupfalse%
   1.198 +\isacommand{case}\ {\isadigit{0}}\ \isamarkupfalse%
   1.199 +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
   1.200 +\isacommand{by}\ simp\isanewline
   1.201 +\ \ \isamarkupfalse%
   1.202 +\isacommand{next}\isanewline
   1.203 +\ \ \ \ \isamarkupfalse%
   1.204 +\isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\ \ \ %
   1.205 +\isamarkupcmt{\isakeyword{fix} \isa{m} \isakeyword{assume} \isa{Suc}: \isa{{\isachardoublequote}{\isacharquery}m\ {\isacharless}\ n\ {\isasymLongrightarrow}\ P\ {\isacharquery}m{\isachardoublequote}} \isa{{\isachardoublequote}m\ {\isacharless}\ Suc\ n{\isachardoublequote}}%
   1.206 +}
   1.207 +\isanewline
   1.208 +\ \ \ \ \isamarkupfalse%
   1.209 +\isacommand{show}\ {\isacharquery}case\ \ \ \ %
   1.210 +\isamarkupcmt{\isa{P\ m}%
   1.211 +}
   1.212 +\isanewline
   1.213 +\ \ \ \ \isamarkupfalse%
   1.214 +\isacommand{proof}\ cases\isanewline
   1.215 +\ \ \ \ \ \ \isamarkupfalse%
   1.216 +\isacommand{assume}\ eq{\isacharcolon}\ {\isachardoublequote}m\ {\isacharequal}\ n{\isachardoublequote}\isanewline
   1.217 +\ \ \ \ \ \ \isamarkupfalse%
   1.218 +\isacommand{from}\ Suc\ \isakeyword{and}\ A\ \isamarkupfalse%
   1.219 +\isacommand{have}\ {\isachardoublequote}P\ n{\isachardoublequote}\ \isamarkupfalse%
   1.220 +\isacommand{by}\ blast\isanewline
   1.221 +\ \ \ \ \ \ \isamarkupfalse%
   1.222 +\isacommand{with}\ eq\ \isamarkupfalse%
   1.223 +\isacommand{show}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse%
   1.224 +\isacommand{by}\ simp\isanewline
   1.225 +\ \ \ \ \isamarkupfalse%
   1.226 +\isacommand{next}\isanewline
   1.227 +\ \ \ \ \ \ \isamarkupfalse%
   1.228 +\isacommand{assume}\ {\isachardoublequote}m\ {\isasymnoteq}\ n{\isachardoublequote}\isanewline
   1.229 +\ \ \ \ \ \ \isamarkupfalse%
   1.230 +\isacommand{with}\ Suc\ \isamarkupfalse%
   1.231 +\isacommand{have}\ {\isachardoublequote}m\ {\isacharless}\ n{\isachardoublequote}\ \isamarkupfalse%
   1.232 +\isacommand{by}\ arith\isanewline
   1.233 +\ \ \ \ \ \ \isamarkupfalse%
   1.234 +\isacommand{thus}\ {\isachardoublequote}P\ m{\isachardoublequote}\ \isamarkupfalse%
   1.235 +\isacommand{by}{\isacharparenleft}rule\ Suc{\isacharparenright}\isanewline
   1.236 +\ \ \ \ \isamarkupfalse%
   1.237 +\isacommand{qed}\isanewline
   1.238 +\ \ \isamarkupfalse%
   1.239 +\isacommand{qed}\isanewline
   1.240  \isamarkupfalse%
   1.241 -\isamarkupfalse%
   1.242 -\isamarkupfalse%
   1.243 -\isamarkupfalse%
   1.244 -\isamarkupfalse%
   1.245 -\isamarkupfalse%
   1.246 -\isamarkupfalse%
   1.247 -\isamarkupfalse%
   1.248 -\isamarkupfalse%
   1.249 -\isamarkupfalse%
   1.250 -\isamarkupfalse%
   1.251 -\isamarkupfalse%
   1.252 -\isamarkupfalse%
   1.253 -\isamarkupfalse%
   1.254 +\isacommand{qed}\isamarkupfalse%
   1.255  %
   1.256  \begin{isamarkuptext}%
   1.257  \noindent Given the explanations above and the comments in the
   1.258 @@ -284,16 +332,21 @@
   1.259  \isamarkuptrue%
   1.260  \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
   1.261  \isamarkupfalse%
   1.262 -\isamarkupfalse%
   1.263 +\isacommand{using}\ A\isanewline
   1.264  \isamarkupfalse%
   1.265 -\isamarkupfalse%
   1.266 -\isamarkupfalse%
   1.267 +\isacommand{proof}\ induct\isanewline
   1.268 +\ \ \isamarkupfalse%
   1.269 +\isacommand{case}\ refl\ \isamarkupfalse%
   1.270 +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
   1.271 +\isacommand{{\isachardot}}\isanewline
   1.272  \isamarkupfalse%
   1.273 -\isamarkupfalse%
   1.274 -\isamarkupfalse%
   1.275 +\isacommand{next}\isanewline
   1.276 +\ \ \isamarkupfalse%
   1.277 +\isacommand{case}\ step\ \isamarkupfalse%
   1.278 +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
   1.279 +\isacommand{by}{\isacharparenleft}blast\ intro{\isacharcolon}\ rtc{\isachardot}step{\isacharparenright}\isanewline
   1.280  \isamarkupfalse%
   1.281 -\isamarkupfalse%
   1.282 -\isamarkupfalse%
   1.283 +\isacommand{qed}\isamarkupfalse%
   1.284  %
   1.285  \begin{isamarkuptext}%
   1.286  \noindent Rule induction is triggered by a fact $(x_1,\dots,x_n)
   1.287 @@ -308,22 +361,37 @@
   1.288  \isacommand{lemma}\ \isakeyword{assumes}\ A{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}y{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\ B{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
   1.289  \ \ \isakeyword{shows}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
   1.290  \isamarkupfalse%
   1.291 -\isamarkupfalse%
   1.292 -\isamarkupfalse%
   1.293 -\isamarkupfalse%
   1.294 -\isamarkupfalse%
   1.295 -\isamarkupfalse%
   1.296 -\isamarkupfalse%
   1.297 -\isamarkupfalse%
   1.298 +\isacommand{proof}\ {\isacharminus}\isanewline
   1.299 +\ \ \isamarkupfalse%
   1.300 +\isacommand{from}\ A\ B\ \isamarkupfalse%
   1.301 +\isacommand{show}\ {\isacharquery}thesis\isanewline
   1.302 +\ \ \isamarkupfalse%
   1.303 +\isacommand{proof}\ induct\isanewline
   1.304 +\ \ \ \ \isamarkupfalse%
   1.305 +\isacommand{fix}\ x\ \isamarkupfalse%
   1.306 +\isacommand{assume}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \ %
   1.307 +\isamarkupcmt{\isa{B}[\isa{y} := \isa{x}]%
   1.308 +}
   1.309 +\isanewline
   1.310 +\ \ \ \ \isamarkupfalse%
   1.311 +\isacommand{thus}\ {\isachardoublequote}{\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse%
   1.312 +\isacommand{{\isachardot}}\isanewline
   1.313 +\ \ \isamarkupfalse%
   1.314 +\isacommand{next}\isanewline
   1.315 +\ \ \ \ \isamarkupfalse%
   1.316 +\isacommand{fix}\ x{\isacharprime}\ x\ y\isanewline
   1.317 +\ \ \ \ \isamarkupfalse%
   1.318 +\isacommand{assume}\ {\isadigit{1}}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}x{\isacharparenright}\ {\isasymin}\ r{\isachardoublequote}\ \isakeyword{and}\isanewline
   1.319 +\ \ \ \ \ \ \ \ \ \ \ IH{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}\ {\isasymLongrightarrow}\ {\isacharparenleft}x{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isakeyword{and}\isanewline
   1.320 +\ \ \ \ \ \ \ \ \ \ \ B{\isacharcolon}\ \ {\isachardoublequote}{\isacharparenleft}y{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\isanewline
   1.321 +\ \ \ \ \isamarkupfalse%
   1.322 +\isacommand{from}\ {\isadigit{1}}\ IH{\isacharbrackleft}OF\ B{\isacharbrackright}\ \isamarkupfalse%
   1.323 +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}x{\isacharprime}{\isacharcomma}z{\isacharparenright}\ {\isasymin}\ r{\isacharasterisk}{\isachardoublequote}\ \isamarkupfalse%
   1.324 +\isacommand{by}{\isacharparenleft}rule\ rtc{\isachardot}step{\isacharparenright}\isanewline
   1.325 +\ \ \isamarkupfalse%
   1.326 +\isacommand{qed}\isanewline
   1.327  \isamarkupfalse%
   1.328 -\isamarkupfalse%
   1.329 -\isamarkupfalse%
   1.330 -\isamarkupfalse%
   1.331 -\isamarkupfalse%
   1.332 -\isamarkupfalse%
   1.333 -\isamarkupfalse%
   1.334 -\isamarkupfalse%
   1.335 -\isamarkupfalse%
   1.336 +\isacommand{qed}\isamarkupfalse%
   1.337  %
   1.338  \begin{isamarkuptext}%
   1.339  \noindent We start the proof with \isakeyword{from}~\isa{A\ B}. Only \isa{A} is ``consumed'' by the induction step.
   1.340 @@ -381,28 +449,38 @@
   1.341  \isamarkuptrue%
   1.342  \isacommand{lemma}\ {\isachardoublequote}xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ rot\ xs\ {\isacharequal}\ tl\ xs\ {\isacharat}\ {\isacharbrackleft}hd\ xs{\isacharbrackright}{\isachardoublequote}\isanewline
   1.343  \isamarkupfalse%
   1.344 -\isamarkupfalse%
   1.345 -\isamarkupfalse%
   1.346 -\isamarkupfalse%
   1.347 -\isamarkupfalse%
   1.348 +\isacommand{proof}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharparenright}\isanewline
   1.349 +\ \ \isamarkupfalse%
   1.350 +\isacommand{case}\ {\isadigit{1}}\ \isamarkupfalse%
   1.351 +\isacommand{thus}\ {\isacharquery}case\ \isamarkupfalse%
   1.352 +\isacommand{by}\ simp\isanewline
   1.353  \isamarkupfalse%
   1.354 -\isamarkupfalse%
   1.355 -\isamarkupfalse%
   1.356 -\isamarkupfalse%
   1.357 -\isamarkupfalse%
   1.358 -\isamarkupfalse%
   1.359 +\isacommand{next}\isanewline
   1.360 +\ \ \isamarkupfalse%
   1.361 +\isacommand{case}\ {\isadigit{2}}\ \isamarkupfalse%
   1.362 +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
   1.363 +\isacommand{by}\ simp\isanewline
   1.364  \isamarkupfalse%
   1.365 -\isamarkupfalse%
   1.366 -\isamarkupfalse%
   1.367 -\isamarkupfalse%
   1.368 -\isamarkupfalse%
   1.369 -\isamarkupfalse%
   1.370 +\isacommand{next}\isanewline
   1.371 +\ \ \isamarkupfalse%
   1.372 +\isacommand{case}\ {\isacharparenleft}{\isadigit{3}}\ a\ b\ cs{\isacharparenright}\isanewline
   1.373 +\ \ \isamarkupfalse%
   1.374 +\isacommand{have}\ {\isachardoublequote}rot\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharequal}\ b\ {\isacharhash}\ rot{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   1.375 +\isacommand{by}\ simp\isanewline
   1.376 +\ \ \isamarkupfalse%
   1.377 +\isacommand{also}\ \isamarkupfalse%
   1.378 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ b\ {\isacharhash}\ tl{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd{\isacharparenleft}a\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse%
   1.379 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}{\isadigit{3}}{\isacharparenright}\isanewline
   1.380 +\ \ \isamarkupfalse%
   1.381 +\isacommand{also}\ \isamarkupfalse%
   1.382 +\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ tl\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}\ {\isacharat}\ {\isacharbrackleft}hd\ {\isacharparenleft}a\ {\isacharhash}\ b\ {\isacharhash}\ cs{\isacharparenright}{\isacharbrackright}{\isachardoublequote}\ \isamarkupfalse%
   1.383 +\isacommand{by}\ simp\isanewline
   1.384 +\ \ \isamarkupfalse%
   1.385 +\isacommand{finally}\ \isamarkupfalse%
   1.386 +\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
   1.387 +\isacommand{{\isachardot}}\isanewline
   1.388  \isamarkupfalse%
   1.389 -\isamarkupfalse%
   1.390 -\isamarkupfalse%
   1.391 -\isamarkupfalse%
   1.392 -\isamarkupfalse%
   1.393 -\isamarkupfalse%
   1.394 +\isacommand{qed}\isamarkupfalse%
   1.395  %
   1.396  \begin{isamarkuptext}%
   1.397  \noindent
   1.398 @@ -420,7 +498,7 @@
   1.399  \end{isamarkuptext}%
   1.400  \isamarkuptrue%
   1.401  \isamarkupfalse%
   1.402 -\isanewline
   1.403 +\isacommand{by}\ {\isacharparenleft}induct\ xs\ rule{\isacharcolon}\ rot{\isachardot}induct{\isacharcomma}\ simp{\isacharunderscore}all{\isacharparenright}\isanewline
   1.404  \isamarkupfalse%
   1.405  \isamarkupfalse%
   1.406  \end{isabellebody}%
     2.1 --- a/doc-src/IsarOverview/Isar/document/Logic.tex	Fri Jun 17 18:35:27 2005 +0200
     2.2 +++ b/doc-src/IsarOverview/Isar/document/Logic.tex	Fri Jun 17 18:36:25 2005 +0200
     2.3 @@ -22,11 +22,14 @@
     2.4  \isamarkuptrue%
     2.5  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
     2.6  \isamarkupfalse%
     2.7 -\isamarkupfalse%
     2.8 -\isamarkupfalse%
     2.9 +\isacommand{proof}\ {\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
    2.10 +\ \ \isamarkupfalse%
    2.11 +\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    2.12 +\ \ \isamarkupfalse%
    2.13 +\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
    2.14 +\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
    2.15  \isamarkupfalse%
    2.16 -\isamarkupfalse%
    2.17 -\isamarkupfalse%
    2.18 +\isacommand{qed}\isamarkupfalse%
    2.19  %
    2.20  \begin{isamarkuptext}%
    2.21  \noindent
    2.22 @@ -42,11 +45,14 @@
    2.23  \isamarkuptrue%
    2.24  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
    2.25  \isamarkupfalse%
    2.26 -\isamarkupfalse%
    2.27 -\isamarkupfalse%
    2.28 +\isacommand{proof}\isanewline
    2.29 +\ \ \isamarkupfalse%
    2.30 +\isacommand{assume}\ a{\isacharcolon}\ A\isanewline
    2.31 +\ \ \isamarkupfalse%
    2.32 +\isacommand{show}\ A\ \isamarkupfalse%
    2.33 +\isacommand{by}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
    2.34  \isamarkupfalse%
    2.35 -\isamarkupfalse%
    2.36 -\isamarkupfalse%
    2.37 +\isacommand{qed}\isamarkupfalse%
    2.38  %
    2.39  \begin{isamarkuptext}%
    2.40  \noindent Single-identifier formulae such as \isa{A} need not
    2.41 @@ -60,11 +66,14 @@
    2.42  \isamarkuptrue%
    2.43  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A{\isachardoublequote}\isanewline
    2.44  \isamarkupfalse%
    2.45 -\isamarkupfalse%
    2.46 -\isamarkupfalse%
    2.47 +\isacommand{proof}\isanewline
    2.48 +\ \ \isamarkupfalse%
    2.49 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    2.50 +\ \ \isamarkupfalse%
    2.51 +\isacommand{show}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
    2.52 +\isacommand{{\isachardot}}\isanewline
    2.53  \isamarkupfalse%
    2.54 -\isamarkupfalse%
    2.55 -\isamarkupfalse%
    2.56 +\isacommand{qed}\isamarkupfalse%
    2.57  %
    2.58  \begin{isamarkuptext}%
    2.59  To hide proofs by assumption further, \isakeyword{by}\isa{{\isacharparenleft}method{\isacharparenright}}
    2.60 @@ -74,11 +83,14 @@
    2.61  \isamarkuptrue%
    2.62  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
    2.63  \isamarkupfalse%
    2.64 -\isamarkupfalse%
    2.65 -\isamarkupfalse%
    2.66 +\isacommand{proof}\isanewline
    2.67 +\ \ \isamarkupfalse%
    2.68 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    2.69 +\ \ \isamarkupfalse%
    2.70 +\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
    2.71 +\isacommand{by}{\isacharparenleft}rule\ conjI{\isacharparenright}\isanewline
    2.72  \isamarkupfalse%
    2.73 -\isamarkupfalse%
    2.74 -\isamarkupfalse%
    2.75 +\isacommand{qed}\isamarkupfalse%
    2.76  %
    2.77  \begin{isamarkuptext}%
    2.78  \noindent Rule \isa{conjI} is of course \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}.
    2.79 @@ -92,11 +104,14 @@
    2.80  \isamarkuptrue%
    2.81  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ A\ {\isasymand}\ A{\isachardoublequote}\isanewline
    2.82  \isamarkupfalse%
    2.83 -\isamarkupfalse%
    2.84 -\isamarkupfalse%
    2.85 +\isacommand{proof}\isanewline
    2.86 +\ \ \isamarkupfalse%
    2.87 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
    2.88 +\ \ \isamarkupfalse%
    2.89 +\isacommand{show}\ {\isachardoublequote}A\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
    2.90 +\isacommand{{\isachardot}{\isachardot}}\isanewline
    2.91  \isamarkupfalse%
    2.92 -\isamarkupfalse%
    2.93 -\isamarkupfalse%
    2.94 +\isacommand{qed}\isamarkupfalse%
    2.95  %
    2.96  \begin{isamarkuptext}%
    2.97  \noindent
    2.98 @@ -121,15 +136,25 @@
    2.99  \isamarkuptrue%
   2.100  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.101  \isamarkupfalse%
   2.102 -\isamarkupfalse%
   2.103 -\isamarkupfalse%
   2.104 -\isamarkupfalse%
   2.105 -\isamarkupfalse%
   2.106 +\isacommand{proof}\isanewline
   2.107 +\ \ \isamarkupfalse%
   2.108 +\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   2.109 +\ \ \isamarkupfalse%
   2.110 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.111 +\ \ \isamarkupfalse%
   2.112 +\isacommand{proof}\ {\isacharparenleft}rule\ conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}{\isacharparenright}\ \ %
   2.113 +\isamarkupcmt{\isa{conjE{\isacharbrackleft}OF\ AB{\isacharbrackright}}: \isa{{\isacharparenleft}{\isasymlbrakk}A{\isacharsemicolon}\ B{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
   2.114 +}
   2.115 +\isanewline
   2.116 +\ \ \ \ \isamarkupfalse%
   2.117 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   2.118 +\ \ \ \ \isamarkupfalse%
   2.119 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.120 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.121 +\ \ \isamarkupfalse%
   2.122 +\isacommand{qed}\isanewline
   2.123  \isamarkupfalse%
   2.124 -\isamarkupfalse%
   2.125 -\isamarkupfalse%
   2.126 -\isamarkupfalse%
   2.127 -\isamarkupfalse%
   2.128 +\isacommand{qed}\isamarkupfalse%
   2.129  %
   2.130  \begin{isamarkuptext}%
   2.131  \noindent Note that the term \isa{{\isacharquery}thesis} always stands for the
   2.132 @@ -155,16 +180,23 @@
   2.133  \isamarkuptrue%
   2.134  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.135  \isamarkupfalse%
   2.136 -\isamarkupfalse%
   2.137 -\isamarkupfalse%
   2.138 -\isamarkupfalse%
   2.139 -\isamarkupfalse%
   2.140 +\isacommand{proof}\isanewline
   2.141 +\ \ \isamarkupfalse%
   2.142 +\isacommand{assume}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   2.143 +\ \ \isamarkupfalse%
   2.144 +\isacommand{from}\ AB\ \isamarkupfalse%
   2.145 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.146 +\ \ \isamarkupfalse%
   2.147 +\isacommand{proof}\isanewline
   2.148 +\ \ \ \ \isamarkupfalse%
   2.149 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   2.150 +\ \ \ \ \isamarkupfalse%
   2.151 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.152 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.153 +\ \ \isamarkupfalse%
   2.154 +\isacommand{qed}\isanewline
   2.155  \isamarkupfalse%
   2.156 -\isamarkupfalse%
   2.157 -\isamarkupfalse%
   2.158 -\isamarkupfalse%
   2.159 -\isamarkupfalse%
   2.160 -\isamarkupfalse%
   2.161 +\isacommand{qed}\isamarkupfalse%
   2.162  %
   2.163  \begin{isamarkuptext}%
   2.164  Now we come to a second important principle:
   2.165 @@ -178,16 +210,23 @@
   2.166  \isamarkuptrue%
   2.167  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.168  \isamarkupfalse%
   2.169 -\isamarkupfalse%
   2.170 -\isamarkupfalse%
   2.171 -\isamarkupfalse%
   2.172 -\isamarkupfalse%
   2.173 +\isacommand{proof}\isanewline
   2.174 +\ \ \isamarkupfalse%
   2.175 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   2.176 +\ \ \isamarkupfalse%
   2.177 +\isacommand{from}\ this\ \isamarkupfalse%
   2.178 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.179 +\ \ \isamarkupfalse%
   2.180 +\isacommand{proof}\isanewline
   2.181 +\ \ \ \ \isamarkupfalse%
   2.182 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   2.183 +\ \ \ \ \isamarkupfalse%
   2.184 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.185 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.186 +\ \ \isamarkupfalse%
   2.187 +\isacommand{qed}\isanewline
   2.188  \isamarkupfalse%
   2.189 -\isamarkupfalse%
   2.190 -\isamarkupfalse%
   2.191 -\isamarkupfalse%
   2.192 -\isamarkupfalse%
   2.193 -\isamarkupfalse%
   2.194 +\isacommand{qed}\isamarkupfalse%
   2.195  %
   2.196  \begin{isamarkuptext}%
   2.197  \noindent Because of the frequency of \isakeyword{from}~\isa{this}, Isar provides two abbreviations:
   2.198 @@ -203,18 +242,23 @@
   2.199  \isamarkuptrue%
   2.200  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.201  \isamarkupfalse%
   2.202 -\isamarkupfalse%
   2.203 -\isamarkupfalse%
   2.204 -\isamarkupfalse%
   2.205 -\isamarkupfalse%
   2.206 -\isamarkupfalse%
   2.207 +\isacommand{proof}\isanewline
   2.208 +\ \ \isamarkupfalse%
   2.209 +\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   2.210 +\ \ \isamarkupfalse%
   2.211 +\isacommand{from}\ ab\ \isamarkupfalse%
   2.212 +\isacommand{have}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   2.213 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.214 +\ \ \isamarkupfalse%
   2.215 +\isacommand{from}\ ab\ \isamarkupfalse%
   2.216 +\isacommand{have}\ b{\isacharcolon}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   2.217 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.218 +\ \ \isamarkupfalse%
   2.219 +\isacommand{from}\ b\ a\ \isamarkupfalse%
   2.220 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
   2.221 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.222  \isamarkupfalse%
   2.223 -\isamarkupfalse%
   2.224 -\isamarkupfalse%
   2.225 -\isamarkupfalse%
   2.226 -\isamarkupfalse%
   2.227 -\isamarkupfalse%
   2.228 -\isamarkupfalse%
   2.229 +\isacommand{qed}\isamarkupfalse%
   2.230  %
   2.231  \begin{isamarkuptext}%
   2.232  \noindent It is worth examining this text in detail because it
   2.233 @@ -265,19 +309,25 @@
   2.234  \isamarkuptrue%
   2.235  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymlongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.236  \isamarkupfalse%
   2.237 -\isamarkupfalse%
   2.238 -\isamarkupfalse%
   2.239 -\isamarkupfalse%
   2.240 -\isamarkupfalse%
   2.241 -\isamarkupfalse%
   2.242 -\isamarkupfalse%
   2.243 +\isacommand{proof}\isanewline
   2.244 +\ \ \isamarkupfalse%
   2.245 +\isacommand{assume}\ ab{\isacharcolon}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
   2.246 +\ \ \isamarkupfalse%
   2.247 +\isacommand{from}\ ab\ \isamarkupfalse%
   2.248 +\isacommand{have}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   2.249 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.250 +\ \ \isamarkupfalse%
   2.251 +\isacommand{moreover}\isanewline
   2.252 +\ \ \isamarkupfalse%
   2.253 +\isacommand{from}\ ab\ \isamarkupfalse%
   2.254 +\isacommand{have}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   2.255 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.256 +\ \ \isamarkupfalse%
   2.257 +\isacommand{ultimately}\ \isamarkupfalse%
   2.258 +\isacommand{show}\ {\isachardoublequote}B\ {\isasymand}\ A{\isachardoublequote}\ \isamarkupfalse%
   2.259 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.260  \isamarkupfalse%
   2.261 -\isamarkupfalse%
   2.262 -\isamarkupfalse%
   2.263 -\isamarkupfalse%
   2.264 -\isamarkupfalse%
   2.265 -\isamarkupfalse%
   2.266 -\isamarkupfalse%
   2.267 +\isacommand{qed}\isamarkupfalse%
   2.268  %
   2.269  \begin{isamarkuptext}%
   2.270  \noindent You can combine any number of facts \isa{A{\isadigit{1}}} \dots\ \isa{An} into a sequence by separating their proofs with
   2.271 @@ -296,36 +346,56 @@
   2.272  \isamarkuptrue%
   2.273  \isacommand{lemma}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ {\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
   2.274  \isamarkupfalse%
   2.275 -\isamarkupfalse%
   2.276 -\isamarkupfalse%
   2.277 -\isamarkupfalse%
   2.278 -\isamarkupfalse%
   2.279 -\isamarkupfalse%
   2.280 -\isamarkupfalse%
   2.281 -\isamarkupfalse%
   2.282 -\isamarkupfalse%
   2.283 -\isamarkupfalse%
   2.284 -\isamarkupfalse%
   2.285 -\isamarkupfalse%
   2.286 -\isamarkupfalse%
   2.287 -\isamarkupfalse%
   2.288 -\isamarkupfalse%
   2.289 +\isacommand{proof}\isanewline
   2.290 +\ \ \isamarkupfalse%
   2.291 +\isacommand{assume}\ n{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}A\ {\isasymand}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   2.292 +\ \ \isamarkupfalse%
   2.293 +\isacommand{show}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\isanewline
   2.294 +\ \ \isamarkupfalse%
   2.295 +\isacommand{proof}\ {\isacharparenleft}rule\ ccontr{\isacharparenright}\isanewline
   2.296 +\ \ \ \ \isamarkupfalse%
   2.297 +\isacommand{assume}\ nn{\isacharcolon}\ {\isachardoublequote}{\isasymnot}\ {\isacharparenleft}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isacharparenright}{\isachardoublequote}\isanewline
   2.298 +\ \ \ \ \isamarkupfalse%
   2.299 +\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline
   2.300 +\ \ \ \ \isamarkupfalse%
   2.301 +\isacommand{proof}\isanewline
   2.302 +\ \ \ \ \ \ \isamarkupfalse%
   2.303 +\isacommand{assume}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
   2.304 +\ \ \ \ \ \ \isamarkupfalse%
   2.305 +\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ B{\isachardoublequote}\isanewline
   2.306 +\ \ \ \ \ \ \isamarkupfalse%
   2.307 +\isacommand{proof}\isanewline
   2.308 +\ \ \ \ \ \ \ \ \isamarkupfalse%
   2.309 +\isacommand{assume}\ {\isachardoublequote}B{\isachardoublequote}\isanewline
   2.310 +\ \ \ \ \ \ \ \ \isamarkupfalse%
   2.311 +\isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   2.312 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.313 +\ \ \ \ \ \ \ \ \isamarkupfalse%
   2.314 +\isacommand{with}\ n\ \isamarkupfalse%
   2.315 +\isacommand{show}\ False\ \isamarkupfalse%
   2.316 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.317 +\ \ \ \ \ \ \isamarkupfalse%
   2.318 +\isacommand{qed}\isanewline
   2.319 +\ \ \ \ \ \ \isamarkupfalse%
   2.320 +\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
   2.321 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.322 +\ \ \ \ \ \ \isamarkupfalse%
   2.323 +\isacommand{with}\ nn\ \isamarkupfalse%
   2.324 +\isacommand{show}\ False\ \isamarkupfalse%
   2.325 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.326 +\ \ \ \ \isamarkupfalse%
   2.327 +\isacommand{qed}\isanewline
   2.328 +\ \ \ \ \isamarkupfalse%
   2.329 +\isacommand{hence}\ {\isachardoublequote}{\isasymnot}\ A\ {\isasymor}\ {\isasymnot}\ B{\isachardoublequote}\ \isamarkupfalse%
   2.330 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.331 +\ \ \ \ \isamarkupfalse%
   2.332 +\isacommand{with}\ nn\ \isamarkupfalse%
   2.333 +\isacommand{show}\ False\ \isamarkupfalse%
   2.334 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.335 +\ \ \isamarkupfalse%
   2.336 +\isacommand{qed}\isanewline
   2.337  \isamarkupfalse%
   2.338 -\isamarkupfalse%
   2.339 -\isamarkupfalse%
   2.340 -\isamarkupfalse%
   2.341 -\isamarkupfalse%
   2.342 -\isamarkupfalse%
   2.343 -\isamarkupfalse%
   2.344 -\isamarkupfalse%
   2.345 -\isamarkupfalse%
   2.346 -\isamarkupfalse%
   2.347 -\isamarkupfalse%
   2.348 -\isamarkupfalse%
   2.349 -\isamarkupfalse%
   2.350 -\isamarkupfalse%
   2.351 -\isamarkupfalse%
   2.352 -\isamarkupfalse%
   2.353 +\isacommand{qed}\isamarkupfalse%
   2.354  %
   2.355  \begin{isamarkuptext}%
   2.356  \noindent
   2.357 @@ -355,15 +425,19 @@
   2.358  \isamarkuptrue%
   2.359  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B\ {\isasymand}\ A{\isachardoublequote}\isanewline
   2.360  \isamarkupfalse%
   2.361 -\isamarkupfalse%
   2.362 -\isamarkupfalse%
   2.363 -\isamarkupfalse%
   2.364 -\isamarkupfalse%
   2.365 +\isacommand{proof}\isanewline
   2.366 +\ \ \isamarkupfalse%
   2.367 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   2.368 +\isacommand{thus}\ {\isachardoublequote}B{\isachardoublequote}\ \isamarkupfalse%
   2.369 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.370  \isamarkupfalse%
   2.371 -\isamarkupfalse%
   2.372 +\isacommand{next}\isanewline
   2.373 +\ \ \isamarkupfalse%
   2.374 +\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\ \isamarkupfalse%
   2.375 +\isacommand{thus}\ {\isachardoublequote}A{\isachardoublequote}\ \isamarkupfalse%
   2.376 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.377  \isamarkupfalse%
   2.378 -\isamarkupfalse%
   2.379 -\isamarkupfalse%
   2.380 +\isacommand{qed}\isamarkupfalse%
   2.381  %
   2.382  \begin{isamarkuptext}%
   2.383  \noindent The \isakeyword{proof} always works on the conclusion,
   2.384 @@ -394,15 +468,19 @@
   2.385  \isacommand{lemma}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B\ {\isasymLongrightarrow}\ large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\isanewline
   2.386  \ \ \ \ \ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}AB\ {\isasymLongrightarrow}\ {\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   2.387  \isamarkupfalse%
   2.388 -\isamarkupfalse%
   2.389 -\isamarkupfalse%
   2.390 -\isamarkupfalse%
   2.391 -\isamarkupfalse%
   2.392 +\isacommand{proof}\isanewline
   2.393 +\ \ \isamarkupfalse%
   2.394 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
   2.395 +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   2.396 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.397  \isamarkupfalse%
   2.398 -\isamarkupfalse%
   2.399 +\isacommand{next}\isanewline
   2.400 +\ \ \isamarkupfalse%
   2.401 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}AB{\isachardoublequote}\ \isamarkupfalse%
   2.402 +\isacommand{thus}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
   2.403 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.404  \isamarkupfalse%
   2.405 -\isamarkupfalse%
   2.406 -\isamarkupfalse%
   2.407 +\isacommand{qed}\isamarkupfalse%
   2.408  %
   2.409  \begin{isamarkuptext}%
   2.410  \noindent Any formula may be followed by
   2.411 @@ -419,15 +497,19 @@
   2.412  \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
   2.413  \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   2.414  \isamarkupfalse%
   2.415 -\isamarkupfalse%
   2.416 -\isamarkupfalse%
   2.417 -\isamarkupfalse%
   2.418 -\isamarkupfalse%
   2.419 +\isacommand{proof}\isanewline
   2.420 +\ \ \isamarkupfalse%
   2.421 +\isacommand{from}\ AB\ \isamarkupfalse%
   2.422 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   2.423 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.424  \isamarkupfalse%
   2.425 -\isamarkupfalse%
   2.426 +\isacommand{next}\isanewline
   2.427 +\ \ \isamarkupfalse%
   2.428 +\isacommand{from}\ AB\ \isamarkupfalse%
   2.429 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ \isamarkupfalse%
   2.430 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.431  \isamarkupfalse%
   2.432 -\isamarkupfalse%
   2.433 -\isamarkupfalse%
   2.434 +\isacommand{qed}\isamarkupfalse%
   2.435  %
   2.436  \begin{isamarkuptext}%
   2.437  \noindent Note the difference between \isa{{\isacharquery}AB}, a term, and
   2.438 @@ -441,12 +523,15 @@
   2.439  \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}large{\isacharunderscore}A\ {\isasymand}\ large{\isacharunderscore}B{\isachardoublequote}\isanewline
   2.440  \ \ \isakeyword{shows}\ {\isachardoublequote}large{\isacharunderscore}B\ {\isasymand}\ large{\isacharunderscore}A{\isachardoublequote}\ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}B\ {\isasymand}\ {\isacharquery}A{\isachardoublequote}{\isacharparenright}\isanewline
   2.441  \isamarkupfalse%
   2.442 -\isamarkupfalse%
   2.443 -\isamarkupfalse%
   2.444 +\isacommand{using}\ AB\isanewline
   2.445  \isamarkupfalse%
   2.446 -\isamarkupfalse%
   2.447 +\isacommand{proof}\isanewline
   2.448 +\ \ \isamarkupfalse%
   2.449 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}A{\isachardoublequote}\ {\isachardoublequote}{\isacharquery}B{\isachardoublequote}\ \isamarkupfalse%
   2.450 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.451 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.452  \isamarkupfalse%
   2.453 -\isamarkupfalse%
   2.454 +\isacommand{qed}\isamarkupfalse%
   2.455  %
   2.456  \begin{isamarkuptext}%
   2.457  \noindent Command \isakeyword{using} can appear before a proof
   2.458 @@ -468,19 +553,26 @@
   2.459  \isamarkuptrue%
   2.460  \isacommand{lemma}\ \isakeyword{assumes}\ AB{\isacharcolon}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isakeyword{shows}\ {\isachardoublequote}B\ {\isasymor}\ A{\isachardoublequote}\isanewline
   2.461  \isamarkupfalse%
   2.462 -\isamarkupfalse%
   2.463 -\isamarkupfalse%
   2.464 -\isamarkupfalse%
   2.465 -\isamarkupfalse%
   2.466 -\isamarkupfalse%
   2.467 -\isamarkupfalse%
   2.468 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.469 +\ \ \isamarkupfalse%
   2.470 +\isacommand{from}\ AB\ \isamarkupfalse%
   2.471 +\isacommand{show}\ {\isacharquery}thesis\isanewline
   2.472 +\ \ \isamarkupfalse%
   2.473 +\isacommand{proof}\isanewline
   2.474 +\ \ \ \ \isamarkupfalse%
   2.475 +\isacommand{assume}\ A\ \isamarkupfalse%
   2.476 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.477 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.478 +\ \ \isamarkupfalse%
   2.479 +\isacommand{next}\isanewline
   2.480 +\ \ \ \ \isamarkupfalse%
   2.481 +\isacommand{assume}\ B\ \isamarkupfalse%
   2.482 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.483 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.484 +\ \ \isamarkupfalse%
   2.485 +\isacommand{qed}\isanewline
   2.486  \isamarkupfalse%
   2.487 -\isamarkupfalse%
   2.488 -\isamarkupfalse%
   2.489 -\isamarkupfalse%
   2.490 -\isamarkupfalse%
   2.491 -\isamarkupfalse%
   2.492 -\isamarkupfalse%
   2.493 +\isacommand{qed}\isamarkupfalse%
   2.494  %
   2.495  \isamarkupsubsection{Predicate calculus%
   2.496  }
   2.497 @@ -497,12 +589,21 @@
   2.498  \isamarkuptrue%
   2.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
   2.500  \isamarkupfalse%
   2.501 -\isamarkupfalse%
   2.502 -\isamarkupfalse%
   2.503 +\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ %
   2.504 +\isamarkupcmt{\isa{allI}: \isa{{\isacharparenleft}{\isasymAnd}x{\isachardot}\ {\isacharquery}P\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isasymforall}x{\isachardot}\ {\isacharquery}P\ x}%
   2.505 +}
   2.506 +\isanewline
   2.507 +\ \ \isamarkupfalse%
   2.508 +\isacommand{fix}\ a\isanewline
   2.509 +\ \ \isamarkupfalse%
   2.510 +\isacommand{from}\ P\ \isamarkupfalse%
   2.511 +\isacommand{show}\ {\isachardoublequote}P{\isacharparenleft}f\ a{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   2.512 +\isacommand{{\isachardot}{\isachardot}}\ \ %
   2.513 +\isamarkupcmt{\isa{allE}: \isa{{\isasymlbrakk}{\isasymforall}x{\isachardot}\ {\isacharquery}P\ x{\isacharsemicolon}\ {\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isacharquery}R{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}R}%
   2.514 +}
   2.515 +\isanewline
   2.516  \isamarkupfalse%
   2.517 -\isamarkupfalse%
   2.518 -\isamarkupfalse%
   2.519 -\isamarkupfalse%
   2.520 +\isacommand{qed}\isamarkupfalse%
   2.521  %
   2.522  \begin{isamarkuptext}%
   2.523  \noindent Note that in the proof we have chosen to call the bound
   2.524 @@ -514,16 +615,29 @@
   2.525  \isamarkuptrue%
   2.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
   2.527  \isamarkupfalse%
   2.528 -\isamarkupfalse%
   2.529 -\isamarkupfalse%
   2.530 -\isamarkupfalse%
   2.531 -\isamarkupfalse%
   2.532 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.533 +\ \ \isamarkupfalse%
   2.534 +\isacommand{from}\ Pf\ \isamarkupfalse%
   2.535 +\isacommand{show}\ {\isacharquery}thesis\isanewline
   2.536 +\ \ \isamarkupfalse%
   2.537 +\isacommand{proof}\ \ \ \ \ \ \ \ \ \ \ \ \ \ %
   2.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}%
   2.539 +}
   2.540 +\isanewline
   2.541 +\ \ \ \ \isamarkupfalse%
   2.542 +\isacommand{fix}\ x\isanewline
   2.543 +\ \ \ \ \isamarkupfalse%
   2.544 +\isacommand{assume}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\isanewline
   2.545 +\ \ \ \ \isamarkupfalse%
   2.546 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.547 +\isacommand{{\isachardot}{\isachardot}}\ \ %
   2.548 +\isamarkupcmt{\isa{exI}: \isa{{\isacharquery}P\ {\isacharquery}x\ {\isasymLongrightarrow}\ {\isasymexists}x{\isachardot}\ {\isacharquery}P\ x}%
   2.549 +}
   2.550 +\isanewline
   2.551 +\ \ \isamarkupfalse%
   2.552 +\isacommand{qed}\isanewline
   2.553  \isamarkupfalse%
   2.554 -\isamarkupfalse%
   2.555 -\isamarkupfalse%
   2.556 -\isamarkupfalse%
   2.557 -\isamarkupfalse%
   2.558 -\isamarkupfalse%
   2.559 +\isacommand{qed}\isamarkupfalse%
   2.560  %
   2.561  \begin{isamarkuptext}%
   2.562  \noindent Explicit $\exists$-elimination as seen above can become
   2.563 @@ -534,13 +648,16 @@
   2.564  \isamarkuptrue%
   2.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
   2.566  \isamarkupfalse%
   2.567 -\isamarkupfalse%
   2.568 -\isamarkupfalse%
   2.569 -\isamarkupfalse%
   2.570 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.571 +\ \ \isamarkupfalse%
   2.572 +\isacommand{from}\ Pf\ \isamarkupfalse%
   2.573 +\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P{\isacharparenleft}f\ x{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
   2.574 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.575 +\ \ \isamarkupfalse%
   2.576 +\isacommand{thus}\ {\isachardoublequote}{\isasymexists}y{\isachardot}\ P\ y{\isachardoublequote}\ \isamarkupfalse%
   2.577 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.578  \isamarkupfalse%
   2.579 -\isamarkupfalse%
   2.580 -\isamarkupfalse%
   2.581 -\isamarkupfalse%
   2.582 +\isacommand{qed}\isamarkupfalse%
   2.583  %
   2.584  \begin{isamarkuptext}%
   2.585  \noindent Note how the proof text follows the usual mathematical style
   2.586 @@ -555,16 +672,21 @@
   2.587  \isamarkuptrue%
   2.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
   2.589  \isamarkupfalse%
   2.590 -\isamarkupfalse%
   2.591 -\isamarkupfalse%
   2.592 -\isamarkupfalse%
   2.593 -\isamarkupfalse%
   2.594 +\isacommand{proof}\isanewline
   2.595 +\ \ \isamarkupfalse%
   2.596 +\isacommand{fix}\ y\isanewline
   2.597 +\ \ \isamarkupfalse%
   2.598 +\isacommand{from}\ ex\ \isamarkupfalse%
   2.599 +\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   2.600 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.601 +\ \ \isamarkupfalse%
   2.602 +\isacommand{hence}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   2.603 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.604 +\ \ \isamarkupfalse%
   2.605 +\isacommand{thus}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   2.606 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.607  \isamarkupfalse%
   2.608 -\isamarkupfalse%
   2.609 -\isamarkupfalse%
   2.610 -\isamarkupfalse%
   2.611 -\isamarkupfalse%
   2.612 -\isamarkupfalse%
   2.613 +\isacommand{qed}\isamarkupfalse%
   2.614  %
   2.615  \isamarkupsubsection{Making bigger steps%
   2.616  }
   2.617 @@ -579,28 +701,43 @@
   2.618  \isamarkuptrue%
   2.619  \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   2.620  \isamarkupfalse%
   2.621 -\isamarkupfalse%
   2.622 -\isamarkupfalse%
   2.623 -\isamarkupfalse%
   2.624 -\isamarkupfalse%
   2.625 -\isamarkupfalse%
   2.626 -\isamarkupfalse%
   2.627 -\isamarkupfalse%
   2.628 -\isamarkupfalse%
   2.629 -\isamarkupfalse%
   2.630 -\isamarkupfalse%
   2.631 +\isacommand{proof}\isanewline
   2.632 +\ \ \isamarkupfalse%
   2.633 +\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
   2.634 +\ \ \isamarkupfalse%
   2.635 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
   2.636 +\ \ \isamarkupfalse%
   2.637 +\isacommand{proof}\isanewline
   2.638 +\ \ \ \ \isamarkupfalse%
   2.639 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
   2.640 +\ \ \ \ \isamarkupfalse%
   2.641 +\isacommand{then}\ \isamarkupfalse%
   2.642 +\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
   2.643 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.644 +\ \ \ \ \isamarkupfalse%
   2.645 +\isacommand{show}\ False\isanewline
   2.646 +\ \ \ \ \isamarkupfalse%
   2.647 +\isacommand{proof}\ cases\isanewline
   2.648 +\ \ \ \ \ \ \isamarkupfalse%
   2.649 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   2.650 +\ \ \ \ \ \ \isamarkupfalse%
   2.651 +\isacommand{with}\ fy\ \isamarkupfalse%
   2.652 +\isacommand{show}\ False\ \isamarkupfalse%
   2.653 +\isacommand{by}\ blast\isanewline
   2.654 +\ \ \ \ \isamarkupfalse%
   2.655 +\isacommand{next}\isanewline
   2.656 +\ \ \ \ \ \ \isamarkupfalse%
   2.657 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   2.658 +\ \ \ \ \ \ \isamarkupfalse%
   2.659 +\isacommand{with}\ fy\ \isamarkupfalse%
   2.660 +\isacommand{show}\ False\ \isamarkupfalse%
   2.661 +\isacommand{by}\ blast\isanewline
   2.662 +\ \ \ \ \isamarkupfalse%
   2.663 +\isacommand{qed}\isanewline
   2.664 +\ \ \isamarkupfalse%
   2.665 +\isacommand{qed}\isanewline
   2.666  \isamarkupfalse%
   2.667 -\isamarkupfalse%
   2.668 -\isamarkupfalse%
   2.669 -\isamarkupfalse%
   2.670 -\isamarkupfalse%
   2.671 -\isamarkupfalse%
   2.672 -\isamarkupfalse%
   2.673 -\isamarkupfalse%
   2.674 -\isamarkupfalse%
   2.675 -\isamarkupfalse%
   2.676 -\isamarkupfalse%
   2.677 -\isamarkupfalse%
   2.678 +\isacommand{qed}\isamarkupfalse%
   2.679  %
   2.680  \begin{isamarkuptext}%
   2.681  \noindent
   2.682 @@ -624,34 +761,53 @@
   2.683  \isamarkuptrue%
   2.684  \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   2.685  \isamarkupfalse%
   2.686 -\isamarkupfalse%
   2.687 -\isamarkupfalse%
   2.688 -\isamarkupfalse%
   2.689 -\isamarkupfalse%
   2.690 -\isamarkupfalse%
   2.691 -\isamarkupfalse%
   2.692 -\isamarkupfalse%
   2.693 -\isamarkupfalse%
   2.694 -\isamarkupfalse%
   2.695 -\isamarkupfalse%
   2.696 -\isamarkupfalse%
   2.697 -\isamarkupfalse%
   2.698 -\isamarkupfalse%
   2.699 +\isacommand{proof}\isanewline
   2.700 +\ \ \isamarkupfalse%
   2.701 +\isacommand{let}\ {\isacharquery}S\ {\isacharequal}\ {\isachardoublequote}{\isacharbraceleft}x{\isachardot}\ x\ {\isasymnotin}\ f\ x{\isacharbraceright}{\isachardoublequote}\isanewline
   2.702 +\ \ \isamarkupfalse%
   2.703 +\isacommand{show}\ {\isachardoublequote}{\isacharquery}S\ {\isasymnotin}\ range\ f{\isachardoublequote}\isanewline
   2.704 +\ \ \isamarkupfalse%
   2.705 +\isacommand{proof}\isanewline
   2.706 +\ \ \ \ \isamarkupfalse%
   2.707 +\isacommand{assume}\ {\isachardoublequote}{\isacharquery}S\ {\isasymin}\ range\ f{\isachardoublequote}\isanewline
   2.708 +\ \ \ \ \isamarkupfalse%
   2.709 +\isacommand{then}\ \isamarkupfalse%
   2.710 +\isacommand{obtain}\ y\ \isakeyword{where}\ fy{\isacharcolon}\ {\isachardoublequote}{\isacharquery}S\ {\isacharequal}\ f\ y{\isachardoublequote}\ \isamarkupfalse%
   2.711 +\isacommand{{\isachardot}{\isachardot}}\isanewline
   2.712 +\ \ \ \ \isamarkupfalse%
   2.713 +\isacommand{show}\ False\isanewline
   2.714 +\ \ \ \ \isamarkupfalse%
   2.715 +\isacommand{proof}\ cases\isanewline
   2.716 +\ \ \ \ \ \ \isamarkupfalse%
   2.717 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   2.718 +\ \ \ \ \ \ \isamarkupfalse%
   2.719 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
   2.720 +\isacommand{by}\ simp\isanewline
   2.721 +\ \ \ \ \ \ \isamarkupfalse%
   2.722 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
   2.723 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
   2.724 +\ \ \ \ \ \ \isamarkupfalse%
   2.725 +\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
   2.726 +\isacommand{by}\ contradiction\isanewline
   2.727 +\ \ \ \ \isamarkupfalse%
   2.728 +\isacommand{next}\isanewline
   2.729 +\ \ \ \ \ \ \isamarkupfalse%
   2.730 +\isacommand{assume}\ {\isachardoublequote}y\ {\isasymnotin}\ {\isacharquery}S{\isachardoublequote}\isanewline
   2.731 +\ \ \ \ \ \ \isamarkupfalse%
   2.732 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ f\ y{\isachardoublequote}\ \ \ \isamarkupfalse%
   2.733 +\isacommand{by}\ simp\isanewline
   2.734 +\ \ \ \ \ \ \isamarkupfalse%
   2.735 +\isacommand{hence}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharquery}S{\isachardoublequote}\ \ \ \ \isamarkupfalse%
   2.736 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}fy{\isacharparenright}\isanewline
   2.737 +\ \ \ \ \ \ \isamarkupfalse%
   2.738 +\isacommand{thus}\ False\ \ \ \ \ \ \ \ \ \isamarkupfalse%
   2.739 +\isacommand{by}\ contradiction\isanewline
   2.740 +\ \ \ \ \isamarkupfalse%
   2.741 +\isacommand{qed}\isanewline
   2.742 +\ \ \isamarkupfalse%
   2.743 +\isacommand{qed}\isanewline
   2.744  \isamarkupfalse%
   2.745 -\isamarkupfalse%
   2.746 -\isamarkupfalse%
   2.747 -\isamarkupfalse%
   2.748 -\isamarkupfalse%
   2.749 -\isamarkupfalse%
   2.750 -\isamarkupfalse%
   2.751 -\isamarkupfalse%
   2.752 -\isamarkupfalse%
   2.753 -\isamarkupfalse%
   2.754 -\isamarkupfalse%
   2.755 -\isamarkupfalse%
   2.756 -\isamarkupfalse%
   2.757 -\isamarkupfalse%
   2.758 -\isamarkupfalse%
   2.759 +\isacommand{qed}\isamarkupfalse%
   2.760  %
   2.761  \begin{isamarkuptext}%
   2.762  \noindent Method \isa{contradiction} succeeds if both $P$ and
   2.763 @@ -664,7 +820,7 @@
   2.764  \isamarkuptrue%
   2.765  \isacommand{theorem}\ {\isachardoublequote}{\isasymexists}S{\isachardot}\ S\ {\isasymnotin}\ range\ {\isacharparenleft}f\ {\isacharcolon}{\isacharcolon}\ {\isacharprime}a\ {\isasymRightarrow}\ {\isacharprime}a\ set{\isacharparenright}{\isachardoublequote}\isanewline
   2.766  \isamarkupfalse%
   2.767 -\isamarkupfalse%
   2.768 +\isacommand{by}\ best\isamarkupfalse%
   2.769  %
   2.770  \isamarkupsubsection{Raw proof blocks%
   2.771  }
   2.772 @@ -680,19 +836,28 @@
   2.773  \isamarkupfalse%
   2.774  \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   2.775  \isamarkupfalse%
   2.776 -\isamarkupfalse%
   2.777 -\isamarkupfalse%
   2.778 -\isamarkupfalse%
   2.779 -\isamarkupfalse%
   2.780 -\isamarkupfalse%
   2.781 -\isamarkupfalse%
   2.782 +\isacommand{proof}\isanewline
   2.783 +\ \ \isamarkupfalse%
   2.784 +\isacommand{fix}\ x\ \isamarkupfalse%
   2.785 +\isacommand{show}\ {\isachardoublequote}{\isasymforall}y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   2.786 +\ \ \isamarkupfalse%
   2.787 +\isacommand{proof}\isanewline
   2.788 +\ \ \ \ \isamarkupfalse%
   2.789 +\isacommand{fix}\ y\ \isamarkupfalse%
   2.790 +\isacommand{show}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   2.791 +\ \ \ \ \isamarkupfalse%
   2.792 +\isacommand{proof}\isanewline
   2.793 +\ \ \ \ \ \ \isamarkupfalse%
   2.794 +\isacommand{assume}\ {\isachardoublequote}A\ x\ y\ {\isasymand}\ B\ x\ y{\isachardoublequote}\isanewline
   2.795 +\ \ \ \ \ \ \isamarkupfalse%
   2.796 +\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   2.797 +\isacommand{sorry}\isanewline
   2.798 +\ \ \ \ \isamarkupfalse%
   2.799 +\isacommand{qed}\isanewline
   2.800 +\ \ \isamarkupfalse%
   2.801 +\isacommand{qed}\isanewline
   2.802  \isamarkupfalse%
   2.803 -\isamarkupfalse%
   2.804 -\isamarkupfalse%
   2.805 -\isamarkupfalse%
   2.806 -\isamarkupfalse%
   2.807 -\isamarkupfalse%
   2.808 -\isamarkupfalse%
   2.809 +\isacommand{qed}\isamarkupfalse%
   2.810  %
   2.811  \begin{isamarkuptext}%
   2.812  \noindent Since we are only interested in the decomposition and not the
   2.813 @@ -706,17 +871,24 @@
   2.814  \isamarkuptrue%
   2.815  \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   2.816  \isamarkupfalse%
   2.817 -\isamarkupfalse%
   2.818 -\isamarkupfalse%
   2.819 -\isamarkupfalse%
   2.820 -\isamarkupfalse%
   2.821 -\isamarkupfalse%
   2.822 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.823 +\ \ \isamarkupfalse%
   2.824 +\isacommand{have}\ {\isachardoublequote}{\isasymAnd}x\ y{\isachardot}\ {\isasymlbrakk}\ A\ x\ y{\isacharsemicolon}\ B\ x\ y\ {\isasymrbrakk}\ {\isasymLongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   2.825 +\ \ \isamarkupfalse%
   2.826 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.827 +\ \ \ \ \isamarkupfalse%
   2.828 +\isacommand{fix}\ x\ y\ \isamarkupfalse%
   2.829 +\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
   2.830 +\ \ \ \ \isamarkupfalse%
   2.831 +\isacommand{show}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   2.832 +\isacommand{sorry}\isanewline
   2.833 +\ \ \isamarkupfalse%
   2.834 +\isacommand{qed}\isanewline
   2.835 +\ \ \isamarkupfalse%
   2.836 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.837 +\isacommand{by}\ blast\isanewline
   2.838  \isamarkupfalse%
   2.839 -\isamarkupfalse%
   2.840 -\isamarkupfalse%
   2.841 -\isamarkupfalse%
   2.842 -\isamarkupfalse%
   2.843 -\isamarkupfalse%
   2.844 +\isacommand{qed}\isamarkupfalse%
   2.845  %
   2.846  \begin{isamarkuptext}%
   2.847  \noindent
   2.848 @@ -726,16 +898,20 @@
   2.849  \isamarkuptrue%
   2.850  \isacommand{lemma}\ {\isachardoublequote}{\isasymforall}x\ y{\isachardot}\ A\ x\ y\ {\isasymand}\ B\ x\ y\ {\isasymlongrightarrow}\ C\ x\ y{\isachardoublequote}\isanewline
   2.851  \isamarkupfalse%
   2.852 -\isamarkupfalse%
   2.853 -\isamarkupfalse%
   2.854 -\isamarkupfalse%
   2.855 -\isamarkupfalse%
   2.856 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.857 +\ \ \isamarkupfalse%
   2.858 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   2.859 +\isacommand{fix}\ x\ y\ \isamarkupfalse%
   2.860 +\isacommand{assume}\ {\isachardoublequote}A\ x\ y{\isachardoublequote}\ {\isachardoublequote}B\ x\ y{\isachardoublequote}\isanewline
   2.861 +\ \ \ \ \isamarkupfalse%
   2.862 +\isacommand{have}\ {\isachardoublequote}C\ x\ y{\isachardoublequote}\ \isamarkupfalse%
   2.863 +\isacommand{sorry}\ \isamarkupfalse%
   2.864 +\isacommand{{\isacharbraceright}}\isanewline
   2.865 +\ \ \isamarkupfalse%
   2.866 +\isacommand{thus}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.867 +\isacommand{by}\ blast\isanewline
   2.868  \isamarkupfalse%
   2.869 -\isamarkupfalse%
   2.870 -\isamarkupfalse%
   2.871 -\isamarkupfalse%
   2.872 -\isamarkupfalse%
   2.873 -\isamarkupfalse%
   2.874 +\isacommand{qed}\isamarkupfalse%
   2.875  %
   2.876  \begin{isamarkuptext}%
   2.877  \noindent The result of the raw proof block is the same theorem
   2.878 @@ -771,31 +947,67 @@
   2.879  %
   2.880  \renewcommand{\isamarkupcmt}[1]{#1}
   2.881  \isamarkupfalse%
   2.882 -\isamarkupfalse%
   2.883 -\isamarkupfalse%
   2.884 -\isamarkupfalse%
   2.885 -\isamarkupfalse%
   2.886 -\isamarkupfalse%
   2.887 -\isamarkupfalse%
   2.888 -\isamarkupfalse%
   2.889 -\isamarkupfalse%
   2.890 -\isamarkupfalse%
   2.891 -\isamarkupfalse%
   2.892 -\isamarkupfalse%
   2.893 -\isamarkupfalse%
   2.894 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.895 +\ \ \isamarkupfalse%
   2.896 +\isacommand{have}\ {\isachardoublequote}P\isactrlisub {\isadigit{1}}\ {\isasymor}\ P\isactrlisub {\isadigit{2}}\ {\isasymor}\ P\isactrlisub {\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
   2.897 +\ %
   2.898 +\isamarkupcmt{\dots%
   2.899 +}
   2.900 +\isanewline
   2.901 +\ \ \isamarkupfalse%
   2.902 +\isacommand{moreover}\isanewline
   2.903 +\ \ \isamarkupfalse%
   2.904 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   2.905 +\isacommand{assume}\ P\isactrlisub {\isadigit{1}}\isanewline
   2.906 +\ \ \ \ %
   2.907 +\isamarkupcmt{\dots%
   2.908 +}
   2.909 +\isanewline
   2.910 +\ \ \ \ \isamarkupfalse%
   2.911 +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.912 +\ %
   2.913 +\isamarkupcmt{\dots%
   2.914 +}
   2.915 +\ \isamarkupfalse%
   2.916 +\isacommand{{\isacharbraceright}}\isanewline
   2.917 +\ \ \isamarkupfalse%
   2.918 +\isacommand{moreover}\isanewline
   2.919 +\ \ \isamarkupfalse%
   2.920 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   2.921 +\isacommand{assume}\ P\isactrlisub {\isadigit{2}}\isanewline
   2.922 +\ \ \ \ %
   2.923 +\isamarkupcmt{\dots%
   2.924 +}
   2.925 +\isanewline
   2.926 +\ \ \ \ \isamarkupfalse%
   2.927 +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.928 +\ %
   2.929 +\isamarkupcmt{\dots%
   2.930 +}
   2.931 +\ \isamarkupfalse%
   2.932 +\isacommand{{\isacharbraceright}}\isanewline
   2.933 +\ \ \isamarkupfalse%
   2.934 +\isacommand{moreover}\isanewline
   2.935 +\ \ \isamarkupfalse%
   2.936 +\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
   2.937 +\isacommand{assume}\ P\isactrlisub {\isadigit{3}}\isanewline
   2.938 +\ \ \ \ %
   2.939 +\isamarkupcmt{\dots%
   2.940 +}
   2.941 +\isanewline
   2.942 +\ \ \ \ \isamarkupfalse%
   2.943 +\isacommand{have}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.944 +\ %
   2.945 +\isamarkupcmt{\dots%
   2.946 +}
   2.947 +\ \isamarkupfalse%
   2.948 +\isacommand{{\isacharbraceright}}\isanewline
   2.949 +\ \ \isamarkupfalse%
   2.950 +\isacommand{ultimately}\ \isamarkupfalse%
   2.951 +\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
   2.952 +\isacommand{by}\ blast\isanewline
   2.953  \isamarkupfalse%
   2.954 -\isamarkupfalse%
   2.955 -\isamarkupfalse%
   2.956 -\isamarkupfalse%
   2.957 -\isamarkupfalse%
   2.958 -\isamarkupfalse%
   2.959 -\isamarkupfalse%
   2.960 -\isamarkupfalse%
   2.961 -\isamarkupfalse%
   2.962 -\isamarkupfalse%
   2.963 -\isamarkupfalse%
   2.964 -\isamarkupfalse%
   2.965 -\isamarkupfalse%
   2.966 +\isacommand{qed}\isamarkupfalse%
   2.967  %
   2.968  \renewcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   2.969  %
   2.970 @@ -878,7 +1090,7 @@
   2.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
   2.972  \ \ \isakeyword{shows}\ {\isachardoublequote}x\ {\isachargreater}\ y\ {\isasymLongrightarrow}\ z\ {\isacharplus}{\isacharplus}\ x\ {\isachargreater}\ z\ {\isacharplus}{\isacharplus}\ y{\isachardoublequote}\isanewline
   2.973  \isamarkupfalse%
   2.974 -\isamarkupfalse%
   2.975 +\isacommand{by}{\isacharparenleft}simp\ add{\isacharcolon}\ comm\ mono{\isacharparenright}\isamarkupfalse%
   2.976  %
   2.977  \begin{isamarkuptext}%
   2.978  \noindent The concrete syntax is dropped at the end of the proof and the
   2.979 @@ -902,10 +1114,11 @@
   2.980  \isamarkuptrue%
   2.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
   2.982  \isamarkupfalse%
   2.983 -\isamarkupfalse%
   2.984 -\isamarkupfalse%
   2.985 -\isamarkupfalse%
   2.986 -\isamarkupfalse%
   2.987 +\isacommand{proof}\ {\isacharminus}\isanewline
   2.988 +\ \ \isamarkupfalse%
   2.989 +\isacommand{from}\ A\ \isamarkupfalse%
   2.990 +\isacommand{obtain}\ x\ y\ \isakeyword{where}\ P{\isacharcolon}\ {\isachardoublequote}P\ x\ y{\isachardoublequote}\ \isakeyword{and}\ Q{\isacharcolon}\ {\isachardoublequote}Q\ x\ y{\isachardoublequote}\ \ \isamarkupfalse%
   2.991 +\isacommand{by}\ blast\isamarkupfalse%
   2.992  \isamarkupfalse%
   2.993  %
   2.994  \begin{isamarkuptext}%
   2.995 @@ -926,15 +1139,23 @@
   2.996  \isamarkuptrue%
   2.997  \isacommand{lemma}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ {\isacharparenleft}A\ {\isasymlongrightarrow}\ B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
   2.998  \isamarkupfalse%
   2.999 -\isamarkupfalse%
  2.1000 -\isamarkupfalse%
  2.1001 -\isamarkupfalse%
  2.1002 -\isamarkupfalse%
  2.1003 +\isacommand{proof}\isanewline
  2.1004 +\ \ \isamarkupfalse%
  2.1005 +\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}A{\isachardoublequote}\isanewline
  2.1006 +\ \ \isamarkupfalse%
  2.1007 +\isacommand{show}\ {\isachardoublequote}{\isacharparenleft}A\ {\isasymlongrightarrow}B{\isacharparenright}\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
  2.1008 +\ \ \ \ \isamarkupfalse%
  2.1009 +\isacommand{apply}{\isacharparenleft}rule\ impI{\isacharparenright}\isanewline
  2.1010 +\ \ \ \ \isamarkupfalse%
  2.1011 +\isacommand{apply}{\isacharparenleft}erule\ impE{\isacharparenright}\isanewline
  2.1012 +\ \ \ \ \isamarkupfalse%
  2.1013 +\isacommand{apply}{\isacharparenleft}rule\ a{\isacharparenright}\isanewline
  2.1014 +\ \ \ \ \isamarkupfalse%
  2.1015 +\isacommand{apply}\ assumption\isanewline
  2.1016 +\ \ \ \ \isamarkupfalse%
  2.1017 +\isacommand{done}\isanewline
  2.1018  \isamarkupfalse%
  2.1019 -\isamarkupfalse%
  2.1020 -\isamarkupfalse%
  2.1021 -\isamarkupfalse%
  2.1022 -\isamarkupfalse%
  2.1023 +\isacommand{qed}\isamarkupfalse%
  2.1024  %
  2.1025  \begin{isamarkuptext}%
  2.1026  \noindent You may need to resort to this technique if an