| author | wenzelm |
| Wed, 01 Jun 2011 12:20:48 +0200 | |
| changeset 44122 | 36daee4cc9c9 |
| parent 44121 | ba23e83b0868 |
| child 44123 | 6e83c2f73240 |
| permissions | -rw-r--r-- |
| wenzelm@44121 | 1 |
% |
| wenzelm@44121 | 2 |
\begin{isabellebody}%
|
| wenzelm@44121 | 3 |
\def\isabellecontext{Synopsis}%
|
| wenzelm@44121 | 4 |
% |
| wenzelm@44121 | 5 |
\isadelimtheory |
| wenzelm@44121 | 6 |
% |
| wenzelm@44121 | 7 |
\endisadelimtheory |
| wenzelm@44121 | 8 |
% |
| wenzelm@44121 | 9 |
\isatagtheory |
| wenzelm@44121 | 10 |
\isacommand{theory}\isamarkupfalse%
|
| wenzelm@44121 | 11 |
\ Synopsis\isanewline |
| wenzelm@44121 | 12 |
\isakeyword{imports}\ Base\ Main\isanewline
|
| wenzelm@44121 | 13 |
\isakeyword{begin}%
|
| wenzelm@44121 | 14 |
\endisatagtheory |
| wenzelm@44121 | 15 |
{\isafoldtheory}%
|
| wenzelm@44121 | 16 |
% |
| wenzelm@44121 | 17 |
\isadelimtheory |
| wenzelm@44121 | 18 |
% |
| wenzelm@44121 | 19 |
\endisadelimtheory |
| wenzelm@44121 | 20 |
% |
| wenzelm@44121 | 21 |
\isamarkupchapter{Synopsis%
|
| wenzelm@44121 | 22 |
} |
| wenzelm@44121 | 23 |
\isamarkuptrue% |
| wenzelm@44121 | 24 |
% |
| wenzelm@44121 | 25 |
\isamarkupsection{Notepad%
|
| wenzelm@44121 | 26 |
} |
| wenzelm@44121 | 27 |
\isamarkuptrue% |
| wenzelm@44121 | 28 |
% |
| wenzelm@44121 | 29 |
\begin{isamarkuptext}%
|
| wenzelm@44121 | 30 |
An Isar proof body serves as mathematical notepad to compose logical |
| wenzelm@44122 | 31 |
content, consisting of types, terms, facts.% |
| wenzelm@44121 | 32 |
\end{isamarkuptext}%
|
| wenzelm@44121 | 33 |
\isamarkuptrue% |
| wenzelm@44121 | 34 |
% |
| wenzelm@44122 | 35 |
\isamarkupsubsection{Types and terms%
|
| wenzelm@44122 | 36 |
} |
| wenzelm@44122 | 37 |
\isamarkuptrue% |
| wenzelm@44122 | 38 |
\isacommand{notepad}\isamarkupfalse%
|
| wenzelm@44122 | 39 |
\isanewline |
| wenzelm@44122 | 40 |
\isakeyword{begin}%
|
| wenzelm@44122 | 41 |
\isadelimproof |
| wenzelm@44122 | 42 |
% |
| wenzelm@44122 | 43 |
\endisadelimproof |
| wenzelm@44122 | 44 |
% |
| wenzelm@44122 | 45 |
\isatagproof |
| wenzelm@44122 | 46 |
% |
| wenzelm@44122 | 47 |
\begin{isamarkuptxt}%
|
| wenzelm@44122 | 48 |
Locally fixed entities:% |
| wenzelm@44122 | 49 |
\end{isamarkuptxt}%
|
| wenzelm@44122 | 50 |
\isamarkuptrue% |
| wenzelm@44122 | 51 |
\ \ \isacommand{fix}\isamarkupfalse%
|
| wenzelm@44122 | 52 |
\ x\ \ \ % |
| wenzelm@44122 | 53 |
\isamarkupcmt{local constant, without any type information yet%
|
| wenzelm@44122 | 54 |
} |
| wenzelm@44122 | 55 |
\isanewline |
| wenzelm@44122 | 56 |
\ \ \isacommand{fix}\isamarkupfalse%
|
| wenzelm@44122 | 57 |
\ x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{27}{\isacharprime}}a\ \ %
|
| wenzelm@44122 | 58 |
\isamarkupcmt{variant with explicit type-constraint for subsequent use%
|
| wenzelm@44122 | 59 |
} |
| wenzelm@44122 | 60 |
\isanewline |
| wenzelm@44122 | 61 |
\isanewline |
| wenzelm@44122 | 62 |
\ \ \isacommand{fix}\isamarkupfalse%
|
| wenzelm@44122 | 63 |
\ a\ b\isanewline |
| wenzelm@44122 | 64 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44122 | 65 |
\ {\isaliteral{22}{\isachardoublequoteopen}}a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{22}{\isachardoublequoteclose}}\ \ %
|
| wenzelm@44122 | 66 |
\isamarkupcmt{type assignment at first occurrence in concrete term%
|
| wenzelm@44122 | 67 |
} |
| wenzelm@44122 | 68 |
% |
| wenzelm@44122 | 69 |
\begin{isamarkuptxt}%
|
| wenzelm@44122 | 70 |
Definitions (non-polymorphic):% |
| wenzelm@44122 | 71 |
\end{isamarkuptxt}%
|
| wenzelm@44122 | 72 |
\isamarkuptrue% |
| wenzelm@44122 | 73 |
\ \ \isacommand{def}\isamarkupfalse%
|
| wenzelm@44122 | 74 |
\ x\ {\isaliteral{5C3C65717569763E}{\isasymequiv}}\ {\isaliteral{22}{\isachardoublequoteopen}}t{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{22}{\isachardoublequoteclose}}%
|
| wenzelm@44122 | 75 |
\begin{isamarkuptxt}%
|
| wenzelm@44122 | 76 |
Abbreviations (polymorphic):% |
| wenzelm@44122 | 77 |
\end{isamarkuptxt}%
|
| wenzelm@44122 | 78 |
\isamarkuptrue% |
| wenzelm@44122 | 79 |
\ \ \isacommand{let}\isamarkupfalse%
|
| wenzelm@44122 | 80 |
\ {\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ x{\isaliteral{22}{\isachardoublequoteclose}}%
|
| wenzelm@44122 | 81 |
\endisatagproof |
| wenzelm@44122 | 82 |
{\isafoldproof}%
|
| wenzelm@44122 | 83 |
% |
| wenzelm@44122 | 84 |
\isadelimproof |
| wenzelm@44122 | 85 |
% |
| wenzelm@44122 | 86 |
\endisadelimproof |
| wenzelm@44122 | 87 |
\isanewline |
| wenzelm@44122 | 88 |
\ \ \isacommand{term}\isamarkupfalse%
|
| wenzelm@44122 | 89 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{3F}{\isacharquery}}f\ {\isaliteral{3F}{\isacharquery}}f{\isaliteral{22}{\isachardoublequoteclose}}%
|
| wenzelm@44122 | 90 |
\isadelimproof |
| wenzelm@44122 | 91 |
% |
| wenzelm@44122 | 92 |
\endisadelimproof |
| wenzelm@44122 | 93 |
% |
| wenzelm@44122 | 94 |
\isatagproof |
| wenzelm@44122 | 95 |
% |
| wenzelm@44122 | 96 |
\begin{isamarkuptxt}%
|
| wenzelm@44122 | 97 |
Notation:% |
| wenzelm@44122 | 98 |
\end{isamarkuptxt}%
|
| wenzelm@44122 | 99 |
\isamarkuptrue% |
| wenzelm@44122 | 100 |
\ \ \isacommand{write}\isamarkupfalse%
|
| wenzelm@44122 | 101 |
\ x\ \ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{29}{\isacharparenright}}%
|
| wenzelm@44122 | 102 |
\endisatagproof |
| wenzelm@44122 | 103 |
{\isafoldproof}%
|
| wenzelm@44122 | 104 |
% |
| wenzelm@44122 | 105 |
\isadelimproof |
| wenzelm@44122 | 106 |
% |
| wenzelm@44122 | 107 |
\endisadelimproof |
| wenzelm@44122 | 108 |
\isanewline |
| wenzelm@44122 | 109 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44122 | 110 |
% |
| wenzelm@44121 | 111 |
\isamarkupsubsection{Facts%
|
| wenzelm@44121 | 112 |
} |
| wenzelm@44121 | 113 |
\isamarkuptrue% |
| wenzelm@44121 | 114 |
% |
| wenzelm@44121 | 115 |
\begin{isamarkuptext}%
|
| wenzelm@44121 | 116 |
A fact is a simultaneous list of theorems.% |
| wenzelm@44121 | 117 |
\end{isamarkuptext}%
|
| wenzelm@44121 | 118 |
\isamarkuptrue% |
| wenzelm@44121 | 119 |
% |
| wenzelm@44121 | 120 |
\isamarkupsubsubsection{Producing facts%
|
| wenzelm@44121 | 121 |
} |
| wenzelm@44121 | 122 |
\isamarkuptrue% |
| wenzelm@44121 | 123 |
\isacommand{notepad}\isamarkupfalse%
|
| wenzelm@44121 | 124 |
\isanewline |
| wenzelm@44121 | 125 |
\isakeyword{begin}%
|
| wenzelm@44121 | 126 |
\isadelimproof |
| wenzelm@44121 | 127 |
% |
| wenzelm@44121 | 128 |
\endisadelimproof |
| wenzelm@44121 | 129 |
% |
| wenzelm@44121 | 130 |
\isatagproof |
| wenzelm@44121 | 131 |
% |
| wenzelm@44121 | 132 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 133 |
Via assumption (``lambda''):% |
| wenzelm@44121 | 134 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 135 |
\isamarkuptrue% |
| wenzelm@44121 | 136 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 137 |
\ a{\isaliteral{3A}{\isacharcolon}}\ A%
|
| wenzelm@44121 | 138 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 139 |
Via proof (``let''):% |
| wenzelm@44121 | 140 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 141 |
\isamarkuptrue% |
| wenzelm@44121 | 142 |
\ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 143 |
\ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 144 |
% |
| wenzelm@44121 | 145 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 146 |
Via abbreviation (``let''):% |
| wenzelm@44121 | 147 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 148 |
\isamarkuptrue% |
| wenzelm@44121 | 149 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 150 |
\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ b%
|
| wenzelm@44121 | 151 |
\endisatagproof |
| wenzelm@44121 | 152 |
{\isafoldproof}%
|
| wenzelm@44121 | 153 |
% |
| wenzelm@44121 | 154 |
\isadelimproof |
| wenzelm@44121 | 155 |
% |
| wenzelm@44121 | 156 |
\endisadelimproof |
| wenzelm@44121 | 157 |
\isanewline |
| wenzelm@44121 | 158 |
\isanewline |
| wenzelm@44121 | 159 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44121 | 160 |
% |
| wenzelm@44121 | 161 |
\isamarkupsubsubsection{Referencing facts%
|
| wenzelm@44121 | 162 |
} |
| wenzelm@44121 | 163 |
\isamarkuptrue% |
| wenzelm@44121 | 164 |
\isacommand{notepad}\isamarkupfalse%
|
| wenzelm@44121 | 165 |
\isanewline |
| wenzelm@44121 | 166 |
\isakeyword{begin}%
|
| wenzelm@44121 | 167 |
\isadelimproof |
| wenzelm@44121 | 168 |
% |
| wenzelm@44121 | 169 |
\endisadelimproof |
| wenzelm@44121 | 170 |
% |
| wenzelm@44121 | 171 |
\isatagproof |
| wenzelm@44121 | 172 |
% |
| wenzelm@44121 | 173 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 174 |
Via explicit name:% |
| wenzelm@44121 | 175 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 176 |
\isamarkuptrue% |
| wenzelm@44121 | 177 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 178 |
\ a{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
|
| wenzelm@44121 | 179 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 180 |
\ a% |
| wenzelm@44121 | 181 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 182 |
Via implicit name:% |
| wenzelm@44121 | 183 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 184 |
\isamarkuptrue% |
| wenzelm@44121 | 185 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 186 |
\ A\isanewline |
| wenzelm@44121 | 187 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 188 |
\ this% |
| wenzelm@44121 | 189 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 190 |
Via literal proposition (unification with results from the proof text):% |
| wenzelm@44121 | 191 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 192 |
\isamarkuptrue% |
| wenzelm@44121 | 193 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 194 |
\ A\isanewline |
| wenzelm@44121 | 195 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 196 |
\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
|
| wenzelm@44121 | 197 |
\isanewline |
| wenzelm@44121 | 198 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 199 |
\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
| wenzelm@44121 | 200 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 201 |
\ {\isaliteral{60}{\isacharbackquoteopen}}B\ a{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
|
| wenzelm@44121 | 202 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 203 |
\ {\isaliteral{60}{\isacharbackquoteopen}}B\ b{\isaliteral{60}{\isacharbackquoteclose}}%
|
| wenzelm@44121 | 204 |
\endisatagproof |
| wenzelm@44121 | 205 |
{\isafoldproof}%
|
| wenzelm@44121 | 206 |
% |
| wenzelm@44121 | 207 |
\isadelimproof |
| wenzelm@44121 | 208 |
% |
| wenzelm@44121 | 209 |
\endisadelimproof |
| wenzelm@44121 | 210 |
\isanewline |
| wenzelm@44121 | 211 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44121 | 212 |
% |
| wenzelm@44121 | 213 |
\isamarkupsubsubsection{Manipulating facts%
|
| wenzelm@44121 | 214 |
} |
| wenzelm@44121 | 215 |
\isamarkuptrue% |
| wenzelm@44121 | 216 |
\isacommand{notepad}\isamarkupfalse%
|
| wenzelm@44121 | 217 |
\isanewline |
| wenzelm@44121 | 218 |
\isakeyword{begin}%
|
| wenzelm@44121 | 219 |
\isadelimproof |
| wenzelm@44121 | 220 |
% |
| wenzelm@44121 | 221 |
\endisadelimproof |
| wenzelm@44121 | 222 |
% |
| wenzelm@44121 | 223 |
\isatagproof |
| wenzelm@44121 | 224 |
% |
| wenzelm@44121 | 225 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 226 |
Instantiation:% |
| wenzelm@44121 | 227 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 228 |
\isamarkuptrue% |
| wenzelm@44121 | 229 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 230 |
\ a{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{5C3C416E643E}{\isasymAnd}}x{\isaliteral{2E}{\isachardot}}\ B\ x{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
| wenzelm@44121 | 231 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 232 |
\ a\isanewline |
| wenzelm@44121 | 233 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 234 |
\ a\ {\isaliteral{5B}{\isacharbrackleft}}of\ b{\isaliteral{5D}{\isacharbrackright}}\isanewline
|
| wenzelm@44121 | 235 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 236 |
\ a\ {\isaliteral{5B}{\isacharbrackleft}}\isakeyword{where}\ x\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{5D}{\isacharbrackright}}%
|
| wenzelm@44121 | 237 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 238 |
Backchaining:% |
| wenzelm@44121 | 239 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 240 |
\isamarkuptrue% |
| wenzelm@44121 | 241 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 242 |
\ {\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}\ A\isanewline
|
| wenzelm@44121 | 243 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 244 |
\ {\isadigit{2}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}A\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ C{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
| wenzelm@44121 | 245 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 246 |
\ {\isadigit{2}}\ {\isaliteral{5B}{\isacharbrackleft}}OF\ {\isadigit{1}}{\isaliteral{5D}{\isacharbrackright}}\isanewline
|
| wenzelm@44121 | 247 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 248 |
\ {\isadigit{1}}\ {\isaliteral{5B}{\isacharbrackleft}}THEN\ {\isadigit{2}}{\isaliteral{5D}{\isacharbrackright}}%
|
| wenzelm@44121 | 249 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 250 |
Symmetric results:% |
| wenzelm@44121 | 251 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 252 |
\isamarkuptrue% |
| wenzelm@44121 | 253 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 254 |
\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{3D}{\isacharequal}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
| wenzelm@44121 | 255 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 256 |
\ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}\isanewline
|
| wenzelm@44121 | 257 |
\isanewline |
| wenzelm@44121 | 258 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 259 |
\ {\isaliteral{22}{\isachardoublequoteopen}}x\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ y{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
| wenzelm@44121 | 260 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 261 |
\ this\ {\isaliteral{5B}{\isacharbrackleft}}symmetric{\isaliteral{5D}{\isacharbrackright}}%
|
| wenzelm@44121 | 262 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 263 |
Adhoc-simplication (take care!):% |
| wenzelm@44121 | 264 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 265 |
\isamarkuptrue% |
| wenzelm@44121 | 266 |
\ \ \isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 267 |
\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{40}{\isacharat}}\ xs{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
|
| wenzelm@44121 | 268 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 269 |
\ this\ {\isaliteral{5B}{\isacharbrackleft}}simplified{\isaliteral{5D}{\isacharbrackright}}%
|
| wenzelm@44121 | 270 |
\endisatagproof |
| wenzelm@44121 | 271 |
{\isafoldproof}%
|
| wenzelm@44121 | 272 |
% |
| wenzelm@44121 | 273 |
\isadelimproof |
| wenzelm@44121 | 274 |
% |
| wenzelm@44121 | 275 |
\endisadelimproof |
| wenzelm@44121 | 276 |
\isanewline |
| wenzelm@44121 | 277 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44121 | 278 |
% |
| wenzelm@44121 | 279 |
\isamarkupsubsubsection{Projections%
|
| wenzelm@44121 | 280 |
} |
| wenzelm@44121 | 281 |
\isamarkuptrue% |
| wenzelm@44121 | 282 |
% |
| wenzelm@44121 | 283 |
\begin{isamarkuptext}%
|
| wenzelm@44121 | 284 |
Isar facts consist of multiple theorems. There is notation to project |
| wenzelm@44121 | 285 |
interval ranges.% |
| wenzelm@44121 | 286 |
\end{isamarkuptext}%
|
| wenzelm@44121 | 287 |
\isamarkuptrue% |
| wenzelm@44121 | 288 |
\isacommand{notepad}\isamarkupfalse%
|
| wenzelm@44121 | 289 |
\isanewline |
| wenzelm@44121 | 290 |
\isakeyword{begin}\isanewline
|
| wenzelm@44121 | 291 |
% |
| wenzelm@44121 | 292 |
\isadelimproof |
| wenzelm@44121 | 293 |
\ \ % |
| wenzelm@44121 | 294 |
\endisadelimproof |
| wenzelm@44121 | 295 |
% |
| wenzelm@44121 | 296 |
\isatagproof |
| wenzelm@44121 | 297 |
\isacommand{assume}\isamarkupfalse%
|
| wenzelm@44121 | 298 |
\ stuff{\isaliteral{3A}{\isacharcolon}}\ A\ B\ C\ D\isanewline
|
| wenzelm@44121 | 299 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 300 |
\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
| wenzelm@44121 | 301 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 302 |
\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isadigit{3}}{\isaliteral{29}{\isacharparenright}}\isanewline
|
| wenzelm@44121 | 303 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 304 |
\ stuff{\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{29}{\isacharparenright}}%
|
| wenzelm@44121 | 305 |
\endisatagproof |
| wenzelm@44121 | 306 |
{\isafoldproof}%
|
| wenzelm@44121 | 307 |
% |
| wenzelm@44121 | 308 |
\isadelimproof |
| wenzelm@44121 | 309 |
\isanewline |
| wenzelm@44121 | 310 |
% |
| wenzelm@44121 | 311 |
\endisadelimproof |
| wenzelm@44121 | 312 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44121 | 313 |
% |
| wenzelm@44121 | 314 |
\isamarkupsubsubsection{Naming conventions%
|
| wenzelm@44121 | 315 |
} |
| wenzelm@44121 | 316 |
\isamarkuptrue% |
| wenzelm@44121 | 317 |
% |
| wenzelm@44121 | 318 |
\begin{isamarkuptext}%
|
| wenzelm@44121 | 319 |
\begin{itemize}
|
| wenzelm@44121 | 320 |
|
| wenzelm@44121 | 321 |
\item Lower-case identifiers are usually preferred. |
| wenzelm@44121 | 322 |
|
| wenzelm@44121 | 323 |
\item Facts can be named after the main term within the proposition. |
| wenzelm@44121 | 324 |
|
| wenzelm@44121 | 325 |
\item Facts should \emph{not} be named after the command that
|
| wenzelm@44121 | 326 |
introduced them (\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}, \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}). This is
|
| wenzelm@44121 | 327 |
misleading and hard to maintain. |
| wenzelm@44121 | 328 |
|
| wenzelm@44121 | 329 |
\item Natural numbers can be used as ``meaningless'' names (more |
| wenzelm@44121 | 330 |
appropriate than \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{1}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isadigit{2}}{\isaliteral{22}{\isachardoublequote}}} etc.)
|
| wenzelm@44121 | 331 |
|
| wenzelm@44121 | 332 |
\item Symbolic identifiers are supported (e.g. \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{2A}{\isacharasterisk}}{\isaliteral{22}{\isachardoublequote}}}).
|
| wenzelm@44121 | 333 |
|
| wenzelm@44121 | 334 |
\end{itemize}%
|
| wenzelm@44121 | 335 |
\end{isamarkuptext}%
|
| wenzelm@44121 | 336 |
\isamarkuptrue% |
| wenzelm@44121 | 337 |
% |
| wenzelm@44121 | 338 |
\isamarkupsubsection{Block structure%
|
| wenzelm@44121 | 339 |
} |
| wenzelm@44121 | 340 |
\isamarkuptrue% |
| wenzelm@44121 | 341 |
% |
| wenzelm@44121 | 342 |
\begin{isamarkuptext}%
|
| wenzelm@44121 | 343 |
The formal notepad is block structured. The fact produced by the last |
| wenzelm@44121 | 344 |
entry of a block is exported into the outer context.% |
| wenzelm@44121 | 345 |
\end{isamarkuptext}%
|
| wenzelm@44121 | 346 |
\isamarkuptrue% |
| wenzelm@44121 | 347 |
\isacommand{notepad}\isamarkupfalse%
|
| wenzelm@44121 | 348 |
\isanewline |
| wenzelm@44121 | 349 |
\isakeyword{begin}\isanewline
|
| wenzelm@44121 | 350 |
% |
| wenzelm@44121 | 351 |
\isadelimproof |
| wenzelm@44121 | 352 |
\ \ % |
| wenzelm@44121 | 353 |
\endisadelimproof |
| wenzelm@44121 | 354 |
% |
| wenzelm@44121 | 355 |
\isatagproof |
| wenzelm@44121 | 356 |
\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 357 |
\isanewline |
| wenzelm@44121 | 358 |
\ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 359 |
\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 360 |
\isanewline |
| wenzelm@44121 | 361 |
\ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 362 |
\ b{\isaliteral{3A}{\isacharcolon}}\ B\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 363 |
\isanewline |
| wenzelm@44121 | 364 |
\ \ \ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 365 |
\ a\ b\isanewline |
| wenzelm@44121 | 366 |
\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 367 |
\isanewline |
| wenzelm@44121 | 368 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 369 |
\ this\isanewline |
| wenzelm@44121 | 370 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 371 |
\ {\isaliteral{60}{\isacharbackquoteopen}}A{\isaliteral{60}{\isacharbackquoteclose}}\isanewline
|
| wenzelm@44121 | 372 |
\ \ \isacommand{note}\isamarkupfalse%
|
| wenzelm@44121 | 373 |
\ {\isaliteral{60}{\isacharbackquoteopen}}B{\isaliteral{60}{\isacharbackquoteclose}}%
|
| wenzelm@44121 | 374 |
\endisatagproof |
| wenzelm@44121 | 375 |
{\isafoldproof}%
|
| wenzelm@44121 | 376 |
% |
| wenzelm@44121 | 377 |
\isadelimproof |
| wenzelm@44121 | 378 |
\isanewline |
| wenzelm@44121 | 379 |
% |
| wenzelm@44121 | 380 |
\endisadelimproof |
| wenzelm@44121 | 381 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44121 | 382 |
% |
| wenzelm@44121 | 383 |
\begin{isamarkuptext}%
|
| wenzelm@44121 | 384 |
Explicit blocks as well as implicit blocks of nested goal |
| wenzelm@44121 | 385 |
statements (e.g.\ \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}) automatically introduce one extra
|
| wenzelm@44121 | 386 |
pair of parentheses in reserve. The \hyperlink{command.next}{\mbox{\isa{\isacommand{next}}}} command allows
|
| wenzelm@44122 | 387 |
to ``jump'' between these sub-blocks.% |
| wenzelm@44121 | 388 |
\end{isamarkuptext}%
|
| wenzelm@44121 | 389 |
\isamarkuptrue% |
| wenzelm@44121 | 390 |
\isacommand{notepad}\isamarkupfalse%
|
| wenzelm@44121 | 391 |
\isanewline |
| wenzelm@44121 | 392 |
\isakeyword{begin}\isanewline
|
| wenzelm@44121 | 393 |
% |
| wenzelm@44121 | 394 |
\isadelimproof |
| wenzelm@44121 | 395 |
\isanewline |
| wenzelm@44121 | 396 |
\ \ % |
| wenzelm@44121 | 397 |
\endisadelimproof |
| wenzelm@44121 | 398 |
% |
| wenzelm@44121 | 399 |
\isatagproof |
| wenzelm@44121 | 400 |
\isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 401 |
\isanewline |
| wenzelm@44121 | 402 |
\ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 403 |
\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 404 |
\isanewline |
| wenzelm@44121 | 405 |
\ \ \isacommand{next}\isamarkupfalse%
|
| wenzelm@44121 | 406 |
\isanewline |
| wenzelm@44121 | 407 |
\ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 408 |
\ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
|
| wenzelm@44121 | 409 |
\ \ \ \ \isacommand{proof}\isamarkupfalse%
|
| wenzelm@44121 | 410 |
\ {\isaliteral{2D}{\isacharminus}}\isanewline
|
| wenzelm@44121 | 411 |
\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
| wenzelm@44121 | 412 |
\ B\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 413 |
\isanewline |
| wenzelm@44121 | 414 |
\ \ \ \ \isacommand{next}\isamarkupfalse%
|
| wenzelm@44121 | 415 |
\isanewline |
| wenzelm@44121 | 416 |
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 417 |
\ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 418 |
\isanewline |
| wenzelm@44121 | 419 |
\ \ \ \ \isacommand{next}\isamarkupfalse%
|
| wenzelm@44121 | 420 |
\isanewline |
| wenzelm@44121 | 421 |
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 422 |
\ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 423 |
\isanewline |
| wenzelm@44121 | 424 |
\ \ \ \ \isacommand{qed}\isamarkupfalse%
|
| wenzelm@44121 | 425 |
\isanewline |
| wenzelm@44121 | 426 |
\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 427 |
% |
| wenzelm@44121 | 428 |
\begin{isamarkuptxt}%
|
| wenzelm@44121 | 429 |
Alternative version with explicit parentheses everywhere:% |
| wenzelm@44121 | 430 |
\end{isamarkuptxt}%
|
| wenzelm@44121 | 431 |
\isamarkuptrue% |
| wenzelm@44121 | 432 |
\ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 433 |
\isanewline |
| wenzelm@44121 | 434 |
\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 435 |
\isanewline |
| wenzelm@44121 | 436 |
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 437 |
\ a{\isaliteral{3A}{\isacharcolon}}\ A\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 438 |
\isanewline |
| wenzelm@44121 | 439 |
\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 440 |
\isanewline |
| wenzelm@44121 | 441 |
\ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 442 |
\isanewline |
| wenzelm@44121 | 443 |
\ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 444 |
\ b{\isaliteral{3A}{\isacharcolon}}\ B\isanewline
|
| wenzelm@44121 | 445 |
\ \ \ \ \ \ \isacommand{proof}\isamarkupfalse%
|
| wenzelm@44121 | 446 |
\ {\isaliteral{2D}{\isacharminus}}\isanewline
|
| wenzelm@44121 | 447 |
\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 448 |
\isanewline |
| wenzelm@44121 | 449 |
\ \ \ \ \ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
|
| wenzelm@44121 | 450 |
\ B\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 451 |
\isanewline |
| wenzelm@44121 | 452 |
\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 453 |
\isanewline |
| wenzelm@44121 | 454 |
\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 455 |
\isanewline |
| wenzelm@44121 | 456 |
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 457 |
\ c{\isaliteral{3A}{\isacharcolon}}\ C\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 458 |
\isanewline |
| wenzelm@44121 | 459 |
\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 460 |
\isanewline |
| wenzelm@44121 | 461 |
\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7B}{\isacharbraceleft}}}\isamarkupfalse%
|
| wenzelm@44121 | 462 |
\isanewline |
| wenzelm@44121 | 463 |
\ \ \ \ \ \ \ \ \ \ \isacommand{have}\isamarkupfalse%
|
| wenzelm@44121 | 464 |
\ d{\isaliteral{3A}{\isacharcolon}}\ D\ \isacommand{sorry}\isamarkupfalse%
|
| wenzelm@44121 | 465 |
\isanewline |
| wenzelm@44121 | 466 |
\ \ \ \ \ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 467 |
\isanewline |
| wenzelm@44121 | 468 |
\ \ \ \ \ \ \isacommand{qed}\isamarkupfalse%
|
| wenzelm@44121 | 469 |
\isanewline |
| wenzelm@44121 | 470 |
\ \ \ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 471 |
\isanewline |
| wenzelm@44121 | 472 |
\ \ \isacommand{{\isaliteral{7D}{\isacharbraceright}}}\isamarkupfalse%
|
| wenzelm@44121 | 473 |
% |
| wenzelm@44121 | 474 |
\endisatagproof |
| wenzelm@44121 | 475 |
{\isafoldproof}%
|
| wenzelm@44121 | 476 |
% |
| wenzelm@44121 | 477 |
\isadelimproof |
| wenzelm@44121 | 478 |
\isanewline |
| wenzelm@44121 | 479 |
% |
| wenzelm@44121 | 480 |
\endisadelimproof |
| wenzelm@44121 | 481 |
\isanewline |
| wenzelm@44121 | 482 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44121 | 483 |
\isanewline |
| wenzelm@44121 | 484 |
% |
| wenzelm@44121 | 485 |
\isadelimtheory |
| wenzelm@44121 | 486 |
\isanewline |
| wenzelm@44121 | 487 |
% |
| wenzelm@44121 | 488 |
\endisadelimtheory |
| wenzelm@44121 | 489 |
% |
| wenzelm@44121 | 490 |
\isatagtheory |
| wenzelm@44121 | 491 |
\isacommand{end}\isamarkupfalse%
|
| wenzelm@44121 | 492 |
% |
| wenzelm@44121 | 493 |
\endisatagtheory |
| wenzelm@44121 | 494 |
{\isafoldtheory}%
|
| wenzelm@44121 | 495 |
% |
| wenzelm@44121 | 496 |
\isadelimtheory |
| wenzelm@44121 | 497 |
% |
| wenzelm@44121 | 498 |
\endisadelimtheory |
| wenzelm@44121 | 499 |
\end{isabellebody}%
|
| wenzelm@44121 | 500 |
%%% Local Variables: |
| wenzelm@44121 | 501 |
%%% mode: latex |
| wenzelm@44121 | 502 |
%%% TeX-master: "root" |
| wenzelm@44121 | 503 |
%%% End: |