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