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