doc-src/TutorialI/Types/document/Numbers.tex
author wenzelm
Tue Oct 16 17:07:40 2007 +0200 (2007-10-16)
changeset 25056 743f3603ba8b
parent 23504 2b2323124e8e
child 27376 ffe9b958bada
permissions -rw-r--r--
updated;
     1 %
     2 \begin{isabellebody}%
     3 \def\isabellecontext{Numbers}%
     4 %
     5 \isadelimtheory
     6 \isanewline
     7 %
     8 \endisadelimtheory
     9 %
    10 \isatagtheory
    11 \isacommand{theory}\isamarkupfalse%
    12 \ Numbers\ \isakeyword{imports}\ Real\ \isakeyword{begin}%
    13 \endisatagtheory
    14 {\isafoldtheory}%
    15 %
    16 \isadelimtheory
    17 \isanewline
    18 %
    19 \endisadelimtheory
    20 %
    21 \isadelimML
    22 \isanewline
    23 %
    24 \endisadelimML
    25 %
    26 \isatagML
    27 \isacommand{ML}\isamarkupfalse%
    28 \ {\isachardoublequoteopen}Pretty{\isachardot}setmargin\ {\isadigit{6}}{\isadigit{4}}{\isachardoublequoteclose}\isanewline
    29 \isacommand{ML}\isamarkupfalse%
    30 \ {\isachardoublequoteopen}ThyOutput{\isachardot}indent\ {\isacharcolon}{\isacharequal}\ {\isadigit{0}}{\isachardoublequoteclose}%
    31 \endisatagML
    32 {\isafoldML}%
    33 %
    34 \isadelimML
    35 %
    36 \endisadelimML
    37 %
    38 \begin{isamarkuptext}%
    39 numeric literals; default simprules; can re-orient%
    40 \end{isamarkuptext}%
    41 \isamarkuptrue%
    42 \isacommand{lemma}\isamarkupfalse%
    43 \ {\isachardoublequoteopen}{\isadigit{2}}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m{\isachardoublequoteclose}%
    44 \isadelimproof
    45 %
    46 \endisadelimproof
    47 %
    48 \isatagproof
    49 %
    50 \begin{isamarkuptxt}%
    51 \begin{isabelle}%
    52 \ {\isadigit{1}}{\isachardot}\ {\isacharparenleft}{\isadigit{2}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isacharasterisk}\ m\ {\isacharequal}\ m\ {\isacharplus}\ m%
    53 \end{isabelle}%
    54 \end{isamarkuptxt}%
    55 \isamarkuptrue%
    56 \isacommand{oops}\isamarkupfalse%
    57 %
    58 \endisatagproof
    59 {\isafoldproof}%
    60 %
    61 \isadelimproof
    62 %
    63 \endisadelimproof
    64 \isanewline
    65 \isanewline
    66 \isacommand{consts}\isamarkupfalse%
    67 \ h\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\isanewline
    68 \isacommand{recdef}\isamarkupfalse%
    69 \ h\ {\isachardoublequoteopen}{\isacharbraceleft}{\isacharbraceright}{\isachardoublequoteclose}\isanewline
    70 {\isachardoublequoteopen}h\ i\ {\isacharequal}\ {\isacharparenleft}if\ i\ {\isacharequal}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isacharparenright}{\isachardoublequoteclose}%
    71 \begin{isamarkuptext}%
    72 \isa{h\ {\isadigit{3}}\ {\isacharequal}\ {\isadigit{2}}}
    73 \isa{h\ i\ {\isacharequal}\ i}%
    74 \end{isamarkuptext}%
    75 \isamarkuptrue%
    76 %
    77 \begin{isamarkuptext}%
    78 \begin{isabelle}%
    79 Numeral{\isadigit{0}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}%
    80 \end{isabelle}
    81 \rulename{numeral_0_eq_0}
    82 
    83 \begin{isabelle}%
    84 Numeral{\isadigit{1}}\ {\isacharequal}\ {\isacharparenleft}{\isadigit{1}}{\isasymColon}{\isacharprime}a{\isacharparenright}%
    85 \end{isabelle}
    86 \rulename{numeral_1_eq_1}
    87 
    88 \begin{isabelle}%
    89 {\isadigit{2}}\ {\isacharplus}\ n\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    90 \end{isabelle}
    91 \rulename{add_2_eq_Suc}
    92 
    93 \begin{isabelle}%
    94 n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharequal}\ Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}%
    95 \end{isabelle}
    96 \rulename{add_2_eq_Suc'}
    97 
    98 \begin{isabelle}%
    99 a\ {\isacharplus}\ b\ {\isacharplus}\ c\ {\isacharequal}\ a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}%
   100 \end{isabelle}
   101 \rulename{add_assoc}
   102 
   103 \begin{isabelle}%
   104 a\ {\isacharplus}\ b\ {\isacharequal}\ b\ {\isacharplus}\ a%
   105 \end{isabelle}
   106 \rulename{add_commute}
   107 
   108 \begin{isabelle}%
   109 a\ {\isacharplus}\ {\isacharparenleft}b\ {\isacharplus}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharplus}\ {\isacharparenleft}a\ {\isacharplus}\ c{\isacharparenright}%
   110 \end{isabelle}
   111 \rulename{add_left_commute}
   112 
   113 these form add_ac; similarly there is mult_ac%
   114 \end{isamarkuptext}%
   115 \isamarkuptrue%
   116 \isacommand{lemma}\isamarkupfalse%
   117 \ {\isachardoublequoteopen}Suc{\isacharparenleft}i\ {\isacharplus}\ j{\isacharasterisk}l{\isacharasterisk}k\ {\isacharplus}\ m{\isacharasterisk}n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n{\isacharasterisk}m\ {\isacharplus}\ i\ {\isacharplus}\ k{\isacharasterisk}j{\isacharasterisk}l{\isacharparenright}{\isachardoublequoteclose}%
   118 \isadelimproof
   119 %
   120 \endisadelimproof
   121 %
   122 \isatagproof
   123 %
   124 \begin{isamarkuptxt}%
   125 \begin{isabelle}%
   126 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ j\ {\isacharasterisk}\ l\ {\isacharasterisk}\ k\ {\isacharplus}\ m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ f\ {\isacharparenleft}n\ {\isacharasterisk}\ m\ {\isacharplus}\ i\ {\isacharplus}\ k\ {\isacharasterisk}\ j\ {\isacharasterisk}\ l{\isacharparenright}%
   127 \end{isabelle}%
   128 \end{isamarkuptxt}%
   129 \isamarkuptrue%
   130 \isacommand{apply}\isamarkupfalse%
   131 \ {\isacharparenleft}simp\ add{\isacharcolon}\ add{\isacharunderscore}ac\ mult{\isacharunderscore}ac{\isacharparenright}%
   132 \begin{isamarkuptxt}%
   133 \begin{isabelle}%
   134 \ {\isadigit{1}}{\isachardot}\ Suc\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
   135 \isaindent{\ {\isadigit{1}}{\isachardot}\ }f\ {\isacharparenleft}i\ {\isacharplus}\ {\isacharparenleft}m\ {\isacharasterisk}\ n\ {\isacharplus}\ j\ {\isacharasterisk}\ {\isacharparenleft}k\ {\isacharasterisk}\ l{\isacharparenright}{\isacharparenright}{\isacharparenright}%
   136 \end{isabelle}%
   137 \end{isamarkuptxt}%
   138 \isamarkuptrue%
   139 \isacommand{oops}\isamarkupfalse%
   140 %
   141 \endisatagproof
   142 {\isafoldproof}%
   143 %
   144 \isadelimproof
   145 %
   146 \endisadelimproof
   147 %
   148 \begin{isamarkuptext}%
   149 \begin{isabelle}%
   150 m\ {\isasymle}\ n\ {\isasymLongrightarrow}\ m\ div\ k\ {\isasymle}\ n\ div\ k%
   151 \end{isabelle}
   152 \rulename{div_le_mono}
   153 
   154 \begin{isabelle}%
   155 {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ {\isacharminus}\ n\ {\isacharasterisk}\ k%
   156 \end{isabelle}
   157 \rulename{diff_mult_distrib}
   158 
   159 \begin{isabelle}%
   160 m\ mod\ n\ {\isacharasterisk}\ k\ {\isacharequal}\ m\ {\isacharasterisk}\ k\ mod\ {\isacharparenleft}n\ {\isacharasterisk}\ k{\isacharparenright}%
   161 \end{isabelle}
   162 \rulename{mod_mult_distrib}
   163 
   164 \begin{isabelle}%
   165 P\ {\isacharparenleft}a\ {\isacharminus}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isacharparenleft}a\ {\isacharless}\ b\ {\isasymlongrightarrow}\ P\ {\isadigit{0}}{\isacharparenright}\ {\isasymand}\ {\isacharparenleft}{\isasymforall}d{\isachardot}\ a\ {\isacharequal}\ b\ {\isacharplus}\ d\ {\isasymlongrightarrow}\ P\ d{\isacharparenright}{\isacharparenright}%
   166 \end{isabelle}
   167 \rulename{nat_diff_split}%
   168 \end{isamarkuptext}%
   169 \isamarkuptrue%
   170 \isacommand{lemma}\isamarkupfalse%
   171 \ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
   172 %
   173 \isadelimproof
   174 %
   175 \endisadelimproof
   176 %
   177 \isatagproof
   178 \isacommand{apply}\isamarkupfalse%
   179 \ {\isacharparenleft}clarsimp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split\ iff\ del{\isacharcolon}\ less{\isacharunderscore}Suc{\isadigit{0}}{\isacharparenright}\isanewline
   180 \ %
   181 \isamarkupcmt{\begin{isabelle}%
   182 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ Suc\ {\isadigit{0}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ Suc\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
   183 \end{isabelle}%
   184 }
   185 \isanewline
   186 \isacommand{apply}\isamarkupfalse%
   187 \ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{0}}{\isachardoublequoteclose}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
   188 \isacommand{done}\isamarkupfalse%
   189 %
   190 \endisatagproof
   191 {\isafoldproof}%
   192 %
   193 \isadelimproof
   194 \isanewline
   195 %
   196 \endisadelimproof
   197 \isanewline
   198 \isanewline
   199 \isacommand{lemma}\isamarkupfalse%
   200 \ {\isachardoublequoteopen}{\isacharparenleft}n\ {\isacharminus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ n\ {\isacharminus}\ {\isacharparenleft}{\isadigit{4}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}{\isachardoublequoteclose}\isanewline
   201 %
   202 \isadelimproof
   203 %
   204 \endisadelimproof
   205 %
   206 \isatagproof
   207 \isacommand{apply}\isamarkupfalse%
   208 \ {\isacharparenleft}simp\ split{\isacharcolon}\ nat{\isacharunderscore}diff{\isacharunderscore}split{\isacharcomma}\ clarify{\isacharparenright}\isanewline
   209 \ %
   210 \isamarkupcmt{\begin{isabelle}%
   211 \ {\isadigit{1}}{\isachardot}\ {\isasymAnd}d{\isachardot}\ {\isasymlbrakk}n\ {\isacharless}\ {\isadigit{2}}{\isacharsemicolon}\ n\ {\isacharasterisk}\ n\ {\isacharequal}\ {\isadigit{4}}\ {\isacharplus}\ d{\isasymrbrakk}\ {\isasymLongrightarrow}\ d\ {\isacharequal}\ {\isadigit{0}}%
   212 \end{isabelle}%
   213 }
   214 \isanewline
   215 \isacommand{apply}\isamarkupfalse%
   216 \ {\isacharparenleft}subgoal{\isacharunderscore}tac\ {\isachardoublequoteopen}n{\isacharequal}{\isadigit{0}}\ {\isacharbar}\ n{\isacharequal}{\isadigit{1}}{\isachardoublequoteclose}{\isacharcomma}\ force{\isacharcomma}\ arith{\isacharparenright}\isanewline
   217 \isacommand{done}\isamarkupfalse%
   218 %
   219 \endisatagproof
   220 {\isafoldproof}%
   221 %
   222 \isadelimproof
   223 %
   224 \endisadelimproof
   225 %
   226 \begin{isamarkuptext}%
   227 \begin{isabelle}%
   228 m\ mod\ n\ {\isacharequal}\ {\isacharparenleft}if\ m\ {\isacharless}\ n\ then\ m\ else\ {\isacharparenleft}m\ {\isacharminus}\ n{\isacharparenright}\ mod\ n{\isacharparenright}%
   229 \end{isabelle}
   230 \rulename{mod_if}
   231 
   232 \begin{isabelle}%
   233 m\ div\ n\ {\isacharasterisk}\ n\ {\isacharplus}\ m\ mod\ n\ {\isacharequal}\ m%
   234 \end{isabelle}
   235 \rulename{mod_div_equality}
   236 
   237 
   238 \begin{isabelle}%
   239 a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%
   240 \end{isabelle}
   241 \rulename{div_mult1_eq}
   242 
   243 \begin{isabelle}%
   244 a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
   245 \end{isabelle}
   246 \rulename{mod_mult1_eq}
   247 
   248 \begin{isabelle}%
   249 a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
   250 \end{isabelle}
   251 \rulename{div_mult2_eq}
   252 
   253 \begin{isabelle}%
   254 a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b%
   255 \end{isabelle}
   256 \rulename{mod_mult2_eq}
   257 
   258 \begin{isabelle}%
   259 {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ c\ {\isacharasterisk}\ a\ div\ {\isacharparenleft}c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ a\ div\ b%
   260 \end{isabelle}
   261 \rulename{div_mult_mult1}
   262 
   263 \begin{isabelle}%
   264 a\ div\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}%
   265 \end{isabelle}
   266 \rulename{DIVISION_BY_ZERO_DIV}
   267 
   268 \begin{isabelle}%
   269 a\ mod\ {\isadigit{0}}\ {\isacharequal}\ a%
   270 \end{isabelle}
   271 \rulename{DIVISION_BY_ZERO_MOD}
   272 
   273 \begin{isabelle}%
   274 {\isasymlbrakk}m\ dvd\ n{\isacharsemicolon}\ n\ dvd\ m{\isasymrbrakk}\ {\isasymLongrightarrow}\ m\ {\isacharequal}\ n%
   275 \end{isabelle}
   276 \rulename{dvd_anti_sym}
   277 
   278 \begin{isabelle}%
   279 {\isasymlbrakk}k\ dvd\ m{\isacharsemicolon}\ k\ dvd\ n{\isasymrbrakk}\ {\isasymLongrightarrow}\ k\ dvd\ m\ {\isacharplus}\ n%
   280 \end{isabelle}
   281 \rulename{dvd_add}
   282 
   283 For the integers, I'd list a few theorems that somehow involve negative 
   284 numbers.%
   285 \end{isamarkuptext}%
   286 \isamarkuptrue%
   287 %
   288 \begin{isamarkuptext}%
   289 Division, remainder of negatives
   290 
   291 
   292 \begin{isabelle}%
   293 {\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ {\isadigit{0}}\ {\isasymle}\ a\ mod\ b%
   294 \end{isabelle}
   295 \rulename{pos_mod_sign}
   296 
   297 \begin{isabelle}%
   298 {\isadigit{0}}\ {\isacharless}\ b\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isacharless}\ b%
   299 \end{isabelle}
   300 \rulename{pos_mod_bound}
   301 
   302 \begin{isabelle}%
   303 b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ a\ mod\ b\ {\isasymle}\ {\isadigit{0}}%
   304 \end{isabelle}
   305 \rulename{neg_mod_sign}
   306 
   307 \begin{isabelle}%
   308 b\ {\isacharless}\ {\isadigit{0}}\ {\isasymLongrightarrow}\ b\ {\isacharless}\ a\ mod\ b%
   309 \end{isabelle}
   310 \rulename{neg_mod_bound}
   311 
   312 \begin{isabelle}%
   313 {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ div\ c\ {\isacharequal}\ a\ div\ c\ {\isacharplus}\ b\ div\ c\ {\isacharplus}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ div\ c%
   314 \end{isabelle}
   315 \rulename{zdiv_zadd1_eq}
   316 
   317 \begin{isabelle}%
   318 {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ mod\ c\ {\isacharequal}\ {\isacharparenleft}a\ mod\ c\ {\isacharplus}\ b\ mod\ c{\isacharparenright}\ mod\ c%
   319 \end{isabelle}
   320 \rulename{zmod_zadd1_eq}
   321 
   322 \begin{isabelle}%
   323 a\ {\isacharasterisk}\ b\ div\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ div\ c{\isacharparenright}\ {\isacharplus}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ div\ c%
   324 \end{isabelle}
   325 \rulename{zdiv_zmult1_eq}
   326 
   327 \begin{isabelle}%
   328 a\ {\isacharasterisk}\ b\ mod\ c\ {\isacharequal}\ a\ {\isacharasterisk}\ {\isacharparenleft}b\ mod\ c{\isacharparenright}\ mod\ c%
   329 \end{isabelle}
   330 \rulename{zmod_zmult1_eq}
   331 
   332 \begin{isabelle}%
   333 {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ div\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ a\ div\ b\ div\ c%
   334 \end{isabelle}
   335 \rulename{zdiv_zmult2_eq}
   336 
   337 \begin{isabelle}%
   338 {\isadigit{0}}\ {\isacharless}\ c\ {\isasymLongrightarrow}\ a\ mod\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ b\ {\isacharasterisk}\ {\isacharparenleft}a\ div\ b\ mod\ c{\isacharparenright}\ {\isacharplus}\ a\ mod\ b%
   339 \end{isabelle}
   340 \rulename{zmod_zmult2_eq}%
   341 \end{isamarkuptext}%
   342 \isamarkuptrue%
   343 \isacommand{lemma}\isamarkupfalse%
   344 \ {\isachardoublequoteopen}abs\ {\isacharparenleft}x{\isacharplus}y{\isacharparenright}\ {\isasymle}\ abs\ x\ {\isacharplus}\ abs\ {\isacharparenleft}y\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   345 %
   346 \isadelimproof
   347 %
   348 \endisadelimproof
   349 %
   350 \isatagproof
   351 \isacommand{by}\isamarkupfalse%
   352 \ arith%
   353 \endisatagproof
   354 {\isafoldproof}%
   355 %
   356 \isadelimproof
   357 \isanewline
   358 %
   359 \endisadelimproof
   360 \isanewline
   361 \isacommand{lemma}\isamarkupfalse%
   362 \ {\isachardoublequoteopen}abs\ {\isacharparenleft}{\isadigit{2}}{\isacharasterisk}x{\isacharparenright}\ {\isacharequal}\ {\isadigit{2}}\ {\isacharasterisk}\ abs\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ int{\isacharparenright}{\isachardoublequoteclose}\isanewline
   363 %
   364 \isadelimproof
   365 %
   366 \endisadelimproof
   367 %
   368 \isatagproof
   369 \isacommand{by}\isamarkupfalse%
   370 \ {\isacharparenleft}simp\ add{\isacharcolon}\ abs{\isacharunderscore}if{\isacharparenright}%
   371 \endisatagproof
   372 {\isafoldproof}%
   373 %
   374 \isadelimproof
   375 %
   376 \endisadelimproof
   377 %
   378 \begin{isamarkuptext}%
   379 Induction rules for the Integers
   380 
   381 \begin{isabelle}%
   382 {\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isasymle}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
   383 \end{isabelle}
   384 \rulename{int_ge_induct}
   385 
   386 \begin{isabelle}%
   387 {\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}k\ {\isacharless}\ i{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
   388 \end{isabelle}
   389 \rulename{int_gr_induct}
   390 
   391 \begin{isabelle}%
   392 {\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ k{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isasymle}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
   393 \end{isabelle}
   394 \rulename{int_le_induct}
   395 
   396 \begin{isabelle}%
   397 {\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ {\isacharparenleft}k\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isacharsemicolon}\ {\isasymAnd}i{\isachardot}\ {\isasymlbrakk}i\ {\isacharless}\ k{\isacharsemicolon}\ P\ i{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isacharparenleft}i\ {\isacharminus}\ {\isadigit{1}}{\isacharparenright}{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ i%
   398 \end{isabelle}
   399 \rulename{int_less_induct}%
   400 \end{isamarkuptext}%
   401 \isamarkuptrue%
   402 %
   403 \begin{isamarkuptext}%
   404 FIELDS
   405 
   406 \begin{isabelle}%
   407 x\ {\isacharless}\ y\ {\isasymLongrightarrow}\ {\isasymexists}z{\isachargreater}x{\isachardot}\ z\ {\isacharless}\ y%
   408 \end{isabelle}
   409 \rulename{dense}
   410 
   411 \begin{isabelle}%
   412 a\ {\isacharasterisk}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ b\ {\isacharslash}\ c%
   413 \end{isabelle}
   414 \rulename{times_divide_eq_right}
   415 
   416 \begin{isabelle}%
   417 b\ {\isacharslash}\ c\ {\isacharasterisk}\ a\ {\isacharequal}\ b\ {\isacharasterisk}\ a\ {\isacharslash}\ c%
   418 \end{isabelle}
   419 \rulename{times_divide_eq_left}
   420 
   421 \begin{isabelle}%
   422 a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharslash}\ c{\isacharparenright}\ {\isacharequal}\ a\ {\isacharasterisk}\ c\ {\isacharslash}\ b%
   423 \end{isabelle}
   424 \rulename{divide_divide_eq_right}
   425 
   426 \begin{isabelle}%
   427 a\ {\isacharslash}\ b\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharparenleft}b\ {\isacharasterisk}\ c{\isacharparenright}%
   428 \end{isabelle}
   429 \rulename{divide_divide_eq_left}
   430 
   431 \begin{isabelle}%
   432 {\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharminus}\ a\ {\isacharslash}\ b%
   433 \end{isabelle}
   434 \rulename{minus_divide_left}
   435 
   436 \begin{isabelle}%
   437 {\isacharminus}\ {\isacharparenleft}a\ {\isacharslash}\ b{\isacharparenright}\ {\isacharequal}\ a\ {\isacharslash}\ {\isacharminus}\ b%
   438 \end{isabelle}
   439 \rulename{minus_divide_right}
   440 
   441 This last NOT a simprule
   442 
   443 \begin{isabelle}%
   444 {\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharslash}\ c\ {\isacharequal}\ a\ {\isacharslash}\ c\ {\isacharplus}\ b\ {\isacharslash}\ c%
   445 \end{isabelle}
   446 \rulename{add_divide_distrib}%
   447 \end{isamarkuptext}%
   448 \isamarkuptrue%
   449 \isacommand{lemma}\isamarkupfalse%
   450 \ {\isachardoublequoteopen}{\isadigit{3}}{\isacharslash}{\isadigit{4}}\ {\isacharless}\ {\isacharparenleft}{\isadigit{7}}{\isacharslash}{\isadigit{8}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequoteclose}\isanewline
   451 %
   452 \isadelimproof
   453 %
   454 \endisadelimproof
   455 %
   456 \isatagproof
   457 \isacommand{by}\isamarkupfalse%
   458 \ simp%
   459 \endisatagproof
   460 {\isafoldproof}%
   461 %
   462 \isadelimproof
   463 \ \isanewline
   464 %
   465 \endisadelimproof
   466 \isanewline
   467 \isacommand{lemma}\isamarkupfalse%
   468 \ {\isachardoublequoteopen}P\ {\isacharparenleft}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
   469 \isadelimproof
   470 %
   471 \endisadelimproof
   472 %
   473 \isatagproof
   474 %
   475 \begin{isamarkuptxt}%
   476 \begin{isabelle}%
   477 \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}{\isacharparenright}%
   478 \end{isabelle}%
   479 \end{isamarkuptxt}%
   480 \isamarkuptrue%
   481 \isacommand{apply}\isamarkupfalse%
   482 \ simp%
   483 \begin{isamarkuptxt}%
   484 \begin{isabelle}%
   485 \ {\isadigit{1}}{\isachardot}\ P\ {\isacharparenleft}{\isadigit{2}}\ {\isacharslash}\ {\isadigit{5}}{\isacharparenright}%
   486 \end{isabelle}%
   487 \end{isamarkuptxt}%
   488 \isamarkuptrue%
   489 \isacommand{oops}\isamarkupfalse%
   490 %
   491 \endisatagproof
   492 {\isafoldproof}%
   493 %
   494 \isadelimproof
   495 %
   496 \endisadelimproof
   497 \isanewline
   498 \isanewline
   499 \isacommand{lemma}\isamarkupfalse%
   500 \ {\isachardoublequoteopen}{\isacharparenleft}{\isadigit{3}}{\isacharslash}{\isadigit{4}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}{\isacharslash}{\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ {\isacharparenleft}x\ {\isacharcolon}{\isacharcolon}\ real{\isacharparenright}{\isachardoublequoteclose}%
   501 \isadelimproof
   502 %
   503 \endisadelimproof
   504 %
   505 \isatagproof
   506 %
   507 \begin{isamarkuptxt}%
   508 \begin{isabelle}%
   509 \ {\isadigit{1}}{\isachardot}\ {\isadigit{3}}\ {\isacharslash}\ {\isadigit{4}}\ {\isacharasterisk}\ {\isacharparenleft}{\isadigit{8}}\ {\isacharslash}\ {\isadigit{1}}{\isadigit{5}}{\isacharparenright}\ {\isacharless}\ x%
   510 \end{isabelle}%
   511 \end{isamarkuptxt}%
   512 \isamarkuptrue%
   513 \isacommand{apply}\isamarkupfalse%
   514 \ simp%
   515 \begin{isamarkuptxt}%
   516 \begin{isabelle}%
   517 \ {\isadigit{1}}{\isachardot}\ {\isadigit{2}}\ {\isacharless}\ x\ {\isacharasterisk}\ {\isadigit{5}}%
   518 \end{isabelle}%
   519 \end{isamarkuptxt}%
   520 \isamarkuptrue%
   521 \isacommand{oops}\isamarkupfalse%
   522 %
   523 \endisatagproof
   524 {\isafoldproof}%
   525 %
   526 \isadelimproof
   527 %
   528 \endisadelimproof
   529 %
   530 \begin{isamarkuptext}%
   531 Ring and Field
   532 
   533 Requires a field, or else an ordered ring
   534 
   535 \begin{isabelle}%
   536 {\isacharparenleft}a\ {\isacharasterisk}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ b\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}{\isacharparenright}%
   537 \end{isabelle}
   538 \rulename{mult_eq_0_iff}
   539 
   540 \begin{isabelle}%
   541 {\isacharparenleft}a\ {\isacharasterisk}\ c\ {\isacharequal}\ b\ {\isacharasterisk}\ c{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
   542 \end{isabelle}
   543 \rulename{mult_cancel_right}
   544 
   545 \begin{isabelle}%
   546 {\isacharparenleft}c\ {\isacharasterisk}\ a\ {\isacharequal}\ c\ {\isacharasterisk}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
   547 \end{isabelle}
   548 \rulename{mult_cancel_left}%
   549 \end{isamarkuptext}%
   550 \isamarkuptrue%
   551 %
   552 \isadelimML
   553 %
   554 \endisadelimML
   555 %
   556 \isatagML
   557 \isacommand{ML}\isamarkupfalse%
   558 {\isacharverbatimopen}set\ show{\isacharunderscore}sorts{\isacharverbatimclose}%
   559 \endisatagML
   560 {\isafoldML}%
   561 %
   562 \isadelimML
   563 %
   564 \endisadelimML
   565 %
   566 \begin{isamarkuptext}%
   567 effect of show sorts on the above
   568 
   569 \begin{isabelle}%
   570 {\isacharparenleft}{\isacharparenleft}c{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}a{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isacharequal}\isanewline
   571 \isaindent{{\isacharparenleft}}c\ {\isacharasterisk}\ {\isacharparenleft}b{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}{\isacharparenright}\ {\isacharequal}\isanewline
   572 {\isacharparenleft}c\ {\isacharequal}\ {\isacharparenleft}{\isadigit{0}}{\isasymColon}{\isacharprime}a{\isasymColon}ring{\isacharunderscore}no{\isacharunderscore}zero{\isacharunderscore}divisors{\isacharparenright}\ {\isasymor}\ a\ {\isacharequal}\ b{\isacharparenright}%
   573 \end{isabelle}
   574 \rulename{mult_cancel_left}%
   575 \end{isamarkuptext}%
   576 \isamarkuptrue%
   577 %
   578 \isadelimML
   579 %
   580 \endisadelimML
   581 %
   582 \isatagML
   583 \isacommand{ML}\isamarkupfalse%
   584 {\isacharverbatimopen}reset\ show{\isacharunderscore}sorts{\isacharverbatimclose}%
   585 \endisatagML
   586 {\isafoldML}%
   587 %
   588 \isadelimML
   589 %
   590 \endisadelimML
   591 %
   592 \begin{isamarkuptext}%
   593 absolute value
   594 
   595 \begin{isabelle}%
   596 {\isasymbar}a\ {\isacharasterisk}\ b{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharasterisk}\ {\isasymbar}b{\isasymbar}%
   597 \end{isabelle}
   598 \rulename{abs_mult}
   599 
   600 \begin{isabelle}%
   601 {\isacharparenleft}{\isasymbar}a{\isasymbar}\ {\isasymle}\ b{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isasymle}\ b\ {\isasymand}\ {\isacharminus}\ a\ {\isasymle}\ b{\isacharparenright}%
   602 \end{isabelle}
   603 \rulename{abs_le_iff}
   604 
   605 \begin{isabelle}%
   606 {\isasymbar}a\ {\isacharplus}\ b{\isasymbar}\ {\isasymle}\ {\isasymbar}a{\isasymbar}\ {\isacharplus}\ {\isasymbar}b{\isasymbar}%
   607 \end{isabelle}
   608 \rulename{abs_triangle_ineq}
   609 
   610 \begin{isabelle}%
   611 a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharplus}\ n{\isacharparenright}\ {\isacharequal}\ a\ {\isacharcircum}\ m\ {\isacharasterisk}\ a\ {\isacharcircum}\ n%
   612 \end{isabelle}
   613 \rulename{power_add}
   614 
   615 \begin{isabelle}%
   616 a\ {\isacharcircum}\ {\isacharparenleft}m\ {\isacharasterisk}\ n{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}a\ {\isacharcircum}\ m{\isacharparenright}\ {\isacharcircum}\ n%
   617 \end{isabelle}
   618 \rulename{power_mult}
   619 
   620 \begin{isabelle}%
   621 {\isasymbar}a\ {\isacharcircum}\ n{\isasymbar}\ {\isacharequal}\ {\isasymbar}a{\isasymbar}\ {\isacharcircum}\ n%
   622 \end{isabelle}
   623 \rulename{power_abs}%
   624 \end{isamarkuptext}%
   625 \isamarkuptrue%
   626 %
   627 \isadelimtheory
   628 %
   629 \endisadelimtheory
   630 %
   631 \isatagtheory
   632 \isacommand{end}\isamarkupfalse%
   633 %
   634 \endisatagtheory
   635 {\isafoldtheory}%
   636 %
   637 \isadelimtheory
   638 %
   639 \endisadelimtheory
   640 \isanewline
   641 \end{isabellebody}%
   642 %%% Local Variables:
   643 %%% mode: latex
   644 %%% TeX-master: "root"
   645 %%% End: