1.1 --- a/doc-src/TutorialI/Types/document/Numbers.tex Thu Jul 26 16:08:16 2012 +0200
1.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
1.3 @@ -1,611 +0,0 @@
1.4 -%
1.5 -\begin{isabellebody}%
1.6 -\def\isabellecontext{Numbers}%
1.7 -%
1.8 -\isadelimtheory
1.9 -%
1.10 -\endisadelimtheory
1.11 -%
1.12 -\isatagtheory
1.13 -\isacommand{theory}\isamarkupfalse%
1.14 -\ Numbers\isanewline
1.15 -\isakeyword{imports}\ Complex{\isaliteral{5F}{\isacharunderscore}}Main\isanewline
1.16 -\isakeyword{begin}%
1.17 -\endisatagtheory
1.18 -{\isafoldtheory}%
1.19 -%
1.20 -\isadelimtheory
1.21 -\isanewline
1.22 -%
1.23 -\endisadelimtheory
1.24 -%
1.25 -\isadelimML
1.26 -\isanewline
1.27 -%
1.28 -\endisadelimML
1.29 -%
1.30 -\isatagML
1.31 -\isacommand{ML}\isamarkupfalse%
1.32 -\ {\isaliteral{22}{\isachardoublequoteopen}}Pretty{\isaliteral{2E}{\isachardot}}margin{\isaliteral{5F}{\isacharunderscore}}default\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3D}{\isacharequal}}\ {\isadigit{6}}{\isadigit{4}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.33 -\endisatagML
1.34 -{\isafoldML}%
1.35 -%
1.36 -\isadelimML
1.37 -\isanewline
1.38 -%
1.39 -\endisadelimML
1.40 -\isacommand{declare}\isamarkupfalse%
1.41 -\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5B}{\isacharbrackleft}}thy{\isaliteral{5F}{\isacharunderscore}}output{\isaliteral{5F}{\isacharunderscore}}indent\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{5D}{\isacharbrackright}}%
1.42 -\begin{isamarkuptext}%
1.43 -numeric literals; default simprules; can re-orient%
1.44 -\end{isamarkuptext}%
1.45 -\isamarkuptrue%
1.46 -\isacommand{lemma}\isamarkupfalse%
1.47 -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2B}{\isacharplus}}\ m{\isaliteral{22}{\isachardoublequoteclose}}%
1.48 -\isadelimproof
1.49 -%
1.50 -\endisadelimproof
1.51 -%
1.52 -\isatagproof
1.53 -%
1.54 -\begin{isamarkuptxt}%
1.55 -\begin{isabelle}%
1.56 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2B}{\isacharplus}}\ m%
1.57 -\end{isabelle}%
1.58 -\end{isamarkuptxt}%
1.59 -\isamarkuptrue%
1.60 -\isacommand{oops}\isamarkupfalse%
1.61 -%
1.62 -\endisatagproof
1.63 -{\isafoldproof}%
1.64 -%
1.65 -\isadelimproof
1.66 -%
1.67 -\endisadelimproof
1.68 -\isanewline
1.69 -\isanewline
1.70 -\isacommand{fun}\isamarkupfalse%
1.71 -\ h\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline
1.72 -{\isaliteral{22}{\isachardoublequoteopen}}h\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ i\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{3}}\ then\ {\isadigit{2}}\ else\ i{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.73 -\begin{isamarkuptext}%
1.74 -\isa{h\ {\isadigit{3}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}}
1.75 -\isa{h\ i\ {\isaliteral{3D}{\isacharequal}}\ i}%
1.76 -\end{isamarkuptext}%
1.77 -\isamarkuptrue%
1.78 -%
1.79 -\begin{isamarkuptext}%
1.80 -\begin{isabelle}%
1.81 -Numeral{\isadigit{1}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}%
1.82 -\end{isabelle}
1.83 -\rulename{numeral_1_eq_1}
1.84 -
1.85 -\begin{isabelle}%
1.86 -{\isadigit{2}}\ {\isaliteral{2B}{\isacharplus}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}%
1.87 -\end{isabelle}
1.88 -\rulename{add_2_eq_Suc}
1.89 -
1.90 -\begin{isabelle}%
1.91 -n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}\ {\isaliteral{3D}{\isacharequal}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}%
1.92 -\end{isabelle}
1.93 -\rulename{add_2_eq_Suc'}
1.94 -
1.95 -\begin{isabelle}%
1.96 -a\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{2B}{\isacharplus}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}%
1.97 -\end{isabelle}
1.98 -\rulename{add_assoc}
1.99 -
1.100 -\begin{isabelle}%
1.101 -a\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ a%
1.102 -\end{isabelle}
1.103 -\rulename{add_commute}
1.104 -
1.105 -\begin{isabelle}%
1.106 -b\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2B}{\isacharplus}}\ c{\isaliteral{29}{\isacharparenright}}%
1.107 -\end{isabelle}
1.108 -\rulename{add_left_commute}
1.109 -
1.110 -these form add_ac; similarly there is mult_ac%
1.111 -\end{isamarkuptext}%
1.112 -\isamarkuptrue%
1.113 -\isacommand{lemma}\isamarkupfalse%
1.114 -\ {\isaliteral{22}{\isachardoublequoteopen}}Suc{\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j{\isaliteral{2A}{\isacharasterisk}}l{\isaliteral{2A}{\isacharasterisk}}k\ {\isaliteral{2B}{\isacharplus}}\ m{\isaliteral{2A}{\isacharasterisk}}n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}n{\isaliteral{2A}{\isacharasterisk}}m\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{2B}{\isacharplus}}\ k{\isaliteral{2A}{\isacharasterisk}}j{\isaliteral{2A}{\isacharasterisk}}l{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.115 -\isadelimproof
1.116 -%
1.117 -\endisadelimproof
1.118 -%
1.119 -\isatagproof
1.120 -%
1.121 -\begin{isamarkuptxt}%
1.122 -\begin{isabelle}%
1.123 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ l\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{2B}{\isacharplus}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ f\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2A}{\isacharasterisk}}\ m\ {\isaliteral{2B}{\isacharplus}}\ i\ {\isaliteral{2B}{\isacharplus}}\ k\ {\isaliteral{2A}{\isacharasterisk}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}%
1.124 -\end{isabelle}%
1.125 -\end{isamarkuptxt}%
1.126 -\isamarkuptrue%
1.127 -\isacommand{apply}\isamarkupfalse%
1.128 -\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ add{\isaliteral{5F}{\isacharunderscore}}ac\ mult{\isaliteral{5F}{\isacharunderscore}}ac{\isaliteral{29}{\isacharparenright}}%
1.129 -\begin{isamarkuptxt}%
1.130 -\begin{isabelle}%
1.131 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ Suc\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.132 -\isaindent{\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ }f\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2B}{\isacharplus}}\ j\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2A}{\isacharasterisk}}\ l{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
1.133 -\end{isabelle}%
1.134 -\end{isamarkuptxt}%
1.135 -\isamarkuptrue%
1.136 -\isacommand{oops}\isamarkupfalse%
1.137 -%
1.138 -\endisatagproof
1.139 -{\isafoldproof}%
1.140 -%
1.141 -\isadelimproof
1.142 -%
1.143 -\endisadelimproof
1.144 -%
1.145 -\begin{isamarkuptext}%
1.146 -\begin{isabelle}%
1.147 -m\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ div\ k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ n\ div\ k%
1.148 -\end{isabelle}
1.149 -\rulename{div_le_mono}
1.150 -
1.151 -\begin{isabelle}%
1.152 -{\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{3D}{\isacharequal}}\ m\ {\isaliteral{2A}{\isacharasterisk}}\ k\ {\isaliteral{2D}{\isacharminus}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ k%
1.153 -\end{isabelle}
1.154 -\rulename{diff_mult_distrib}
1.155 -
1.156 -\begin{isabelle}%
1.157 -a\ mod\ b\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}%
1.158 -\end{isabelle}
1.159 -\rulename{mult_mod_left}
1.160 -
1.161 -\begin{isabelle}%
1.162 -P\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2D}{\isacharminus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ {\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}d{\isaliteral{2E}{\isachardot}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2B}{\isacharplus}}\ d\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ P\ d{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
1.163 -\end{isabelle}
1.164 -\rulename{nat_diff_split}%
1.165 -\end{isamarkuptext}%
1.166 -\isamarkuptrue%
1.167 -\isacommand{lemma}\isamarkupfalse%
1.168 -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{1}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.169 -%
1.170 -\isadelimproof
1.171 -%
1.172 -\endisadelimproof
1.173 -%
1.174 -\isatagproof
1.175 -\isacommand{apply}\isamarkupfalse%
1.176 -\ {\isaliteral{28}{\isacharparenleft}}clarsimp\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split\ iff\ del{\isaliteral{3A}{\isacharcolon}}\ less{\isaliteral{5F}{\isacharunderscore}}Suc{\isadigit{0}}{\isaliteral{29}{\isacharparenright}}\isanewline
1.177 -\ %
1.178 -\isamarkupcmt{\begin{isabelle}%
1.179 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}d{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{3C}{\isacharless}}\ Suc\ {\isadigit{0}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{3D}{\isacharequal}}\ Suc\ d{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ d\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}%
1.180 -\end{isabelle}%
1.181 -}
1.182 -\isanewline
1.183 -\isacommand{apply}\isamarkupfalse%
1.184 -\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ force{\isaliteral{2C}{\isacharcomma}}\ arith{\isaliteral{29}{\isacharparenright}}\isanewline
1.185 -\isacommand{done}\isamarkupfalse%
1.186 -%
1.187 -\endisatagproof
1.188 -{\isafoldproof}%
1.189 -%
1.190 -\isadelimproof
1.191 -\isanewline
1.192 -%
1.193 -\endisadelimproof
1.194 -\isanewline
1.195 -\isanewline
1.196 -\isacommand{lemma}\isamarkupfalse%
1.197 -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}n\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{4}}{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}nat{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.198 -%
1.199 -\isadelimproof
1.200 -%
1.201 -\endisadelimproof
1.202 -%
1.203 -\isatagproof
1.204 -\isacommand{apply}\isamarkupfalse%
1.205 -\ {\isaliteral{28}{\isacharparenleft}}simp\ split{\isaliteral{3A}{\isacharcolon}}\ nat{\isaliteral{5F}{\isacharunderscore}}diff{\isaliteral{5F}{\isacharunderscore}}split{\isaliteral{2C}{\isacharcomma}}\ clarify{\isaliteral{29}{\isacharparenright}}\isanewline
1.206 -\ %
1.207 -\isamarkupcmt{\begin{isabelle}%
1.208 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}d{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}n\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{2}}{\isaliteral{3B}{\isacharsemicolon}}\ n\ {\isaliteral{2A}{\isacharasterisk}}\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{4}}\ {\isaliteral{2B}{\isacharplus}}\ d{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ d\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{0}}%
1.209 -\end{isabelle}%
1.210 -}
1.211 -\isanewline
1.212 -\isacommand{apply}\isamarkupfalse%
1.213 -\ {\isaliteral{28}{\isacharparenleft}}subgoal{\isaliteral{5F}{\isacharunderscore}}tac\ {\isaliteral{22}{\isachardoublequoteopen}}n{\isaliteral{3D}{\isacharequal}}{\isadigit{0}}\ {\isaliteral{7C}{\isacharbar}}\ n{\isaliteral{3D}{\isacharequal}}{\isadigit{1}}{\isaliteral{22}{\isachardoublequoteclose}}{\isaliteral{2C}{\isacharcomma}}\ force{\isaliteral{2C}{\isacharcomma}}\ arith{\isaliteral{29}{\isacharparenright}}\isanewline
1.214 -\isacommand{done}\isamarkupfalse%
1.215 -%
1.216 -\endisatagproof
1.217 -{\isafoldproof}%
1.218 -%
1.219 -\isadelimproof
1.220 -%
1.221 -\endisadelimproof
1.222 -%
1.223 -\begin{isamarkuptext}%
1.224 -\begin{isabelle}%
1.225 -m\ mod\ n\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}if\ m\ {\isaliteral{3C}{\isacharless}}\ n\ then\ m\ else\ {\isaliteral{28}{\isacharparenleft}}m\ {\isaliteral{2D}{\isacharminus}}\ n{\isaliteral{29}{\isacharparenright}}\ mod\ n{\isaliteral{29}{\isacharparenright}}%
1.226 -\end{isabelle}
1.227 -\rulename{mod_if}
1.228 -
1.229 -\begin{isabelle}%
1.230 -a\ div\ b\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b\ {\isaliteral{3D}{\isacharequal}}\ a%
1.231 -\end{isabelle}
1.232 -\rulename{mod_div_equality}
1.233 -
1.234 -
1.235 -\begin{isabelle}%
1.236 -a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ div\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c%
1.237 -\end{isabelle}
1.238 -\rulename{div_mult1_eq}
1.239 -
1.240 -\begin{isabelle}%
1.241 -a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c%
1.242 -\end{isabelle}
1.243 -\rulename{mod_mult_right_eq}
1.244 -
1.245 -\begin{isabelle}%
1.246 -a\ div\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b\ div\ c%
1.247 -\end{isabelle}
1.248 -\rulename{div_mult2_eq}
1.249 -
1.250 -\begin{isabelle}%
1.251 -a\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a\ div\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b%
1.252 -\end{isabelle}
1.253 -\rulename{mod_mult2_eq}
1.254 -
1.255 -\begin{isabelle}%
1.256 -c\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ div\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b%
1.257 -\end{isabelle}
1.258 -\rulename{div_mult_mult1}
1.259 -
1.260 -\begin{isabelle}%
1.261 -a\ div\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}%
1.262 -\end{isabelle}
1.263 -\rulename{div_by_0}
1.264 -
1.265 -\begin{isabelle}%
1.266 -a\ mod\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a%
1.267 -\end{isabelle}
1.268 -\rulename{mod_by_0}
1.269 -
1.270 -\begin{isabelle}%
1.271 -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}m\ dvd\ n{\isaliteral{3B}{\isacharsemicolon}}\ n\ dvd\ m{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ m\ {\isaliteral{3D}{\isacharequal}}\ n%
1.272 -\end{isabelle}
1.273 -\rulename{dvd_antisym}
1.274 -
1.275 -\begin{isabelle}%
1.276 -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}a\ dvd\ b{\isaliteral{3B}{\isacharsemicolon}}\ a\ dvd\ c{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ dvd\ b\ {\isaliteral{2B}{\isacharplus}}\ c%
1.277 -\end{isabelle}
1.278 -\rulename{dvd_add}
1.279 -
1.280 -For the integers, I'd list a few theorems that somehow involve negative
1.281 -numbers.%
1.282 -\end{isamarkuptext}%
1.283 -\isamarkuptrue%
1.284 -%
1.285 -\begin{isamarkuptext}%
1.286 -Division, remainder of negatives
1.287 -
1.288 -
1.289 -\begin{isabelle}%
1.290 -{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isadigit{0}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ a\ mod\ b%
1.291 -\end{isabelle}
1.292 -\rulename{pos_mod_sign}
1.293 -
1.294 -\begin{isabelle}%
1.295 -{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ b\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ b\ {\isaliteral{3C}{\isacharless}}\ b%
1.296 -\end{isabelle}
1.297 -\rulename{pos_mod_bound}
1.298 -
1.299 -\begin{isabelle}%
1.300 -b\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ b\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isadigit{0}}%
1.301 -\end{isabelle}
1.302 -\rulename{neg_mod_sign}
1.303 -
1.304 -\begin{isabelle}%
1.305 -b\ {\isaliteral{3C}{\isacharless}}\ {\isadigit{0}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ b\ {\isaliteral{3C}{\isacharless}}\ a\ mod\ b%
1.306 -\end{isabelle}
1.307 -\rulename{neg_mod_bound}
1.308 -
1.309 -\begin{isabelle}%
1.310 -{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ div\ c\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{28}{\isacharparenleft}}a\ mod\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c%
1.311 -\end{isabelle}
1.312 -\rulename{zdiv_zadd1_eq}
1.313 -
1.314 -\begin{isabelle}%
1.315 -{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ mod\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c%
1.316 -\end{isabelle}
1.317 -\rulename{mod_add_eq}
1.318 -
1.319 -\begin{isabelle}%
1.320 -a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ div\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ div\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ div\ c%
1.321 -\end{isabelle}
1.322 -\rulename{zdiv_zmult1_eq}
1.323 -
1.324 -\begin{isabelle}%
1.325 -a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ mod\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ mod\ c%
1.326 -\end{isabelle}
1.327 -\rulename{mod_mult_right_eq}
1.328 -
1.329 -\begin{isabelle}%
1.330 -{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ div\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ div\ b\ div\ c%
1.331 -\end{isabelle}
1.332 -\rulename{zdiv_zmult2_eq}
1.333 -
1.334 -\begin{isabelle}%
1.335 -{\isadigit{0}}\ {\isaliteral{3C}{\isacharless}}\ c\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ a\ mod\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a\ div\ b\ mod\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2B}{\isacharplus}}\ a\ mod\ b%
1.336 -\end{isabelle}
1.337 -\rulename{zmod_zmult2_eq}%
1.338 -\end{isamarkuptext}%
1.339 -\isamarkuptrue%
1.340 -\isacommand{lemma}\isamarkupfalse%
1.341 -\ {\isaliteral{22}{\isachardoublequoteopen}}abs\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2B}{\isacharplus}}y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ abs\ x\ {\isaliteral{2B}{\isacharplus}}\ abs\ {\isaliteral{28}{\isacharparenleft}}y\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.342 -%
1.343 -\isadelimproof
1.344 -%
1.345 -\endisadelimproof
1.346 -%
1.347 -\isatagproof
1.348 -\isacommand{by}\isamarkupfalse%
1.349 -\ arith%
1.350 -\endisatagproof
1.351 -{\isafoldproof}%
1.352 -%
1.353 -\isadelimproof
1.354 -\isanewline
1.355 -%
1.356 -\endisadelimproof
1.357 -\isanewline
1.358 -\isacommand{lemma}\isamarkupfalse%
1.359 -\ {\isaliteral{22}{\isachardoublequoteopen}}abs\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}{\isaliteral{2A}{\isacharasterisk}}x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isadigit{2}}\ {\isaliteral{2A}{\isacharasterisk}}\ abs\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ int{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.360 -%
1.361 -\isadelimproof
1.362 -%
1.363 -\endisadelimproof
1.364 -%
1.365 -\isatagproof
1.366 -\isacommand{by}\isamarkupfalse%
1.367 -\ {\isaliteral{28}{\isacharparenleft}}simp\ add{\isaliteral{3A}{\isacharcolon}}\ abs{\isaliteral{5F}{\isacharunderscore}}if{\isaliteral{29}{\isacharparenright}}%
1.368 -\endisatagproof
1.369 -{\isafoldproof}%
1.370 -%
1.371 -\isadelimproof
1.372 -%
1.373 -\endisadelimproof
1.374 -%
1.375 -\begin{isamarkuptext}%
1.376 -Induction rules for the Integers
1.377 -
1.378 -\begin{isabelle}%
1.379 -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ k{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{5C3C6C653E}{\isasymle}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
1.380 -\end{isabelle}
1.381 -\rulename{int_ge_induct}
1.382 -
1.383 -\begin{isabelle}%
1.384 -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}k\ {\isaliteral{3C}{\isacharless}}\ i{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2B}{\isacharplus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
1.385 -\end{isabelle}
1.386 -\rulename{int_gr_induct}
1.387 -
1.388 -\begin{isabelle}%
1.389 -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ k{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
1.390 -\end{isabelle}
1.391 -\rulename{int_le_induct}
1.392 -
1.393 -\begin{isabelle}%
1.394 -{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{3C}{\isacharless}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ {\isaliteral{28}{\isacharparenleft}}k\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C416E643E}{\isasymAnd}}i{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}i\ {\isaliteral{3C}{\isacharless}}\ k{\isaliteral{3B}{\isacharsemicolon}}\ P\ i{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{28}{\isacharparenleft}}i\ {\isaliteral{2D}{\isacharminus}}\ {\isadigit{1}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ i%
1.395 -\end{isabelle}
1.396 -\rulename{int_less_induct}%
1.397 -\end{isamarkuptext}%
1.398 -\isamarkuptrue%
1.399 -%
1.400 -\begin{isamarkuptext}%
1.401 -FIELDS
1.402 -
1.403 -\begin{isabelle}%
1.404 -x\ {\isaliteral{3C}{\isacharless}}\ y\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C6578697374733E}{\isasymexists}}z{\isaliteral{3E}{\isachargreater}}x{\isaliteral{2E}{\isachardot}}\ z\ {\isaliteral{3C}{\isacharless}}\ y%
1.405 -\end{isabelle}
1.406 -\rulename{dense}
1.407 -
1.408 -\begin{isabelle}%
1.409 -a\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2F}{\isacharslash}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c%
1.410 -\end{isabelle}
1.411 -\rulename{times_divide_eq_right}
1.412 -
1.413 -\begin{isabelle}%
1.414 -b\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{2F}{\isacharslash}}\ c%
1.415 -\end{isabelle}
1.416 -\rulename{times_divide_eq_left}
1.417 -
1.418 -\begin{isabelle}%
1.419 -a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2F}{\isacharslash}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{2F}{\isacharslash}}\ b%
1.420 -\end{isabelle}
1.421 -\rulename{divide_divide_eq_right}
1.422 -
1.423 -\begin{isabelle}%
1.424 -a\ {\isaliteral{2F}{\isacharslash}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{28}{\isacharparenleft}}b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}%
1.425 -\end{isabelle}
1.426 -\rulename{divide_divide_eq_left}
1.427 -
1.428 -\begin{isabelle}%
1.429 -{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{2D}{\isacharminus}}\ a\ {\isaliteral{2F}{\isacharslash}}\ b%
1.430 -\end{isabelle}
1.431 -\rulename{minus_divide_left}
1.432 -
1.433 -\begin{isabelle}%
1.434 -{\isaliteral{2D}{\isacharminus}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2F}{\isacharslash}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ {\isaliteral{2D}{\isacharminus}}\ b%
1.435 -\end{isabelle}
1.436 -\rulename{minus_divide_right}
1.437 -
1.438 -This last NOT a simprule
1.439 -
1.440 -\begin{isabelle}%
1.441 -{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{3D}{\isacharequal}}\ a\ {\isaliteral{2F}{\isacharslash}}\ c\ {\isaliteral{2B}{\isacharplus}}\ b\ {\isaliteral{2F}{\isacharslash}}\ c%
1.442 -\end{isabelle}
1.443 -\rulename{add_divide_distrib}%
1.444 -\end{isamarkuptext}%
1.445 -\isamarkuptrue%
1.446 -\isacommand{lemma}\isamarkupfalse%
1.447 -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{7}}{\isaliteral{2F}{\isacharslash}}{\isadigit{8}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline
1.448 -%
1.449 -\isadelimproof
1.450 -%
1.451 -\endisadelimproof
1.452 -%
1.453 -\isatagproof
1.454 -\isacommand{by}\isamarkupfalse%
1.455 -\ simp%
1.456 -\endisatagproof
1.457 -{\isafoldproof}%
1.458 -%
1.459 -\isadelimproof
1.460 -\ \isanewline
1.461 -%
1.462 -\endisadelimproof
1.463 -\isanewline
1.464 -\isacommand{lemma}\isamarkupfalse%
1.465 -\ {\isaliteral{22}{\isachardoublequoteopen}}P\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{5}}\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.466 -\isadelimproof
1.467 -%
1.468 -\endisadelimproof
1.469 -%
1.470 -\isatagproof
1.471 -%
1.472 -\begin{isamarkuptxt}%
1.473 -\begin{isabelle}%
1.474 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
1.475 -\end{isabelle}%
1.476 -\end{isamarkuptxt}%
1.477 -\isamarkuptrue%
1.478 -\isacommand{apply}\isamarkupfalse%
1.479 -\ simp%
1.480 -\begin{isamarkuptxt}%
1.481 -\begin{isabelle}%
1.482 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{2}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{5}}{\isaliteral{29}{\isacharparenright}}%
1.483 -\end{isabelle}%
1.484 -\end{isamarkuptxt}%
1.485 -\isamarkuptrue%
1.486 -\isacommand{oops}\isamarkupfalse%
1.487 -%
1.488 -\endisatagproof
1.489 -{\isafoldproof}%
1.490 -%
1.491 -\isadelimproof
1.492 -%
1.493 -\endisadelimproof
1.494 -\isanewline
1.495 -\isanewline
1.496 -\isacommand{lemma}\isamarkupfalse%
1.497 -\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isadigit{3}}{\isaliteral{2F}{\isacharslash}}{\isadigit{4}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}{\isaliteral{2F}{\isacharslash}}{\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ {\isaliteral{28}{\isacharparenleft}}x\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ real{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}%
1.498 -\isadelimproof
1.499 -%
1.500 -\endisadelimproof
1.501 -%
1.502 -\isatagproof
1.503 -%
1.504 -\begin{isamarkuptxt}%
1.505 -\begin{isabelle}%
1.506 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{3}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{4}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{8}}\ {\isaliteral{2F}{\isacharslash}}\ {\isadigit{1}}{\isadigit{5}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3C}{\isacharless}}\ x%
1.507 -\end{isabelle}%
1.508 -\end{isamarkuptxt}%
1.509 -\isamarkuptrue%
1.510 -\isacommand{apply}\isamarkupfalse%
1.511 -\ simp%
1.512 -\begin{isamarkuptxt}%
1.513 -\begin{isabelle}%
1.514 -\ {\isadigit{1}}{\isaliteral{2E}{\isachardot}}\ {\isadigit{2}}\ {\isaliteral{3C}{\isacharless}}\ x\ {\isaliteral{2A}{\isacharasterisk}}\ {\isadigit{5}}%
1.515 -\end{isabelle}%
1.516 -\end{isamarkuptxt}%
1.517 -\isamarkuptrue%
1.518 -\isacommand{oops}\isamarkupfalse%
1.519 -%
1.520 -\endisatagproof
1.521 -{\isafoldproof}%
1.522 -%
1.523 -\isadelimproof
1.524 -%
1.525 -\endisadelimproof
1.526 -%
1.527 -\begin{isamarkuptext}%
1.528 -Ring and Field
1.529 -
1.530 -Requires a field, or else an ordered ring
1.531 -
1.532 -\begin{isabelle}%
1.533 -{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2A}{\isacharasterisk}}\ b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ b\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}%
1.534 -\end{isabelle}
1.535 -\rulename{mult_eq_0_iff}
1.536 -
1.537 -\begin{isabelle}%
1.538 -{\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{2A}{\isacharasterisk}}\ c\ {\isaliteral{3D}{\isacharequal}}\ b\ {\isaliteral{2A}{\isacharasterisk}}\ c{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}%
1.539 -\end{isabelle}
1.540 -\rulename{mult_cancel_right}
1.541 -
1.542 -\begin{isabelle}%
1.543 -{\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{2A}{\isacharasterisk}}\ a\ {\isaliteral{3D}{\isacharequal}}\ c\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}%
1.544 -\end{isabelle}
1.545 -\rulename{mult_cancel_left}%
1.546 -\end{isamarkuptext}%
1.547 -\isamarkuptrue%
1.548 -%
1.549 -\begin{isamarkuptext}%
1.550 -effect of show sorts on the above
1.551 -
1.552 -\begin{isabelle}%
1.553 -{\isaliteral{28}{\isacharparenleft}}{\isaliteral{28}{\isacharparenleft}}c{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.554 -\isaindent{{\isaliteral{28}{\isacharparenleft}}}c\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{28}{\isacharparenleft}}b{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline
1.555 -{\isaliteral{28}{\isacharparenleft}}c\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isadigit{0}}{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}{\isaliteral{27}{\isacharprime}}a{\isaliteral{5C3C436F6C6F6E3E}{\isasymColon}}ring{\isaliteral{5F}{\isacharunderscore}}no{\isaliteral{5F}{\isacharunderscore}}zero{\isaliteral{5F}{\isacharunderscore}}divisors{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C6F723E}{\isasymor}}\ a\ {\isaliteral{3D}{\isacharequal}}\ b{\isaliteral{29}{\isacharparenright}}%
1.556 -\end{isabelle}
1.557 -\rulename{mult_cancel_left}%
1.558 -\end{isamarkuptext}%
1.559 -\isamarkuptrue%
1.560 -%
1.561 -\begin{isamarkuptext}%
1.562 -absolute value
1.563 -
1.564 -\begin{isabelle}%
1.565 -{\isaliteral{5C3C6261723E}{\isasymbar}}a\ {\isaliteral{2A}{\isacharasterisk}}\ b{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{2A}{\isacharasterisk}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}b{\isaliteral{5C3C6261723E}{\isasymbar}}%
1.566 -\end{isabelle}
1.567 -\rulename{abs_mult}
1.568 -
1.569 -\begin{isabelle}%
1.570 -{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{2D}{\isacharminus}}\ a\ {\isaliteral{5C3C6C653E}{\isasymle}}\ b{\isaliteral{29}{\isacharparenright}}%
1.571 -\end{isabelle}
1.572 -\rulename{abs_le_iff}
1.573 -
1.574 -\begin{isabelle}%
1.575 -{\isaliteral{5C3C6261723E}{\isasymbar}}a\ {\isaliteral{2B}{\isacharplus}}\ b{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{5C3C6C653E}{\isasymle}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{2B}{\isacharplus}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}b{\isaliteral{5C3C6261723E}{\isasymbar}}%
1.576 -\end{isabelle}
1.577 -\rulename{abs_triangle_ineq}
1.578 -
1.579 -\begin{isabelle}%
1.580 -a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\ {\isaliteral{2B}{\isacharplus}}\ n\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{3D}{\isacharequal}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{2A}{\isacharasterisk}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup %
1.581 -\end{isabelle}
1.582 -\rulename{power_add}
1.583 -
1.584 -\begin{isabelle}%
1.585 -a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\ {\isaliteral{2A}{\isacharasterisk}}\ n\isaliteral{5C3C5E657375703E}{}\isactrlesup \ {\isaliteral{3D}{\isacharequal}}\ a\isaliteral{5C3C5E627375703E}{}\isactrlbsup m\isaliteral{5C3C5E657375703E}{}\isactrlesup \isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup %
1.586 -\end{isabelle}
1.587 -\rulename{power_mult}
1.588 -
1.589 -\begin{isabelle}%
1.590 -{\isaliteral{5C3C6261723E}{\isasymbar}}a\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup {\isaliteral{5C3C6261723E}{\isasymbar}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{5C3C6261723E}{\isasymbar}}a{\isaliteral{5C3C6261723E}{\isasymbar}}\isaliteral{5C3C5E627375703E}{}\isactrlbsup n\isaliteral{5C3C5E657375703E}{}\isactrlesup %
1.591 -\end{isabelle}
1.592 -\rulename{power_abs}%
1.593 -\end{isamarkuptext}%
1.594 -\isamarkuptrue%
1.595 -%
1.596 -\isadelimtheory
1.597 -%
1.598 -\endisadelimtheory
1.599 -%
1.600 -\isatagtheory
1.601 -\isacommand{end}\isamarkupfalse%
1.602 -%
1.603 -\endisatagtheory
1.604 -{\isafoldtheory}%
1.605 -%
1.606 -\isadelimtheory
1.607 -%
1.608 -\endisadelimtheory
1.609 -\isanewline
1.610 -\end{isabellebody}%
1.611 -%%% Local Variables:
1.612 -%%% mode: latex
1.613 -%%% TeX-master: "root"
1.614 -%%% End: