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